Екзистенційні висловлювання

У логіці предикатів, квантифікація існування — тип квантора, логічна константа, яка інтерпретується як «існує», «є принаймні один» або «для деяких». Деякі джерела використовують термін екзистенціалізація для позначення квантифікації існування. Вона зазвичай позначається символом логічного оператора ^[en] (${\displaystyle \exists }$), який при використанні разом зі змінною предикату називається квантором існування (${\displaystyle \exists {x}}$ або ${\displaystyle \exists {\left(x\right)}}$). Квантор існування відрізняється від квантора загальності («для всіх»), який припускає, що властивість або відношення має місце для всіх членів області.

Квантор існування
Нотація	∃^[d]
Підтримується Вікіпроєктом
Протилежне	квантор загальності

Основи

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

${\displaystyle 0\cdot 0=25}$, або ${\displaystyle 1\cdot 1=25}$, або ${\displaystyle 2\cdot 2=25}$, або ${\displaystyle 3\cdot 3=25}$, і так далі.

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

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

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

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

Для деякого додатного непарного числа n, ${\displaystyle n\cdot n=25}$

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

Для деякого натурального числа n, n непарне та ${\displaystyle n\cdot n=25}$.

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

У символічній логіці, «${\displaystyle \exists }$» (зворотна літера «E» у гротескному шрифті) використовується для позначення квантора існування. Тому, якщо ${\displaystyle P\left(a,b,c\right)}$ є предикатом «${\displaystyle a\cdot b=c}$», а ${\displaystyle \mathbb {N} }$ є множиною натуральних чисел, то

${\displaystyle \exists {n\in \mathbb {N} }\,P(n,n,25)}$

є (істинним) судженням: Для деякого натурального числа n, ${\displaystyle n\cdot n=25}$. Аналогічно, якщо ${\displaystyle Q\left(n\right)}$ є предикатом «n парне», то

${\displaystyle \exists {n\in \mathbb {N} }\,{\big (}Q\left(n\right)\land P\left(n,n,25\right){\big )}}$

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

Властивості

Заперечення

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

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

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

${\displaystyle \exists {x\in \mathbf {X} }\,P\left(x\right)}$

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

${\displaystyle \lnot {\exists {x\in \mathbf {X} }\,P\left(x\right)}}$.

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

${\displaystyle \exists {x\in \mathbf {X} }\,P\left(x\right)}$

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

${\displaystyle \forall {x\in \mathbf {X} }\,\lnot {P\left(x\right)}}$

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

${\displaystyle \lnot \exists {x}{\in }\mathbf {X} \,P(x)\equiv \ \forall {x}{\in }\mathbf {X} \,\lnot P(x)}$

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

${\displaystyle \lnot \exists {x}{\in }\mathbf {X} \,P(x)\equiv \ \forall {x}{\in }\mathbf {X} \,\lnot P(x)\not \equiv \ \lnot \ \forall {x}{\in }\mathbf {X} \,P(x)\equiv \ \exists {x}{\in }\mathbf {X} \,\lnot P(x)}$

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

${\displaystyle \nexists {x}{\in }\mathbf {X} \,P(x)\equiv \lnot \ \exists {x}{\in }\mathbf {X} \,P(x)}$

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

${\displaystyle \exists {x}{\in }\mathbf {X} \,P(x)\lor Q(x)\to \ (\exists {x}{\in }\mathbf {X} \,P(x)\lor \exists {x}{\in }\mathbf {X} \,Q(x))}$

Правило висновування

Докладніше: Правило висновування

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

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

${\displaystyle P\left(a\right)\to \ \exists {x}{\in }\mathbf {X} \,P\left(x\right)}$

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

${\displaystyle \exists {x\in \mathbf {X} }\,P\left(x\right)\to {\big (}\left(P\left(c\right)\to Q\right)\to Q{\big )}}$

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

Порожня множина

Формула ${\displaystyle \exists {x\in \emptyset }P\left(x\right)}$ завжди хибна, незалежно від ${\displaystyle P\left(x\right)}$. Це так, оскільки ${\displaystyle \emptyset }$ позначає порожню множину, і немає x будь-якого опису — не кажучи вже про x, що задовольняє даний предикат ${\displaystyle P\left(x\right)}$ — існує в порожній множині. Див. також ^[en].

Як приєднання

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

HTML-кодування кванторів існування

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

Див. також

• ^[en]
• Квантори
• Логіка першого порядку
• Список логічних символів — для Юнікодного символу ${\displaystyle \exists }$
• Єдиність

Примітки

1. Аллен, Колін; Ганд, Майкл (2001). (англійською) . MIT Press. ISBN . Архів оригіналу за 11 Березня 2017. Процитовано 3 Березня 2018.
2. Цей символ також відомий як оператор існування.
3. Маклейн, Саундерс; Мордійк, Айк (1992). Sheaves in Geometry and Logic. Springer-Verlag. с. 58. ISBN .

Література

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