Відкрити головне меню

У логіці предикатів, квантифікація існування — тип квантора, логічна константа, яка інтерпретується як «існує», «є принаймні один» або «для деяких». Деякі джерела використовують термін екзистенціалізація для позначення квантифікації існування[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.