Квантор існування
Квантор існування | |
Нотація | ∃[d] |
---|---|
Протилежно | квантор загальності |
У логіці предикатів, квантифікація існування — тип квантора, логічна константа, яка інтерпретується як «існує», «є принаймні один» або «для деяких». Деякі джерела використовують термін екзистенціалізація для позначення квантифікації існування[1]. Вона зазвичай позначається символом логічного оператора обернена E[en] (), який при використанні разом зі змінною предикату називається квантором існування ( або ). Квантор існування відрізняється від квантора загальності («для всіх»), який припускає, що властивість або відношення має місце для всіх членів області.
Основи[ред. | ред. код]
Розглянемо формулу, яка стверджує, що деяке натуральне число, помножене на себе, дорівнює 25.
- , або , або , або , і так далі.
Це, здавалося б, є логічною диз'юнкцією через повторюване використання «або». Проте, «і так далі» унеможливлює інтеграцію й інтерпретацію як диз'юнкцію у формальній логіці. Натомість, судження може бути перефразоване формальніше як: Для деякого натурального числа n, . Це одиночне судження з використанням квантора існування.
Це судження точніше за початкове, оскільки фраза «і так далі» необов'язково включає всі натуральні числа, і нічого більше. Оскільки область не було задано явно, фраза не може інтерпретуватися формально. У квантифікованому судженні, з іншого боку, натуральні числа згадуються явно.
Це конкретний приклад є істинним, оскільки 5 є натуральним числом, і коли ми підставляємо 5 замість n, ми отримуємо «», що є істиною. Неважливо, що «» є істиною для єдиного натурального числа 5; навіть існування єдиного розв'язку достатньо для доведення істинності квантора існування. На противагу, «Для деякого парного числа n, » є хибним, оскільки не існує парних розв'язків.
Область дискурсу[en] задає, які значення змінної n дозволено брати, тому має вирішальне значення в істинності чи хибності судження. Логічна кон'юнкція використовується для обмеження області дискурсу для виконання даного предикату. Наприклад:
- Для деякого додатного непарного числа n,
- Для деякого натурального числа 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].
Як приєднання[ред. | ред. код]
У теорії категорій і теорії елементарних топосів, квантор існування може розумітися як ліве приєднання функтора між булеанами, функтором оберненого образу функції між множинами; так само квантор загальності є правим приєднанням[3].
HTML-кодування кванторів існування[ред. | ред. код]
Символи кодуються U+2203 ∃ ІСНУЄ (як математичний символ) та U+2204 ∄ НЕ ІСНУЄ.
Див. також[ред. | ред. код]
- Дисперсія квантора[en]
- Квантори
- Логіка першого порядку
- Список логічних символів — для Юнікодного символу
- Єдиність
Примітки[ред. | ред. код]
- ↑ Аллен, Колін; Ганд, Майкл (2001). Logic Primer (англійською). MIT Press. ISBN 0262303965. Архів оригіналу за 11 Березня 2017. Процитовано 3 Березня 2018.
- ↑ Цей символ також відомий як оператор існування.
- ↑ Маклейн, Саундерс; Мордійк, Айк (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.