Перегляд вихідного коду сторінки Інтуїціоністська логіка

{{Сирий переклад|дата=лютий 2015}}

'''Інтуїтивна логіка''' (інколи '''конструктивна логіка''') — система [[Математична логіка|символічної логіки]], яка відрізняється від [[Класична логіка|класичної логіки]], замінюючи традиційне поняття істини поняттям [[Конструктивне доведення|конструктивно доказової]] істини. Наприклад, у класичній логіці, [[Предикат|пропозиціональні формули]] (предикати) завжди приймають [[значення істинності]] з множини двох тривіальних елементів [[Твердження|тверджень]] <math>\{\top, \bot\}</math> («істина» і «хиба» відповідно) незалежно від того, чи є у нас прямий [[Доказ (логіка)|доказ]] для будь-якого випадку. Навпаки, пропозиціональним формулам (предикатам) в інтуїтивній логіці взагалі ''не'' надається жодного певного значення істинності: натомість вони  вважаються «істинними» ''лише тоді'', коли у нас є ''прямий доказ''. (Замість «формула істинна на основі прямого доказу» можна також сказати, що формула {{Не перекладено|Населена множина|уможливлена||Inhabited set}} доказом у сенсі [[Відповідність Каррі — Говарда|Каррі — Говарда]]). Тому операції в інтуїтивній логіці зберігають {{Не перекладено|Джастифікаціонізм|юстифікацію (виправдання)|ru|Джастификационизм}}, щодо доказу та доказової операції, а не оцінки істини.

Недоведеним твердженням в інтуїтивній логіці не надаються проміжні значення істинності (як іноді помилково стверджується). Справді, можна довести, що у них немає третього значення істинності, що було визначено [[Гливенко Валерій Іванович|Гливенком]] у 1928.<ref>{{Cite web |url=http://plato.stanford.edu/entries/intuitionistic-logic-development/#4.3 |title=Proof that intuitionistic logic has no third truth value, Glivenko 1928 |accessdate=31 жовтня 2014 |archive-date=11 вересня 2018 |archive-url=https://web.archive.org/web/20180911093509/https://plato.stanford.edu/entries/intuitionistic-logic-development/#4.3 }}</ref> Замість цього вони залишаються з невідомим значенням істинності, доти, доки вони або не доведені, або не спростовані. Твердження спростовуються, виводом з них [[протиріччя]].

Наслідком цього погляду є те, що в інтуїтивної логіки немає інтерпретації як двозначної логіки, або навіть як логіки з кінцевим знаком. Попри те, що інтуїтивна логіка зберігає тривіальні судження <math>\{\top, \bot\}</math> наслідувані від класичної логіки, кожен ''доказ'' пропозиціональної формули вважається допустимим пропозиціональним значенням, таким чином, за поняттям твердження {{Не перекладено|Брауер-Гейтінгова-Колмогорова інтерпретація|Гейтінга|en|Brouwer–Heyting–Kolmogorov interpretation}} про множини, пропозиціональні формули (потенційні чи не кінцеві)&nbsp;— це множини особистих доказів.

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

Кілька семантик інтуїтивної логіки було вивчено. Одна семантика відбиває класичну {{Не перекладено|Семантика з булевим знаком|семантику з булевим знаком|en|Algebraic semantics (mathematical logic)}}, але використовує [[Алгебра Гейтінга|алгебру Гейтінга]] замість [[Булева алгебра|булевої алгебри]]. Інша семантика використовує [[Семантика Кріпке|модель Кріпке]].

Інтуїтивна логіка практично корисна, бо її обмеження створюють докази, у яких є {{Не перекладено|Диз'юнкція і властивість існування|властивість існування|en|existence property}}, роблячи її також відповідною для інших форм [[Конструктивна математика|математичного конструктивізму]]. Неофіційно, це означає, що, якщо у Вас є конструктивний доказ того, що об'єкт існує, то Ви можете перетворити цей конструктивний доказ в алгоритм для генерації його прикладу.

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

== Синтаксис ==
[[Файл:Rieger-Nishimura.svg|thumb|right|280px|[[Решітка]] Rieger-Nishimura. Її вузли - пропозиціональні формули в однієї змінної до інтуїціоністської логічної еквівалентності, впорядкованої інтуїціоністською логічною імплікацією.]] 
[[Синтаксис]] формул інтуїтивної логіки подібний [[Числення висловлень|логіці висловлювань]] або [[Логіка першого порядку|логіці першого порядку]]. Проте, інтуїціоністські зв'язки не визначені один з одним таким самим чином, як у [[Класична логіка|класичній логіці]], отже, їх вибір має значення. В інтуїціоністській логіці прийнято використовувати →, ∧, ∨, ⊥ як основні зв'язки, розглядаючи ¬''A'' як скорочення для {{nowrap|(''A'' → ⊥)}}. В інтуїціоністській логіці першого порядку необхідні обидва квантора ∃, ∀.

Багато [[Тавтологія (логіка)|тавтологій]] класичної логіки більше не можуть доводитися в інтуїтивній логіці. Приклади включають не лише [[закон виключеного третього]] {{nowrap|''p'' ∨ ¬''p''}}, але також і [[закон Пірса]] {{nowrap|((''p'' → ''q'') → ''p'') → ''p''}}, і навіть [[Закон подвійного заперечення|усунення подвійного заперечення]]. У класичній логіці і {{nowrap|''p'' → ¬¬''p''}}, і також {{nowrap|¬¬''p'' → ''p''}} є теоремами. В інтуїтивній логіці лише для першого є теорема: подвійне заперечення може бути представлено, але воно не може бути усунуто. Відкидання {{nowrap|''p'' ∨ ¬''p''}} може здаватися дивним для тих, хто більш знайомий з класичною логікою, але доказ цієї пропозиціональної формули в інтуїтивній логіці вимагав би створення доказів для істинності або хибності ''всіх можливих пропозиціональних формул'', які неможливі для ряду причин.

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

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

[[Ґергард Ґенцен]] виявив, що просте обмеження його системи, LK (його подальше обчислення для класичної логіки) приводить до системи, яка є звуковою та сповненою щодо інтуїтивної логіки. Він назвав цю систему LJ. У LK будь-якому числу формул дозволяють з'явитися на стороні укладення наступного; у відмінності LJ дозволяє не більше однієї формули у цій позиції.
Інші похідні LK обмежені інтуїціоністськими похідними, але все ще дозволяють багаторазові укладення в наступному. LJ'<ref>Proof Theory by G. Takeuti, ISBN 0-444-10492-5</ref> є одним з прикладів.

=== Обчислення стилю Гільберта ===
Інтуїтивна логіка може бути визначена, використовуючи наступне обчислення {{Не перекладено|Система Гільберта|стилю Гільберта|en|Hilbert system}}. Це схоже на [[Числення висловлювань|спосіб]] аксіоматизації класичної логіки висловлювань.
У логіці висловлювань правилом висновку є [[modus ponens]].
* MP: від <math>\phi</math> і <math>\phi \to \psi</math> виводять <math>\psi</math>
Аксіоми логіки висловлювань:
* ТОДІ-1: <math>\phi \to (\chi \to \phi )</math>
* ТОДІ-2: <math>(\phi \to (\chi \to \psi )) \to ((\phi \to \chi ) \to (\phi \to \psi ))</math>
* І-1: <math>\phi \land \chi \to \phi </math>
* І-2: <math>\phi \land \chi \to \chi </math>
* І-3: <math>\phi \to (\chi \to (\phi \land \chi ))</math>
* АБО-1: <math>\phi \to \phi \lor \chi </math>
* АБО-2: <math>\chi \to \phi \lor \chi </math>
* АБО-3: <math>(\phi \to \psi ) \to ((\chi \to \psi ) \to (\phi \lor \chi \to \psi ))</math>
* ХИБА: <math>\bot \to \phi </math>
[[Узагальнення|Правила узагальнення]] роблять це системою логіки предикатів першого порядку
* <math>\forall </math>&nbsp;— ГЕНЕРАЛ: від <math>\psi \to \phi </math> виводять <math>\psi \to (\forall x \ \phi )</math>, якщо <math>x</math> не вільний в <math>\psi </math>
<math>\exists </math>&nbsp;— ГЕНЕРАЛ: від <math>\phi \to \psi </math> виводять <math>(\exists x \ \phi ) \to \psi </math>, якщо <math>x</math> не вільний в <math>\psi </math>

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

* PRED-1: <math>(\forall x \ \phi (x)) \to \phi (t)</math>, якщо термін ''t'' вільний для заміни на змінну ''x'' в <math>\phi</math> (тобто, якщо ніяке виникнення якої-небудь змінної в ''t'' не стає пов'язаним в <math>\phi (t)</math>),
* PRED-2: <math>\phi (t) \to (\exists x \ \phi (x))</math>, з тим же обмеженням що стосується PRED-1

==== Додаткові зв'язки ====
===== Заперечення =====

Якщо Ви хочете включати з'єднувальний <math>\lnot </math> для заперечення, а не вважати його скороченням для <math>\phi \to \bot </math>, достатньо додати:
* НЕ-1': <math>(\phi \to \bot ) \to \lnot \phi </math>
* НЕ-2': <math>\lnot \phi \to (\phi \to \bot )</math>
Є багато доступних альтернатив, якщо Ви хочете опустити з'єднувальний <math>\bot </math>(хиба). Наприклад, можна замінити ці три аксіоми ХИБА, НЕ 1 ', і НЕ 2 ' цими двома аксіомами

* НЕ-1: <math>(\phi \to \chi ) \to ((\phi \to \lnot \chi ) \to \lnot \phi )</math>
* НЕ-2: <math>\phi \to (\lnot \phi \to \chi )</math>
як в аксіомах альтернативних числень. Альтернативи НЕ-1 <math>(\phi \to \lnot \chi ) \to (\chi \to \lnot \phi )</math> або <math>(\phi \to \lnot \phi ) \to \lnot \phi </math>.

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

З'єднувальний <math>\leftrightarrow </math> для еквівалентності можна розглядати як скорочення з <math>\phi \leftrightarrow \chi </math>, позначається <math>(\phi \to \chi ) \land (\chi \to \phi )</math>. Альтернативно, можна додати аксіоми
 
* ЕКВІВАЛЕНТНІСТЬ 1: <math>(\phi \leftrightarrow \chi ) \to (\phi \to \chi )</math>
* ЕКВІВАЛЕНТНІСТЬ 2: <math>(\phi \leftrightarrow \chi ) \to (\chi \to \phi )</math>
* ЕКВІВАЛЕНТНІСТЬ 3: <math>(\phi \to \chi ) \to ((\chi \to \phi ) \to (\phi \leftrightarrow \chi ))</math>

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

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

Система класичної логіки виходить шляхом додавання будь-якої однієї з наступних аксіом:
 
* <math>\phi \lor \lnot \phi </math> (Закон виключеного третього. Може також бути сформульована як <math>(\phi \to \chi ) \to ((\lnot \phi \to \chi ) \to \chi )</math>.)
* <math>\lnot \lnot \phi \to \phi </math> (Усунення подвійного заперечення)
* <math>((\phi \to \chi ) \to \phi ) \to \phi </math> (закон Пірса)
У цілому можна взяти як додаткову аксіому будь-яку класичну тавтологію, яка не припустима в двоелементному [[Семантика Кріпке|кадрі Кріпке]] <math>\circ{\longrightarrow}\circ</math> (іншими словами, який не включений в {{Не перекладено|Проміжна логіка|логіку Сметеніча|en|Intermediate logic}}).

Інше ставлення визначається {{Не перекладено|Переклад подвійного заперечення|негативним перекладом Геделя-Гентцена|en|Double-negation translation}}, який забезпечує [[Вкладення|вбудовування]] класичної логіки першого порядку в інтуїтивну логіку: формула першого порядку доказова в класичній логіці, якщо і лише якщо, переклад Геделя-Гентцена її доводиться інтуїціоністськи. Тому інтуїтивна логіка замість цього може бути розглянута як засіб розширення класичної логіки з конструктивною семантикою.
У 1932 [[Курт Гедель]] визначив систему логік Геделя, проміжну між класичною логікою та інтуїтивною логікою; такі логіки відомі як {{Не перекладено|Проміжна логіка|проміжні логіки|en|Intermediate logic}}.

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

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

Це істотний наслідок [[Алгебра логіки|закону двозначності]], який робить всі такі зв'язки простими [[Булева функція|булевими функціями]]. Закон двозначності не міститься в інтуїтивній логіці, лише [[закон суперечності]]. Внаслідок жодна з основних зв'язок не може обійтися без цього, і всі вищезгадані аксіоми необхідні. Більшість класичних тотожностей є лише теоремами інтуїтивної логіки в одному напрямку, хоча деякі є теоремами в обох напрямках. Вони такі:
 
З'єднання порівняно з диз'юнкцією:
* <math>(\phi \wedge \psi) \to \neg (\neg \phi \vee \neg \psi)</math>
* <math>(\phi \vee \psi) \to \neg (\neg \phi \wedge \neg \psi)</math>
* <math>(\neg \phi \vee \neg \psi) \to \neg (\phi \wedge \psi)</math>
* <math>(\neg \phi \wedge \neg \psi) \leftrightarrow \neg (\phi \vee \psi)</math>
З'єднання порівняно з імплікацією:
* <math>(\phi \wedge \psi) \to \neg (\phi \to \neg \psi)</math>
* <math>(\phi \to \psi) \to \neg (\phi \wedge \neg \psi)</math>
* <math>(\phi \wedge \neg \psi) \to \neg (\phi \to \psi)</math>
* <math>(\phi \to \neg \psi) \leftrightarrow \neg (\phi \wedge \psi) </math>
Диз'юнкція порівняно з імплікацією:
* <math>(\phi \vee \psi) \to (\neg \phi \to \psi)</math>
* <math>(\neg \phi \vee \psi) \to (\phi \to \psi)</math>
Універсальна порівняно з екзистенціальною квантифікацією:
* <math>(\forall x \ \phi(x)) \to \neg (\exists x \ \neg \phi(x))</math>
* <math>(\exists x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))</math>
* <math>(\exists x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))</math>
* <math>(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exists x \ \phi(x))</math>

Так, наприклад, "a або b" є сильнішою пропозиціональною формулою, ніж, "якщо не a, то b", тоді як вони класично взаємозамінні. З іншого боку, "не (a або b) «еквівалентно» не a, і також не b".
Якщо ми включаємо еквівалентність в список зв'язок, деякі зв'язки стають визначними від інших:
* <math>(\phi\leftrightarrow \psi) \leftrightarrow ((\phi \to \psi)\land(\psi\to\phi))</math>
* <math>(\phi\to\psi) \leftrightarrow ((\phi\lor\psi) \leftrightarrow \psi)</math>
* <math>(\phi\to\psi) \leftrightarrow ((\phi\land\psi) \leftrightarrow \phi)</math>
* <math>(\phi\land\psi) \leftrightarrow ((\phi\to\psi)\leftrightarrow\phi)</math>
* <math>(\phi\land\psi) \leftrightarrow (((\phi\lor\psi)\leftrightarrow\psi)\leftrightarrow\phi)</math>
Зокрема {∨, ↔, ⊥} і {∨, ↔, Є} - повні основи інтуїціоністських зв'язок.

Як показано Олександром Кузнєцовим, одна з таких зв'язок - перша троїчна, друга п'ятерична - окремо є [[Функціональна повнота|функціонально повними]]: будь-яка може служити в ролі єдиного достатнього оператора для інтуїціоністської логіки висловлювань, таким чином формуючи аналог [[Штрих Шефера|штриха Шефера]] з класичної логіки висловлювань:<ref>Alexander Chagrov, Michael Zakharyaschev, ''Modal Logic'', vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59. ISBN 0-19-853779-4.</ref>
* <math>((p\lor q)\land\neg r)\lor(\neg p\land(q\leftrightarrow r)),</math>
* <math>p\to(q\land\neg r\land(s\lor t)).</math>

== Семантика ==

Семантика набагато складніше, ніж для класичного випадку. [[Теорія моделей]] може бути задана [[Алгебра Гейтінга|алгеброю Гейтінга]] або, еквівалентно, [[Семантика Кріпке|семантикою Кріпке]]. Нещодавно, подібна теорія моделей Тарського повністю була доведена {{Не перекладено|Роберт Лі Констебль|Робертом Констеблем|en|Robert Lee Constable}}, але з іншим поняттям повноти, ніж у класичній.
  
=== Семантика алгебри Гейтінга ===

У класичній логіці ми часто обговорюємо [[значення істинності]], які може взяти формула. Зазвичай, обираються значення елементів [[Булева алгебра|булевої алгебри]]. Зустріч та приєднання до операцій в булевій алгебрі, ототожнюються з ∧ і ∨ логічними зв'язками, так, щоб значення формули виду ''A'' ∧ ''B'' було об'єднанням значення ''A'' і значення ''B'' в булевій алгебрі. Тоді у нас є корисна теорема, що формула є допустимим судженням класичної логіки, якщо і лише якщо, її значення дорівнює 1 для кожної {{Не перекладено|Оцінка (логіка)|оцінки|en|Valuation (logic)}}&nbsp;— тобто для будь-якого привласнення значень до її змінних.

Відповідна теорема вірна для інтуїціоністської логіки, але замість призначення кожній формулі значення з алгебри логіки, використовується значення з [[Алгебра Гейтінга|гейтінгової алгебри]], в якій булева алгебра являє собою особливий випадок. Формула допустима в інтуїтивній логіці, коли вона отримує значення верхнього елемента для будь-якої оцінки в [[Алгебра Гейтінга|алгебрі Гейтінга]].
Можна показати, що, щоб розпізнати допустимі формули, достатньо розглянути єдину алгебру Гейтінга, елементи якої є відкритими підмножинами реального рядка '''R'''.<ref name="S-U">{{cite book | title = Lectures on the Curry-Howard Isomorphism | last = Sørensen | first = Morten Heine B |author2=Paweł Urzyczyn | year = 2006 | publisher = [[Elsevier]] | isbn = 0-444-52077-5 | series = Studies in Logic and the Foundations of Mathematics | page = 42 }}</ref> У цій алгебрі, ∧ і ∨ операції відповідають набору перетину та об'єднання, і значення, присвоєне формулою, ''A'' → ''B'' є інтервалом (''A''<sup>C</sup> ∪ ''B''), [[Внутрішність|внутрішня частина]] об'єднання значення ''B'' і [[Доповнення множин|доповнення]] значення ''A''. Нижній елемент&nbsp;— [[порожня множина]] ∅, і вершина&nbsp;— весь рядок '''R'''. Заперечення ¬''A'' формули ''A'' (як звичайно), визначено для ''A'' → ∅. Значення ¬''A'' тоді зменшується до інтервалу (''A''<sup>C</sup>), внутрішня частина доповнення значення ''A'', також відомого як [[Зовнішність (топологія)|зовнішній вигляд]] ''A''. За допомогою цих завдань, інтуїціоністсько-дійсні формули&nbsp;— це якраз ті, які отримують значення всієї лінії.<ref name="S-U"/>

Наприклад, формула ¬(''A'' ∧ ¬''A'') справедлива, незалежно від того, що множина ''Х'' вибирається як значення формули ''А'', значення ¬(''A'' ∧ ¬''A'') може бути показано, як вся лінія:
 
: Значення (¬(''A'' ∧ ¬''A'')) =
: інтервал ((Значення (''A'' ∧ ¬''A''))<sup>C</sup>) =
: інтервал ((значення (''A'') ∩ значення (¬''A''))<sup>C</sup>) =
: інтервал ((''X'' ∩ інтервал ((значення (''A''))<sup>C</sup>))<sup>C</sup>) =
: інтервал ((''X'' ∩ інтервал (''X''<sup>C</sup>))<sup>C</sup>)

Теорема [[Топологія|топології]] каже нам, що інтервал (''X''<sup>C</sup>) є підмножиною ''X''<sup>C</sup>, таким чином, перетин порожній, залишивши:
 
: інтервал (∅<sup>C</sup>) = інтервал ('''R''') = '''R'''

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

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

[[Інтерпретація (логіка)|Інтерпретація]] інтуїціоністської допустимої формули в нескінченній алгебрі Гейтінга описала вище результати у верхньому елементі, представляючи істину, як оцінку формули, незалежно від того, які значення від алгебри присвоєні змінним формули.<ref name="S-U"/> І навпаки, для кожної недійсної формули, є привласнення значень в змінних, які дають оцінку, відмінну від верхнього елемента.<ref>Alfred Tarski, ''Der Aussagenkalkül und die Topologie'', Fundamenta Mathematicae 31 (1938), 103–134. [http://matwbn.icm.edu.pl/tresc.php?wyd=1&tom=31] {{Webarchive|url=https://web.archive.org/web/20120211140955/http://matwbn.icm.edu.pl/tresc.php?wyd=1&tom=31|date=11 лютого 2012}}</ref><ref name="R-S">{{cite book | title = The Mathematics of Metamathematics | url = https://archive.org/details/mathematicsmetam00rasi_119 | last = Rasiowa | first = Helena |author2=Roman Sikorski | year = 1963 | publisher = Państwowe Wydawn. Naukowe | isbn = | location = Warsaw |series =  Monografie matematyczne | pages = [https://archive.org/details/mathematicsmetam00rasi_119/page/n382 385]–386 }}</ref> Ні у якій кінцевій алгебрі Гейтінга немає обох цих властивостей.<ref name="S-U"/>

=== Семантика Кріпке ===
{{Докладніше|Семантика Кріпке}}
Покладаючись на його роботу над семантикою [[модальна логіка|модальної логіки]], [[Саул Аарон Кріпке|Сол Кріпке]] створив іншу семантику для інтуїтивної логіки, відомої як '''семантика Кріпке''' або '''реляційна семантика'''.<ref name=Mosch-IntLog>[http://plato.stanford.edu/entries/logic-intuitionistic/ Intuitionistic Logic] {{Webarchive|url=https://web.archive.org/web/20210426013615/http://plato.stanford.edu/entries/logic-intuitionistic/ |date=26 квітня 2021 }}. Written by [http://www.math.ucla.edu/~joan/ Joan Moschovakis] {{Webarchive|url=https://web.archive.org/web/20210210234438/http://www.math.ucla.edu/~joan/ |date=10 лютого 2021 }}. Published in Stanford Encyclopedia of Philosophy.</ref>

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

Було виявлено, що  семантика на зразок Тарскі  для інтуїтивної логіки не була повністю доведена. Однак {{Не перекладено|Роберт Лі Констебль|Роберт Констебль|en|Robert Lee Constable}} показав, що більш слабке поняття повноти все ще міститься для інтуїтивної логіки під подібною моделлю Тарскі. У цьому понятті повноти ми зацікавлені не з усіма операторами, які правильні для кожної моделі, а з операторами, які ''таким самим чином'' є істиною в кожній моделі. Тобто, єдиний доказ, що модель оцінює, що формула істинна, повинен бути допустимим для кожної моделі. В цьому випадку, існує не лише доказ повноти, але й той, що діє відповідно до інтуїціоністської логіки.<ref>R. Constable, M. Bickford, ''Intuitionistic completeness of first-order logic'', Annals of Pure and Applied Logic, to appear, {{doi|10.1016/j.apal.2013.07.009}}. Preprint on [http://arxiv.org/abs/1110.1614 ArXiv] {{Webarchive|url=https://web.archive.org/web/20161006082519/https://arxiv.org/abs/1110.1614 |date=6 жовтня 2016 }}.</ref>

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

Інтуїтивна логіка пов'язана [[Дуальність|дуальністю]] з {{Не перекладено|Паранепротирічна логіка|паранепротирічною логікою|en|Paraconsistent logic}}, відомою як ''бразильська'', ''антиінтуїціоністська'' або ''подвійна інтуїтивна логіка''.<ref>{{cite journal | author=Aoyama, Hiroshi | title= LK, LJ, Dual Intuitionistic Logic, and Quantum Logic | journal=Notre Dame Journal of Formal Logic | year=2004 | volume=45 | issue= 4 | pages= 193–213 | url=  | doi=10.1305/ndjfl/1099238445}}</ref>
Підсистема інтуїтивної логіки з віддаленою неправдивою аксіомою відома як [[Числення висловів мінімальне|мінімальна логіка]].

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

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

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

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

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

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

{|
|-
| <math>\bot^*</math>
| =
| &nbsp;&nbsp;<math>\ \bot</math>
|-
| <math>A^*</math>
| =
| &nbsp;&nbsp;<math>\ \Box A \qquad \hbox{if } A \hbox{ is prime (a positive literal)}</math>
|-
| <math>(A \wedge B)^*</math>
| =
| &nbsp;&nbsp;<math>\ A^* \wedge B^*</math>
|-
| <math>(A \vee B)^*</math>
| =
| &nbsp;&nbsp;<math>\ A^* \vee B^*</math>
|-
| <math>(A \rightarrow B)^*</math>
| =
| &nbsp;&nbsp;<math>\ \Box(A^* \rightarrow B^*)</math>
|-
| <math> (\neg A)^*</math>
| =
| &nbsp;&nbsp;<math>\ \Box(\neg (A^*)) \qquad \hbox{since } \neg A := A \rightarrow \bot</math>
|}
і це продемонструвало <ref>Lévy, Michel (2011). [http://teachinglogic.liglab.fr/INT1/S4Lint.pdf ''Logique modale propositionnelle S4 et logique intuitioniste propositionnelle''] {{Webarchive|url=https://web.archive.org/web/20140204042326/http://teachinglogic.liglab.fr/INT1/S4Lint.pdf |date=4 лютого 2014 }}, pp. 4–5.</ref>, що перекладена формула допустима в пропозиціональному модальному логічному S4, якщо і лише якщо, попередньо перекладена формула допустима в IPC. Вищезгаданий набір формул викликається {{Не перекладено|Модальний компаньйон|перекладом Геделя-Маккінзі-Тарського|en|Modal companion}}.
Є також інтуїціоністська версія модального логічного S4 під назвою Конструктивний Модальний Логічний CS4. <ref name=categorical>Natasha Alechina, Michael Mendler, Valeria de Paiva, and Eike Ritter. [http://www.cs.nott.ac.uk/~nza/papers/Alechina++:01a.pdf ''Categorical and Kripke Semantics for Constructive S4 Modal Logic''] {{Webarchive|url=https://web.archive.org/web/20150326212957/http://www.cs.nott.ac.uk/~nza/papers/Alechina++:01a.pdf |date=26 березня 2015 }}</ref>

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

Існує розширений [[Відповідність Каррі — Говарда|ізоморфізм Каррі — Говарда IPC]] і {{Не перекладено|Просто типізоване лямбда-числення|просто типізоване лямбда-числення||Simply typed lambda calculus}}.<ref name=categorical />

== Примітки ==
{{Reflist}}

== Див. також ==
*[[Конструктивізм (математика)]]
== Джерела ==
* 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.[http://dx.doi.org/10.1016/j.jal.2004.07.016 "Anti-intuitionism and paraconsistency"] {{Webarchive|url=https://web.archive.org/web/20081012135757/http://dx.doi.org/10.1016/j.jal.2004.07.016 |date=12 жовтня 2008 }}// Journal of Applied Logic.— березень, 2005. — Т. 3. — № 1. — С. 161-184.

== Посилання ==
* ''Joan Moschovakis'', Stanford Encyclopedia of Philosophy: "[http://plato.stanford.edu/entries/logic-intuitionistic/ Intuitionistic Logic] {{Webarchive|url=https://web.archive.org/web/20210426013615/http://plato.stanford.edu/entries/logic-intuitionistic/ |date=26 квітня 2021 }}".
* ''Nick Bezhanishvili'', ''Dick de Jongh'', [http://www.cs.le.ac.uk/people/nb118/Publications/ESSLLI'05.pdf Intuitionistic Logic] {{Webarchive|url=https://web.archive.org/web/20220122000338/https://www.cs.le.ac.uk/people/nb118/Publications/ESSLLI'05.pdf |date=22 січня 2022 }}.
* ''Saul A. Kripke'', [https://www.princeton.edu/~hhalvors/restricted/kripke_intuitionism.pdf Semantical Analysis of Intuitionistic Logic I] {{Webarchive|url=https://web.archive.org/web/20150222140959/https://www.princeton.edu/~hhalvors/restricted/kripke_intuitionism.pdf |date=22 лютого 2015 }}.
* ''Dirk van Dalen'', [https://web.archive.org/web/20120404002639/http://www.phil.uu.nl/~dvdalen/articles/Blackwell(Dalen).pdf Intuitionistic Logic]
* ''A.S. Troelstra'', ''P. van Ulsen'', [http://www.illc.uva.nl/j50/contribs/troelstra/troelstra.pdf The discovery of E.W. Beth's semantics for intuitionistic logic] {{Webarchive|url=https://web.archive.org/web/20150924033651/http://www.illc.uva.nl/j50/contribs/troelstra/troelstra.pdf |date=24 вересня 2015 }}.
* ''Anthony J. Bonner'', ''L. Thorne McCarty'', ''Kumar Vadaparty'', [ftp://ftp.cs.toronto.edu/pub/bonner/papers/hypotheticals/naclp89.ps Expressing Database Queries with Intuitionistic Logic] (''[[FTP]] завантаження одним кліком миші'').
* [http://teachinglogic.liglab.fr/INT1/index.php Tableaux'method for intuitionistic logic through S4-translation] {{Webarchive|url=https://web.archive.org/web/20160304031141/http://teachinglogic.liglab.fr/INT1/index.php |date=4 березня 2016 }} перевіка інтуїціоністської обґрунтованості пропозиціональних формул; забезпечена комп'ютерною лабораторією [[Гренобль|Гренобля]].
* [https://web.archive.org/web/20150222141235/http://www.playmycode.com/play/game/torusglider/validity-tester-for-ipc Validity tester for IPC] (засноване на [https://web.archive.org/web/20150222141530/http://www.playmycode.com/play/game/torusglider/mezhirovs-game-for-ipc Mezhirov's game for IPC]) на сайті ''playmycode.com''
{{refend}}

{{Некласична логіка}}

[[Категорія:Системи формальної логіки]]
[[Категорія:Логіка в інформатиці]]