Інтуїціоністська логіка

Інтуїтивна логіка (інколи конструктивна логіка) — система символічної логіки, яка відрізняється від класичної логіки, замінюючи традиційне поняття істини поняттям конструктивно доказової істини. Наприклад, у класичній логіці, пропозиціональні формули (предикати) завжди приймають значення істинності з множини двох тривіальних елементів тверджень $\{\mathrm{\top },\mathrm{\perp }\}$ («істина» і «хиба» відповідно) незалежно від того, чи є у нас прямий доказ для будь-якого випадку. Навпаки, пропозиціональним формулам (предикатам) в інтуїтивній логіці взагалі не надається жодного певного значення істинності: натомість вони вважаються «істинними» лише тоді, коли у нас є прямий доказ. (Замість «формула істинна на основі прямого доказу» можна також сказати, що формула Шаблон:Не перекладено доказом у сенсі Каррі — Говарда). Тому операції в інтуїтивній логіці зберігають Шаблон:Не перекладено, щодо доказу та доказової операції, а не оцінки істини.

Недоведеним твердженням в інтуїтивній логіці не надаються проміжні значення істинності (як іноді помилково стверджується). Справді, можна довести, що у них немає третього значення істинності, що було визначено Гливенком у 1928. Замість цього вони залишаються з невідомим значенням істинності, доти, доки вони або не доведені, або не спростовані. Твердження спростовуються, виводом з них протиріччя.

Наслідком цього погляду є те, що в інтуїтивної логіки немає інтерпретації як двозначної логіки, або навіть як логіки з кінцевим знаком. Попри те, що інтуїтивна логіка зберігає тривіальні судження $\{\mathrm{\top },\mathrm{\perp }\}$ наслідувані від класичної логіки, кожен доказ пропозиціональної формули вважається допустимим пропозиціональним значенням, таким чином, за поняттям твердження Шаблон:Не перекладено про множини, пропозиціональні формули (потенційні чи не кінцеві) — це множини особистих доказів.

Семантично, інтуїтивна логіка є обмеженням класичної логіки, в якій закон виключеного третього та усунення подвійного заперечення не допускаються як аксіоми. Закон виключеного третього та усунення подвійного заперечення можуть все ще бути доведені для деяких висловлювань на індивідуальній основі, але не виконуватися універсально, як вони це робили з класичною логікою.

Кілька семантик інтуїтивної логіки було вивчено. Одна семантика відбиває класичну Шаблон:Не перекладено, але використовує алгебру Гейтінга замість булевої алгебри. Інша семантика використовує модель Кріпке.

Інтуїтивна логіка практично корисна, бо її обмеження створюють докази, у яких є Шаблон:Не перекладено, роблячи її також відповідною для інших форм математичного конструктивізму. Неофіційно, це означає, що, якщо у Вас є конструктивний доказ того, що об'єкт існує, то Ви можете перетворити цей конструктивний доказ в алгоритм для генерації його прикладу.

Формалізована інтуїтивна логіка була спочатку розроблена Арендом Гейтінгом, щоб забезпечити формальну основу для програми інтуїтивізму Брауера.

Синтаксис

Решітка Rieger-Nishimura. Її вузли - пропозиціональні формули в однієї змінної до інтуїціоністської логічної еквівалентності, впорядкованої інтуїціоністською логічною імплікацією.

Синтаксис формул інтуїтивної логіки подібний логіці висловлювань або логіці першого порядку. Проте, інтуїціоністські зв'язки не визначені один з одним таким самим чином, як у класичній логіці, отже, їх вибір має значення. В інтуїціоністській логіці прийнято використовувати →, ∧, ∨, ⊥ як основні зв'язки, розглядаючи ¬A як скорочення для Шаблон:Nowrap. В інтуїціоністській логіці першого порядку необхідні обидва квантора ∃, ∀.

Багато тавтологій класичної логіки більше не можуть доводитися в інтуїтивній логіці. Приклади включають не лише закон виключеного третього Шаблон:Nowrap, але також і закон Пірса Шаблон:Nowrap, і навіть усунення подвійного заперечення. У класичній логіці і Шаблон:Nowrap, і також Шаблон:Nowrap є теоремами. В інтуїтивній логіці лише для першого є теорема: подвійне заперечення може бути представлено, але воно не може бути усунуто. Відкидання Шаблон:Nowrap може здаватися дивним для тих, хто більш знайомий з класичною логікою, але доказ цієї пропозиціональної формули в інтуїтивній логіці вимагав би створення доказів для істинності або хибності всіх можливих пропозиціональних формул, які неможливі для ряду причин.

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

Подальше обчислення

Ґергард Ґенцен виявив, що просте обмеження його системи, LK (його подальше обчислення для класичної логіки) приводить до системи, яка є звуковою та сповненою щодо інтуїтивної логіки. Він назвав цю систему LJ. У LK будь-якому числу формул дозволяють з'явитися на стороні укладення наступного; у відмінності LJ дозволяє не більше однієї формули у цій позиції. Інші похідні LK обмежені інтуїціоністськими похідними, але все ще дозволяють багаторазові укладення в наступному. LJ' є одним з прикладів.

Обчислення стилю Гільберта

Інтуїтивна логіка може бути визначена, використовуючи наступне обчислення Шаблон:Не перекладено. Це схоже на спосіб аксіоматизації класичної логіки висловлювань. У логіці висловлювань правилом висновку є modus ponens.

• MP: від $\varphi$ і $\varphi \to \psi$ виводять $\psi$

Аксіоми логіки висловлювань:

• ТОДІ-1: $\varphi \to (\chi \to \varphi )$
• ТОДІ-2: $(\varphi \to (\chi \to \psi ))\to ((\varphi \to \chi )\to (\varphi \to \psi ))$
• І-1: $\varphi \wedge \chi \to \varphi$
• І-2: $\varphi \wedge \chi \to \chi$
• І-3: $\varphi \to (\chi \to (\varphi \wedge \chi ))$
• АБО-1: $\varphi \to \varphi \vee \chi$
• АБО-2: $\chi \to \varphi \vee \chi$
• АБО-3: $(\varphi \to \psi )\to ((\chi \to \psi )\to (\varphi \vee \chi \to \psi ))$
• ХИБА: $\mathrm{\perp }\to \varphi$

Правила узагальнення роблять це системою логіки предикатів першого порядку

• $\mathrm{\forall }$ — ГЕНЕРАЛ: від $\psi \to \varphi$ виводять $\psi \to (\mathrm{\forall }x\varphi )$, якщо $x$ не вільний в $\psi$

$\mathrm{\exists }$ — ГЕНЕРАЛ: від $\varphi \to \psi$ виводять $(\mathrm{\exists }x\varphi )\to \psi$, якщо $x$ не вільний в $\psi$

І додаються разом з аксіомами

• PRED-1: $(\mathrm{\forall }x\varphi (x))\to \varphi (t)$, якщо термін t вільний для заміни на змінну x в $\varphi$ (тобто, якщо ніяке виникнення якої-небудь змінної в t не стає пов'язаним в $\varphi (t)$),
• PRED-2: $\varphi (t)\to (\mathrm{\exists }x\varphi (x))$, з тим же обмеженням що стосується PRED-1

Додаткові зв'язки

Заперечення

Якщо Ви хочете включати з'єднувальний $\mathrm{\neg }$ для заперечення, а не вважати його скороченням для $\varphi \to \mathrm{\perp }$, достатньо додати:

• НЕ-1': $(\varphi \to \mathrm{\perp })\to \mathrm{\neg }\varphi$
• НЕ-2': $\mathrm{\neg }\varphi \to (\varphi \to \mathrm{\perp })$

Є багато доступних альтернатив, якщо Ви хочете опустити з'єднувальний $\mathrm{\perp }$(хиба). Наприклад, можна замінити ці три аксіоми ХИБА, НЕ 1 ', і НЕ 2 ' цими двома аксіомами

• НЕ-1: $(\varphi \to \chi )\to ((\varphi \to \mathrm{\neg }\chi )\to \mathrm{\neg }\varphi )$
• НЕ-2: $\varphi \to (\mathrm{\neg }\varphi \to \chi )$

як в аксіомах альтернативних числень. Альтернативи НЕ-1 $(\varphi \to \mathrm{\neg }\chi )\to (\chi \to \mathrm{\neg }\varphi )$ або $(\varphi \to \mathrm{\neg }\varphi )\to \mathrm{\neg }\varphi$.

Еквівалентність

З'єднувальний $\leftrightarrow$ для еквівалентності можна розглядати як скорочення з $\varphi \leftrightarrow \chi$, позначається $(\varphi \to \chi )\wedge (\chi \to \varphi )$. Альтернативно, можна додати аксіоми

• ЕКВІВАЛЕНТНІСТЬ 1: $(\varphi \leftrightarrow \chi )\to (\varphi \to \chi )$
• ЕКВІВАЛЕНТНІСТЬ 2: $(\varphi \leftrightarrow \chi )\to (\chi \to \varphi )$
• ЕКВІВАЛЕНТНІСТЬ 3: $(\varphi \to \chi )\to ((\chi \to \varphi )\to (\varphi \leftrightarrow \chi ))$

ЕКВІВАЛЕНТНІСТЬ 1 і ЕКВІВАЛЕНТНІСТЬ 2 можуть при бажанні бути об'єднані в єдину аксіому $(\varphi \leftrightarrow \chi )\to ((\varphi \to \chi )\wedge (\chi \to \varphi ))$, використовуючи з'єднання.

Ставлення до класичної логіки

Система класичної логіки виходить шляхом додавання будь-якої однієї з наступних аксіом:

• $\varphi \vee \mathrm{\neg }\varphi$ (Закон виключеного третього. Може також бути сформульована як $(\varphi \to \chi )\to ((\mathrm{\neg }\varphi \to \chi )\to \chi )$.)
• $\mathrm{\neg }\mathrm{\neg }\varphi \to \varphi$ (Усунення подвійного заперечення)
• $((\varphi \to \chi )\to \varphi )\to \varphi$ (закон Пірса)

У цілому можна взяти як додаткову аксіому будь-яку класичну тавтологію, яка не припустима в двоелементному кадрі Кріпке $\circ ⟶\circ$ (іншими словами, який не включений в Шаблон:Не перекладено).

Інше ставлення визначається Шаблон:Не перекладено, який забезпечує вбудовування класичної логіки першого порядку в інтуїтивну логіку: формула першого порядку доказова в класичній логіці, якщо і лише якщо, переклад Геделя-Гентцена її доводиться інтуїціоністськи. Тому інтуїтивна логіка замість цього може бути розглянута як засіб розширення класичної логіки з конструктивною семантикою. У 1932 Курт Гедель визначив систему логік Геделя, проміжну між класичною логікою та інтуїтивною логікою; такі логіки відомі як Шаблон:Не перекладено.

Невизначеність операторів

У класичній логіці висловлювань можливо взяти одне з кон'юнкції, диз'юнкції або імплікації, як примітивних, і визначити інші два з точки зору їх разом з запереченням, як в трьох аксіомах логіки висловлювань Лукашевича. Навіть можливо визначити всі чотири з точки зору єдиного достатнього оператора, такі як стрілка Пірса (NOR) або штрих Шефера (NAND). Точнісінько так само в класичній логіці першого порядку, один з кванторів може бути визначений з точки зору іншого та заперечення.

Це істотний наслідок закону двозначності, який робить всі такі зв'язки простими булевими функціями. Закон двозначності не міститься в інтуїтивній логіці, лише закон суперечності. Внаслідок жодна з основних зв'язок не може обійтися без цього, і всі вищезгадані аксіоми необхідні. Більшість класичних тотожностей є лише теоремами інтуїтивної логіки в одному напрямку, хоча деякі є теоремами в обох напрямках. Вони такі:

З'єднання порівняно з диз'юнкцією:

• $(\varphi \wedge \psi )\to \mathrm{\neg }(\mathrm{\neg }\varphi \vee \mathrm{\neg }\psi )$
• $(\varphi \vee \psi )\to \mathrm{\neg }(\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$
• $(\mathrm{\neg }\varphi \vee \mathrm{\neg }\psi )\to \mathrm{\neg }(\varphi \wedge \psi )$
• $(\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )\leftrightarrow \mathrm{\neg }(\varphi \vee \psi )$

З'єднання порівняно з імплікацією:

• $(\varphi \wedge \psi )\to \mathrm{\neg }(\varphi \to \mathrm{\neg }\psi )$
• $(\varphi \to \psi )\to \mathrm{\neg }(\varphi \wedge \mathrm{\neg }\psi )$
• $(\varphi \wedge \mathrm{\neg }\psi )\to \mathrm{\neg }(\varphi \to \psi )$
• $(\varphi \to \mathrm{\neg }\psi )\leftrightarrow \mathrm{\neg }(\varphi \wedge \psi )$

Диз'юнкція порівняно з імплікацією:

• $(\varphi \vee \psi )\to (\mathrm{\neg }\varphi \to \psi )$
• $(\mathrm{\neg }\varphi \vee \psi )\to (\varphi \to \psi )$

Універсальна порівняно з екзистенціальною квантифікацією:

• $(\mathrm{\forall }x\varphi (x))\to \mathrm{\neg }(\mathrm{\exists }x\mathrm{\neg }\varphi (x))$
• $(\mathrm{\exists }x\varphi (x))\to \mathrm{\neg }(\mathrm{\forall }x\mathrm{\neg }\varphi (x))$
• $(\mathrm{\exists }x\mathrm{\neg }\varphi (x))\to \mathrm{\neg }(\mathrm{\forall }x\varphi (x))$
• $(\mathrm{\forall }x\mathrm{\neg }\varphi (x))\leftrightarrow \mathrm{\neg }(\mathrm{\exists }x\varphi (x))$

Так, наприклад, "a або b" є сильнішою пропозиціональною формулою, ніж, "якщо не a, то b", тоді як вони класично взаємозамінні. З іншого боку, "не (a або b) «еквівалентно» не a, і також не b". Якщо ми включаємо еквівалентність в список зв'язок, деякі зв'язки стають визначними від інших:

• $(\varphi \leftrightarrow \psi )\leftrightarrow ((\varphi \to \psi )\wedge (\psi \to \varphi ))$
• $(\varphi \to \psi )\leftrightarrow ((\varphi \vee \psi )\leftrightarrow \psi )$
• $(\varphi \to \psi )\leftrightarrow ((\varphi \wedge \psi )\leftrightarrow \varphi )$
• $(\varphi \wedge \psi )\leftrightarrow ((\varphi \to \psi )\leftrightarrow \varphi )$
• $(\varphi \wedge \psi )\leftrightarrow (((\varphi \vee \psi )\leftrightarrow \psi )\leftrightarrow \varphi )$

Зокрема {∨, ↔, ⊥} і {∨, ↔, Є} - повні основи інтуїціоністських зв'язок.

Як показано Олександром Кузнєцовим, одна з таких зв'язок - перша троїчна, друга п'ятерична - окремо є функціонально повними: будь-яка може служити в ролі єдиного достатнього оператора для інтуїціоністської логіки висловлювань, таким чином формуючи аналог штриха Шефера з класичної логіки висловлювань:

• $((p\vee q)\wedge \mathrm{\neg }r)\vee (\mathrm{\neg }p\wedge (q\leftrightarrow r)),$
• $p\to (q\wedge \mathrm{\neg }r\wedge (s\vee t)).$

Семантика

Семантика набагато складніше, ніж для класичного випадку. Теорія моделей може бути задана алгеброю Гейтінга або, еквівалентно, семантикою Кріпке. Нещодавно, подібна теорія моделей Тарського повністю була доведена Шаблон:Не перекладено, але з іншим поняттям повноти, ніж у класичній.

Семантика алгебри Гейтінга

У класичній логіці ми часто обговорюємо значення істинності, які може взяти формула. Зазвичай, обираються значення елементів булевої алгебри. Зустріч та приєднання до операцій в булевій алгебрі, ототожнюються з ∧ і ∨ логічними зв'язками, так, щоб значення формули виду A ∧ B було об'єднанням значення A і значення B в булевій алгебрі. Тоді у нас є корисна теорема, що формула є допустимим судженням класичної логіки, якщо і лише якщо, її значення дорівнює 1 для кожної Шаблон:Не перекладено — тобто для будь-якого привласнення значень до її змінних.

Відповідна теорема вірна для інтуїціоністської логіки, але замість призначення кожній формулі значення з алгебри логіки, використовується значення з гейтінгової алгебри, в якій булева алгебра являє собою особливий випадок. Формула допустима в інтуїтивній логіці, коли вона отримує значення верхнього елемента для будь-якої оцінки в алгебрі Гейтінга. Можна показати, що, щоб розпізнати допустимі формули, достатньо розглянути єдину алгебру Гейтінга, елементи якої є відкритими підмножинами реального рядка R. У цій алгебрі, ∧ і ∨ операції відповідають набору перетину та об'єднання, і значення, присвоєне формулою, A → B є інтервалом (A^C ∪ B), внутрішня частина об'єднання значення B і доповнення значення A. Нижній елемент — порожня множина ∅, і вершина — весь рядок R. Заперечення ¬A формули A (як звичайно), визначено для A → ∅. Значення ¬A тоді зменшується до інтервалу (A^C), внутрішня частина доповнення значення A, також відомого як зовнішній вигляд A. За допомогою цих завдань, інтуїціоністсько-дійсні формули — це якраз ті, які отримують значення всієї лінії.

Наприклад, формула ¬(A ∧ ¬A) справедлива, незалежно від того, що множина Х вибирається як значення формули А, значення ¬(A ∧ ¬A) може бути показано, як вся лінія:

Значення (¬(A ∧ ¬A)) =

інтервал ((Значення (A ∧ ¬A))^C) =

інтервал ((значення (A) ∩ значення (¬A))^C) =

інтервал ((X ∩ інтервал ((значення (A))^C))^C) =

інтервал ((X ∩ інтервал (X^C))^C)

Теорема топології каже нам, що інтервал (X^C) є підмножиною X^C, таким чином, перетин порожній, залишивши:

інтервал (∅^C) = інтервал (R) = R

Таким чином, оцінка цієї формули — істина, і дійсно формула допустима.

Але закон виключеного третього, A ∨ ¬A, як може здатися, є недійсним, дозволяючи значенню A бути {y : y > 0 }. Тоді значення ¬A — мають внутрішню частину {y : y ≤ 0 }, яка є {y : y < 0 }, а значення формули є об'єднанням {y : y > 0 } і {y : y < 0 }, яке є {y : y ≠ 0 }, не всією лінією.

Інтерпретація інтуїціоністської допустимої формули в нескінченній алгебрі Гейтінга описала вище результати у верхньому елементі, представляючи істину, як оцінку формули, незалежно від того, які значення від алгебри присвоєні змінним формули. І навпаки, для кожної недійсної формули, є привласнення значень в змінних, які дають оцінку, відмінну від верхнього елемента. Ні у якій кінцевій алгебрі Гейтінга немає обох цих властивостей.

Семантика Кріпке

Шаблон:Докладніше Покладаючись на його роботу над семантикою модальної логіки, Сол Кріпке створив іншу семантику для інтуїтивної логіки, відомої як семантика Кріпке або реляційна семантика.

Семантика на зразок семантики Тарскі

Було виявлено, що семантика на зразок Тарскі для інтуїтивної логіки не була повністю доведена. Однак Шаблон:Не перекладено показав, що більш слабке поняття повноти все ще міститься для інтуїтивної логіки під подібною моделлю Тарскі. У цьому понятті повноти ми зацікавлені не з усіма операторами, які правильні для кожної моделі, а з операторами, які таким самим чином є істиною в кожній моделі. Тобто, єдиний доказ, що модель оцінює, що формула істинна, повинен бути допустимим для кожної моделі. В цьому випадку, існує не лише доказ повноти, але й той, що діє відповідно до інтуїціоністської логіки.

Ставлення до інших логік

Інтуїтивна логіка пов'язана дуальністю з Шаблон:Не перекладено, відомою як бразильська, антиінтуїціоністська або подвійна інтуїтивна логіка. Підсистема інтуїтивної логіки з віддаленою неправдивою аксіомою відома як мінімальна логіка.

Ставлення до багатозначної логіки

Курт Гедель у 1932 показав, що інтуїтивна логіка не є багатозначною логікою. (Див. розділ під назвою семантика алгебри Гейтінга вище для свого роду "нескінченно багатозначної логіки" інтерпретації інтуїтивної логіки.)

Ставлення до проміжних логік

Будь-яка кінцева алгебра Гейтінга, яка не є еквівалентною булевої алгебри, визначає (семантично) Шаблон:Не перекладено. З іншого боку, законність формул в чистій інтуїтивній логіці не пов'язана з жодною індивідуальною алгеброю Гейтінга, але стосується кожної частини та всієї алгебри Гейтінга одночасно.

Ставлення до модальної логіки

Будь-яка формула інтуїціоністської логіки висловлювань може бути переведена в модальну логічну S4 таким чином:

${\mathrm{\perp }}^{*}$	=	$\mathrm{\perp }$
$A^{*}$	=	$◻A\text{if }A\text{ is prime (a positive literal)}$
$(A\wedge B{)}^{*}$	=	$A^{*}\wedge B^{*}$
$(A\vee B{)}^{*}$	=	$A^{*}\vee B^{*}$
$(A\to B{)}^{*}$	=	$◻(A^{*}\to B^{*})$
$(\mathrm{\neg }A{)}^{*}$	=	$◻(\mathrm{\neg }(A^{*}))\text{since }\mathrm{\neg }A:=A\to \mathrm{\perp }$

і це продемонструвало , що перекладена формула допустима в пропозиціональному модальному логічному S4, якщо і лише якщо, попередньо перекладена формула допустима в IPC. Вищезгаданий набір формул викликається Шаблон:Не перекладено. Є також інтуїціоністська версія модального логічного S4 під назвою Конструктивний Модальний Логічний CS4.

Лямбда-числення

Існує розширений ізоморфізм Каррі — Говарда IPC і Шаблон:Не перекладено.

Див. також

• Конструктивізм (математика)

Джерела

• Dirk van Dalen. Intuitionistic Logic // The Blackwell Guide to Philosophical Logic. / Goble, Lou. — Blackwell, 2001.
• Morten H. Sørensen, Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism. (chapter 2: "Intuitionistic Logic") // Studies in Logic and the Foundations of Mathematics vol. 149. — Elsevier, 2006.
• W. A. Carnielli, A. B.M. Brunner."Anti-intuitionism and paraconsistency" Шаблон:Webarchive// Journal of Applied Logic.— березень, 2005. — Т. 3. — № 1. — С. 161-184.

Посилання

• Joan Moschovakis, Stanford Encyclopedia of Philosophy: "Intuitionistic Logic Шаблон:Webarchive".
• Nick Bezhanishvili, Dick de Jongh, Intuitionistic Logic Шаблон:Webarchive.
• Saul A. Kripke, Semantical Analysis of Intuitionistic Logic I Шаблон:Webarchive.
• Dirk van Dalen, Intuitionistic Logic
• A.S. Troelstra, P. van Ulsen, The discovery of E.W. Beth's semantics for intuitionistic logic Шаблон:Webarchive.
• Anthony J. Bonner, L. Thorne McCarty, Kumar Vadaparty, Expressing Database Queries with Intuitionistic Logic (FTP завантаження одним кліком миші).
• Tableaux'method for intuitionistic logic through S4-translation Шаблон:Webarchive перевіка інтуїціоністської обґрунтованості пропозиціональних формул; забезпечена комп'ютерною лабораторією Гренобля.
• Validity tester for IPC (засноване на Mezhirov's game for IPC) на сайті playmycode.com