Квантор існування

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

У логіці предикатів, квантифікація існування — тип квантора, логічна константа, яка інтерпретується як «існує», «є принаймні один» або «для деяких». Деякі джерела використовують термін екзистенціалізація для позначення квантифікації існування[1]. Вона зазвичай позначається символом логічного оператора обернена E[en] (), який при використанні разом зі змінною предикату називається квантором існування ( або ). Квантор існування відрізняється від квантора загальності («для всіх»), який припускає, що властивість або відношення має місце для всіх членів області.

Основи[ред. | ред. код]

Розглянемо формулу, яка стверджує, що деяке натуральне число, помножене на себе, дорівнює 25.

, або , або , або , і так далі.

Це, здавалося б, є логічною диз'юнкцією через повторюване використання «або». Проте, «і так далі» унеможливлює інтеграцію й інтерпретацію як диз'юнкцію у формальній логіці. Натомість, судження може бути перефразоване формальніше як: Для деякого натурального числа n, . Це одиночне судження з використанням квантора існування.

Це судження точніше за початкове, оскільки фраза «і так далі» необов'язково включає всі натуральні числа, і нічого більше. Оскільки область не було задано явно, фраза не може інтерпретуватися формально. У квантифікованому судженні, з іншого боку, натуральні числа згадуються явно.

Це конкретний приклад є істинним, оскільки 5 є натуральним числом, і коли ми підставляємо 5 замість n, ми отримуємо «», що є істиною. Неважливо, що «» є істиною для єдиного натурального числа 5; навіть існування єдиного розв'язку достатньо для доведення істинності квантора існування. На противагу, «Для деякого парного числа n, » є хибним, оскільки не існує парних розв'язків.

Область дискурсу[en] задає, які значення змінної n дозволено брати, тому має вирішальне значення в істинності чи хибності судження. Логічна кон'юнкція використовується для обмеження області дискурсу для виконання даного предикату. Наприклад:

Для деякого додатного непарного числа n,

є логічним еквівалентом[en]

Для деякого натурального числа n, n непарне та .

Тут, «та» є логічною кон'юнкцією.

У символічній логіці, «» (зворотна літера «E» у гротескному шрифті) використовується для позначення квантора існування[2]. Тому, якщо є предикатом «», а є множиною натуральних чисел, то

є (істинним) судженням: Для деякого натурального числа n, . Аналогічно, якщо є предикатом «n парне», то

є (хибним) судженням: Для деякого натурального числа n, n парне та . У математиці, доведення «деякого» судження можна досягти або конструктивним доведенням, яке показує задоволення об'єкта «деякому» судженню, або неконструктивним доведенням, яке показує існування такого об'єкту, не показуючи сам об'єкт.

Властивості[ред. | ред. код]

Заперечення[ред. | ред. код]

Докладніше: Заперечення

Квантифікована пропозиційна функція є судженням; тому, як і судження, квантифіковані функції можуть бути заперечені. Символ   використовується для позначення заперечення.

Наприклад, якщо  — пропозиційна функція «x більше 0 і менше 1», то для області дискурсу X усіх натуральних чисел квантор існування «Існує натуральне число x, яке більше 0 і менше 1» символічно має вигляд:

Можливо продемонструвати його хибність. По правді, варто сказати: «Це не випадок, що існує натуральне число x, яке більше 0 і менше 1», або символічно:

.

Якщо немає елементів області дискурсу, для якого судження істинне, то воно повинно бути хибним для всіх таких елементів. Тобто, заперечення

є логічним еквівалентом «Для будь якого натурального числа x, x не більше 0 і менше 1», або:

Загалом, тоді заперечення квантора існування пропозиційної функції є квантором загальності заперечення тієї ж пропозиційної функції; символічно:

Поширеною помилкою є казати «всі особи неодружені» (тобто «не існує особи, яка одружена»), маючи на увазі «не всі особи одружені» (тобто «існує особа, яка неодружена»):

Заперечення також висловлюється через судження «для жодного», на відміну від «для деяких»:

На відміну від квантора загальності, квантор існування поширюється над логічними диз'юнкціями:

Правило висновування[ред. | ред. код]

Правило висновування — правило, що виправдовує логічний крок від гіпотези до висновку. Існують декілька правил висновувань, які використовують квантор існування.

Екзистенційне введення[en] () заключає, що, якщо пропозиційна функція, як відомо, істинна для конкретного елементу області дискурсу, то повинно бути істиною те, що існує елемент, для якого пропозиційна функція істинна. Символічно:

Усунення існування, коли проводиться у дедукції стиля Фітча, продовжується введенням нового під-висновку, поки підстановка змінної під квантором існування для теми, яка не з'являється в будь-якому активному під-висновку. Якщо висновку можна досягти в тому ж під-висновку, у якому підставлена тема не з'являється, то може вийти під-висновок з тим висновком. Міркування за усуненням існування () наступні: Якщо дано, що існує елемент, для якого пропозиційна функція істинна, і якщо висновку можна досягти, давши цьому елементові довільне ім'я, то висновок неодмінно істинний так довго, поки він не містить імені. Символічно, для довільного c і пропозиції Q, в якій c не з'являється:

повинно бути істиною для всіх значень c над тією ж областю X; інакше логіка не слідує: Якщо c не довільний, і є натомість конкретний елемент області дискурсу, то заява P(c) може невиправдано дати більше інформації про той об'єкт.

Порожня множина[ред. | ред. код]

Формула завжди хибна, незалежно від . Це так, оскільки позначає порожню множину, і немає x будь-якого опису — не кажучи вже про x, що задовольняє даний предикат  — існує в порожній множині. Див. також порожня істина[en].

Як приєднання[ред. | ред. код]

У теорії категорій і теорії елементарних топосів[ru], квантор існування може розумітися як ліве приєднання[en] функтора між булеанами, функтором оберненого образу функції між множинами; так само квантор загальності є правим приєднанням[en][3].

HTML-кодування кванторів існування[ред. | ред. код]

Символи кодуються U+2203 ІСНУЄ (як математичний символ) та U+2204 НЕ ІСНУЄ.

Див. також[ред. | ред. код]

Примітки[ред. | ред. код]

  1. Аллен, Колін; Ганд, Майкл (2001). Logic Primer (англійською). MIT Press. ISBN 0262303965. 
  2. Цей символ також відомий як оператор існування.
  3. Маклейн, Саундерс; Мордійк, Айк (1992). Sheaves in Geometry and Logic. Springer-Verlag. с. 58. ISBN 0-387-97710-4. 

Література[ред. | ред. код]

  • Гінман, П. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.