Интуиционистская логика

Интуиционистская логика , иногда более широко называемая конструктивной логикой , относится к системам символической логики, которые отличаются от систем, используемых для классической логики , более точным отражением понятия конструктивного доказательства . В частности, системы интуиционистской логики не включают в себя закон исключенного среднего и исключения двойного отрицания , которые являются фундаментальными правилами вывода в классической логике.

Формализованная интуиционистская логика была первоначально разработана Арендом Гейтингом, чтобы обеспечить формальную основу для программы интуиционизма Брауэра . С точки зрения теории доказательств , исчисление Гейтинга является ограничением классической логики, в которой были устранены законы исключенного среднего и двойного отрицания. Исключенное исключение среднего и двойного отрицания все еще может быть доказано для некоторых предложений в каждом конкретном случае, однако, оно не выполняется повсеместно, как в случае с классической логикой.

Были изучены несколько систем семантики интуиционистской логики. Одна из этих семантик отражает классическую булевозначную семантику, но использует алгебры Гейтинга вместо булевых алгебр . Другая семантика использует модели Крипке . Это, однако, технические средства для изучения дедуктивной системы Гейтинга, а не формализации исходных неформальных семантических интуиций Брауэра. Семантические системы , называющих захватить такие интуитивные, из - за предлагая значимые понятия «конструктивной истины» (а не только действительность или доказуемость), являются Гедель «s интерпретация Диалектика , Клини «s реализуемостьЛогика Юрия Медведева конечных задач, ^[1] или Джапаридзе «s вычислимости логика . Однако такая семантика постоянно вызывает логику, более сильную, чем логика Гейтинга. Некоторые авторы утверждали, что это могло быть признаком неадекватности самого исчисления Гейтинга, считая последнее неполным как конструктивную логику. ^[2]

Математический конструктивизм [ править ]

В семантике классической логики пропозициональным формулам присваиваются значения истинности из двухэлементного набора («истина» и «ложь» соответственно), независимо от того, есть ли у нас прямые доказательства для любого случая. Это называется «законом исключенного третьего», потому что он исключает возможность любого значения истинности, кроме «истинного» или «ложного». В отличие от пропозициональных формул в интуиционистской логике не присваивается определенное значение истинности и только считается «истинным» , когда у нас есть прямые доказательства, следовательно , доказательство . (Мы также можем сказать, что вместо того, чтобы формула предложения была "истинной" благодаря прямым свидетельствам,что он населен доказательством в${\ displaystyle \ {\ top, \ bot \}}$Смысл Карри-Ховарда .) Операции в интуиционистской логике, таким образом, сохраняют обоснование в отношении свидетельств и доказуемости, а не оценки истинности.

Интуиционистская логика - широко используемый инструмент при разработке подходов к конструктивизму в математике. Использование конструктивистской логики в целом было спорной темой среди математиков и философов (см., Например, полемику Брауэра – Гильберта ). Распространенным возражением против их использования является процитированное выше отсутствие двух центральных правил классической логики, закона исключенного среднего и исключения двойного отрицания. Они считаются настолько важными для математической практики, что Дэвид Гильбертписал о них: «Принятие принципа исключенного среднего из математика было бы тем же самым, что, скажем, запретить телескоп астроному или боксеру использовать свои кулаки. Запретить утверждения о существовании и принцип исключенного среднего равносильно к полному отказу от математики ". ^[3]

Несмотря на серьезные проблемы, связанные с неспособностью использовать ценные правила исключения исключенного среднего и двойного отрицания, интуиционистская логика имеет практическое применение. Одна из причин этого заключается в том, что его ограничения производят доказательства, обладающие свойством существования , что делает его также пригодным для других форм математического конструктивизма . Неформально это означает, что если есть конструктивное доказательство того, что объект существует, это конструктивное доказательство может быть использовано в качестве алгоритма для создания примера этого объекта, принцип, известный как соответствие Карри – Ховарда.между доказательствами и алгоритмами. Одна из причин, по которой этот конкретный аспект интуиционистской логики так ценен, заключается в том, что он позволяет практикам использовать широкий спектр компьютеризированных инструментов, известных как помощники по доказательству . Эти инструменты помогают своим пользователям в проверке (и создании ) крупномасштабных доказательств, размер которых обычно исключает обычную человеческую проверку, которая осуществляется при публикации и рецензировании математических доказательств. Таким образом, использование помощников доказательства (таких как Agda или Coq) позволяет современным математикам и логикам разрабатывать и доказывать чрезвычайно сложные системы, помимо тех, которые можно создать и проверить исключительно вручную. Одним из примеров доказательства, которое невозможно было удовлетворительно проверить без формальной проверки, является знаменитое доказательство теоремы о четырех цветах . Эта теорема ставила математиков в тупик более чем на сто лет, пока не было разработано доказательство, которое исключало большие классы возможных контрпримеров, но все же оставляло достаточно открытых возможностей, и для завершения доказательства потребовалась компьютерная программа. Это доказательство было спорным в течение некоторого времени, но позже оно было проверено с помощью Coq.

Синтаксис [ править ]

Синтаксис формул интуиционистской логики аналогична логике высказываний или логики первого порядка . Однако интуиционистские связки не поддаются определению в терминах друг друга так же, как в классической логике , поэтому их выбор имеет значение. В интуиционистской логике высказываний (IPL) принято использовать →, ∧, ∨, ⊥ в качестве основных связок, трактуя ¬ A как сокращение для ( A → ⊥) . В интуиционистской логике первого порядка необходимы оба квантора ∃, ∀.

Слабее классической логики [ править ]

Интуиционистскую логику можно понимать как ослабление классической логики, означающее, что она более консервативна в том, что позволяет рассуждающему делать выводы, но не допускает никаких новых выводов, которые не могли быть сделаны в рамках классической логики. Каждая теорема интуиционистской логики - это теорема классической логики, но не наоборот. Многие тавтологии в классической логике не являются теоремами в интуиционистской логике - в частности, как было сказано выше, одна из главных целей интуиционистской логики состоит в том, чтобы не утверждать закон исключенного третьего, чтобы свести на нет использование неконструктивного доказательства противоречием., который может использоваться для предоставления утверждений о существовании без предоставления явных примеров объектов, которые он доказывает. Мы говорим «не подтверждать», потому что, хотя это не обязательно верно, что закон соблюдается в любом контексте, нельзя привести никакого контрпримера: такой контрпример был бы выводом (предполагающим отрицание закона для определенного утверждения), недопустимым согласно классическим правилам. логика и, следовательно, не допускается в строгом ослаблении, как интуиционистская логика. Действительно, двойное отрицание закона сохраняется как тавтология системы: то есть это теорема, которая независимо от предложения .${\ Displaystyle \ neg [\ neg (P \ vee \ neg P)]}$${\ displaystyle P}$

Последовательное исчисление [ править ]

Герхард Генцен обнаружил, что простое ограничение его системы LK (его секвенциальное исчисление для классической логики) приводит к системе, которая является надежной и полной по отношению к интуиционистской логике. Он назвал эту систему ЖЖ. В LK разрешено использовать любое количество формул в конце секвенции; в отличие от этого LJ допускает не более одной формулы в этой позиции.

Другие производные от LK ограничиваются интуиционистскими выводами, но все же позволяют делать несколько выводов подряд. LJ ' ^[4] является одним из примеров.

Исчисление в стиле Гильберта [ править ]

Интуиционистскую логику можно определить с помощью следующего исчисления в стиле Гильберта . Это похоже на способ аксиоматизации классической логики высказываний.

В логике высказываний правилом вывода является modus ponens.

• МП: от и вывести${\ displaystyle \ phi}$${\ displaystyle \ phi \ to \ psi}$${\displaystyle \psi }$

и аксиомы

• ТО-1: ${\displaystyle \phi \to (\chi \to \phi )}$
• ТО-2: ${\displaystyle (\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))}$
• И-1: ${\displaystyle \phi \land \chi \to \phi }$
• И-2: ${\displaystyle \phi \land \chi \to \chi }$
• И-3: ${\displaystyle \phi \to (\chi \to (\phi \land \chi ))}$
• ИЛИ-1: ${\displaystyle \phi \to \phi \lor \chi }$
• ИЛИ-2: ${\displaystyle \chi \to \phi \lor \chi }$
• ИЛИ-3: ${\displaystyle (\phi \to \psi )\to ((\chi \to \psi )\to ((\phi \lor \chi )\to \psi ))}$
• ЛОЖНЫЙ: ${\displaystyle \bot \to \phi }$

Чтобы сделать это системой логики предикатов первого порядка, правила обобщения

• ${\displaystyle \forall }$-GEN: из логического вывода , если не свободен в${\displaystyle \psi \to \phi }$${\displaystyle \psi \to (\forall x\ \phi )}$${\displaystyle x}$${\displaystyle \psi }$
• ${\displaystyle \exists }$-GEN: из логического вывода , если не свободен в${\displaystyle \phi \to \psi }$${\displaystyle (\exists x\ \phi )\to \psi }$${\displaystyle x}$${\displaystyle \psi }$

добавляются вместе с аксиомами

• PRED-1:, если термин t свободен для подстановки переменной x в (т. Е. Если никакое вхождение какой-либо переменной в t не становится связанным )${\displaystyle (\forall x\ \phi (x))\to \phi (t)}$${\displaystyle \phi }$${\displaystyle \phi (t)}$
• ПРЕД-2:, с тем же ограничением, что и для ПРЕД-1${\displaystyle \phi (t)\to (\exists x\ \phi (x))}$

Необязательные связки [ править ]

Отрицание [ править ]

Если кто-то желает включить связку для отрицания, а не рассматривать ее как сокращение , достаточно добавить:${\displaystyle \lnot }$${\displaystyle \phi \to \bot }$

• НЕ-1 ': ${\displaystyle (\phi \to \bot )\to \lnot \phi }$
• НЕ-2 ': ${\displaystyle \lnot \phi \to (\phi \to \bot )}$

Если кто-то хочет опустить связку (ложь) , существует ряд альтернатив . Например, можно заменить три аксиомы ЛОЖЬ, НЕ-1 'и НЕ-2' двумя аксиомами${\displaystyle \bot }$

• НЕ-1: ${\displaystyle (\phi \to \chi )\to ((\phi \to \lnot \chi )\to \lnot \phi )}$
• НЕ-2: ${\displaystyle \phi \to (\lnot \phi \to \chi )}$

как в исчислении высказываний § Аксиомы . Альтернативами НЕ-1 являются или .${\displaystyle (\phi \to \lnot \chi )\to (\chi \to \lnot \phi )}$${\displaystyle (\phi \to \lnot \phi )\to \lnot \phi }$

Эквивалентность [ править ]

Соединительно эквивалентности может рассматриваться как аббревиатура, с стоять в течение . В качестве альтернативы можно добавить аксиомы${\displaystyle \leftrightarrow }$${\displaystyle \phi \leftrightarrow \chi }$${\displaystyle (\phi \to \chi )\land (\chi \to \phi )}$

• МКФ-1: ${\displaystyle (\phi \leftrightarrow \chi )\to (\phi \to \chi )}$
• МКФ-2: ${\displaystyle (\phi \leftrightarrow \chi )\to (\chi \to \phi )}$
• МКФ-3: ${\displaystyle (\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))}$

IFF-1 и IFF-2 при желании можно объединить в единую аксиому с помощью конъюнкции.${\displaystyle (\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))}$

Отношение к классической логике [ править ]

Система классической логики получается добавлением любой из следующих аксиом:

• ${\displaystyle \phi \lor \lnot \phi }$(Закон исключенной середины. Также можно сформулировать как .)${\displaystyle (\phi \to \chi )\to ((\lnot \phi \to \chi )\to \chi )}$
• ${\displaystyle \lnot \lnot \phi \to \phi }$ (Устранение двойного отрицания)
• ${\displaystyle ((\phi \to \chi )\to \phi )\to \phi }$( Закон Пирса )
• ${\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}$ (Закон противопоставления)

В общем, в качестве дополнительной аксиомы можно принять любую классическую тавтологию, которая не верна в двухэлементной системе отсчета Крипке (другими словами, она не входит в логику Сметанича ).${\displaystyle \circ {\longrightarrow }\circ }$

Другое отношение задается отрицательным переводом Гёделя – Генцена , который обеспечивает вложение классической логики первого порядка в интуиционистскую логику: формула первого порядка доказуема в классической логике тогда и только тогда, когда ее перевод Геделя-Генцена доказуем интуиционистски. Следовательно, интуиционистскую логику вместо этого можно рассматривать как средство расширения классической логики конструктивной семантикой.

В 1932 году Курт Гёдель определил систему логики, промежуточную между классической и интуиционистской логикой; Логики Гёделя одновременно известны как промежуточные логики .

Неопределимость операторов [ править ]

В классической логике высказываний, можно взять одну из совокупности , дизъюнкции , или косвенно , как примитивные, и определить два других с точки зрения его вместе с отрицанием , например, в Лукасевич «s трех аксиом логики . Можно даже определить все четыре в терминах единственного достаточного оператора, такого как стрелка Пирса (NOR) или штрих Шеффера (NAND). Точно так же в классической логике первого порядка один из кванторов может быть определен в терминах другого и отрицания.

По сути, это следствия закона бивалентности , который делает все такие связки просто булевыми функциями . В интуиционистской логике не требуется соблюдения закона бивалентности, только закон непротиворечивости . В результате нельзя обойтись без основных связок, и все вышеперечисленные аксиомы необходимы. Большинство классических тождеств - это только теоремы интуиционистской логики в одном направлении, хотя некоторые - теоремы в обоих направлениях. Вот они:

Конъюнкция против дизъюнкции:

• ${\displaystyle (\phi \wedge \psi )\to \neg (\neg \phi \vee \neg \psi )}$
• ${\displaystyle (\phi \vee \psi )\to \neg (\neg \phi \wedge \neg \psi )}$
• ${\displaystyle (\neg \phi \vee \neg \psi )\to \neg (\phi \wedge \psi )}$
• ${\displaystyle (\neg \phi \wedge \neg \psi )\leftrightarrow \neg (\phi \vee \psi )}$

Соединение против импликации:

• ${\displaystyle (\phi \wedge \psi )\to \neg (\phi \to \neg \psi )}$
• ${\displaystyle (\phi \to \psi )\to \neg (\phi \wedge \neg \psi )}$
• ${\displaystyle (\phi \wedge \neg \psi )\to \neg (\phi \to \psi )}$
• ${\displaystyle (\phi \to \neg \psi )\leftrightarrow \neg (\phi \wedge \psi )}$

Дизъюнкция против импликации:

• ${\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}$
• ${\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}$

Универсальная и экзистенциальная количественная оценка:

• ${\displaystyle (\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))}$
• ${\displaystyle (\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))}$
• ${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))}$
• ${\displaystyle (\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))}$

Так, например, «a или b» - более сильная пропозициональная формула, чем «если не a, то b», тогда как они классически взаимозаменяемы. С другой стороны, «не (а или б)» эквивалентно «не а, а также не б».

Если мы включим эквивалентность в список связок, некоторые из связок станут определяемыми из других:

• ${\displaystyle (\phi \leftrightarrow \psi )\leftrightarrow ((\phi \to \psi )\land (\psi \to \phi ))}$
• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )}$
• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )}$
• ${\displaystyle (\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )}$
• ${\displaystyle (\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )}$

В частности, {∨, ↔, ⊥} и {∨, ↔, ¬} являются полными базами интуиционистских связок.

Как показал Александр В. Кузнецов, любая из следующих связок - первая тернарная, вторая - пятеричная - сама по себе является функционально полной : любой из них может выполнять роль единственного достаточного оператора для интуиционистской логики высказываний, образуя аналог от инсульта Шеффера от классической логики: ^[5]

• ${\displaystyle ((p\lor q)\land \neg r)\lor (\neg p\land (q\leftrightarrow r)),}$
• ${\displaystyle p\to (q\land \neg r\land (s\lor t)).}$

Семантика [ править ]

Семантика несколько сложнее, чем в классическом случае. Теория моделей может быть дана алгебрами Гейтинга или, что то же самое, семантикой Крипке . Недавно Боб Констебл доказал полноту теории модели, подобной Тарскому , но с другим понятием полноты, чем в классическом.

Недоказанным утверждениям в интуиционистской логике не придается промежуточное значение истинности (как иногда ошибочно утверждают). Можно доказать, что такие утверждения не имеют третьей ценности истинности, результат восходит к Гливенко в 1928 году. ^[6] Вместо этого они сохраняют неизвестную ценность истинности, пока они не будут либо доказаны, либо опровергнуты. Утверждения опровергаются путем вывода из них противоречия.

Следствием этой точки зрения является то, что интуиционистская логика не имеет интерпретации ни как двузначная логика, ни даже как конечно-значная логика в привычном смысле. Хотя интуиционистская логика сохраняет тривиальные утверждения классической логики, каждое доказательство пропозициональной формулы считается действительной пропозициональной ценностью, таким образом, в соответствии с понятием Гейтинга пропозиций-как-множеств, пропозициональные формулы являются (потенциально не конечными) наборами своих доказательств.${\displaystyle \{\top ,\bot \}}$

Семантика алгебры Гейтинга [ править ]

В классической логике мы часто обсуждаем значения истинности, которые может принимать формула. Значения обычно выбираются как члены булевой алгебры . Встречается и присоединиться к операции в булевой алгебре идентифицируется с ∧ и ∨ логическими связками, так что значение формулы вида ∧ B является пересечением стоимости A и значения B в булевой алгебре. Тогда у нас есть полезная теорема о том, что формула является действительным утверждением классической логики тогда и только тогда, когда ее значение равно 1 для каждой оценки, то есть для любого присвоения значений ее переменным.

Соответствующая теорема верна для интуиционистской логики, но вместо присвоения каждой формуле значения из булевой алгебры используются значения из алгебры Гейтинга , особым случаем которой являются булевы алгебры. Формула действительна в интуиционистской логике тогда и только тогда, когда она получает значение верхнего элемента для любой оценки любой алгебры Гейтинга.

Можно показать , что признать действительные формулы, достаточно рассмотреть один Гейтингова алгебру, элементы которой являются открытыми подмножествами вещественной прямой R . ^[7] В этой алгебре мы имеем:

${\displaystyle {\begin{aligned}{\text{Value}}[\bot ]&=\emptyset \\{\text{Value}}[\top ]&=\mathbf {R} \\{\text{Value}}[A\land B]&={\text{Value}}[A]\cap {\text{Value}}[B]\\{\text{Value}}[A\lor B]&={\text{Value}}[A]\cup {\text{Value}}[B]\\{\text{Value}}[A\to B]&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup {\text{Value}}[B]\right)\end{aligned}}}$

где Int ( X ) является внутренность из X и X ^∁ его дополнения .

Последнее тождество относительно A → B позволяет вычислить значение ¬ A :

${\displaystyle {\begin{aligned}{\text{Value}}[\neg A]&={\text{Value}}[A\to \bot ]\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup {\text{Value}}[\bot ]\right)\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup \emptyset \right)\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\right)\end{aligned}}}$

При таких присвоениях интуиционистски верные формулы - это именно те формулы, которым присваивается значение всей строки. ^[7] Например, формула ¬ ( A ∧ ¬ A ) действительна, потому что независимо от того, какой набор X выбран в качестве значения формулы A , значение ¬ ( A ∧ ¬ A ) может быть показано как вся строка:

${\displaystyle {\begin{aligned}{\text{Value}}[\neg (A\land \neg A)]&={\text{int}}\left({\text{Value}}[A\land \neg A]^{\complement }\right)&&{\text{Value}}[\neg B]={\text{int}}\left({\text{Value}}[B]^{\complement }\right)\\&={\text{int}}\left(\left({\text{Value}}[A]\cap {\text{Value}}[\neg A]\right)^{\complement }\right)\\&={\text{int}}\left(\left({\text{Value}}[A]\cap {\text{int}}\left({\text{Value}}[A]^{\complement }\right)\right)^{\complement }\right)\\&={\text{int}}\left(\left(X\cap {\text{int}}\left(X^{\complement }\right)\right)^{\complement }\right)\\&={\text{int}}\left(\emptyset ^{\complement }\right)&&{\text{int}}\left(X^{\complement }\right)\subseteq X^{\complement }\\&={\text{int}}(\mathbf {R} )\\&=\mathbf {R} \end{aligned}}}$

Таким образом, оценка этой формулы верна, и формула действительно действительна. Но можно показать, что закон исключенного среднего, A ∨ ¬ A , недействителен, если использовать конкретное значение набора положительных действительных чисел для A :

${\displaystyle {\begin{aligned}{\text{Value}}[A\lor \neg A]&={\text{Value}}[A]\cup {\text{Value}}[\neg A]\\&={\text{Value}}[A]\cup {\text{int}}\left({\text{Value}}[A]^{\complement }\right)&&{\text{Value}}[\neg B]={\text{int}}\left({\text{Value}}[B]^{\complement }\right)\\&=\{x>0\}\cup {\text{int}}\left(\{x>0\}^{\complement }\right)\\&=\{x>0\}\cup {\text{int}}\left(\{x\leqslant 0\}\right)\\&=\{x>0\}\cup \{x<0\}\\&=\{x\neq 0\}\\&\neq \mathbf {R} \end{aligned}}}$

Интерпретация любых действительных интуиционистский формулы в бесконечной алгебре гейтинговой описана выше , приводит в верхнем элементе, представляющая правда, в качестве оценки формулы, независимо от того, каких значений из алгебры присваивается переменной формула. ^[7] И наоборот, для каждой недопустимой формулы существует присвоение значений переменным, что дает оценку, отличную от верхнего элемента. ^{[8] [9]} Никакая конечная алгебра Гейтинга не обладает вторым из этих двух свойств. ^[7]

Семантика Крипке [ править ]

Основываясь на своей работе по семантике модальной логики , Сол Крипке создал другую семантику для интуиционистской логики, известную как семантика Крипке или реляционная семантика. ^[10]

Семантика типа Тарского [ править ]

Было обнаружено, что семантика, подобная Тарскому, для интуиционистской логики не может быть доказана полной. Однако Роберт Констебл показал, что более слабое понятие полноты все еще справедливо для интуиционистской логики в рамках модели, подобной Тарскому. В этом понятии полноты нас интересуют не все утверждения, которые верны для каждой модели, а утверждения, которые одинаково верны для каждой модели. То есть одно доказательство того, что модель считает формулу истинной, должно быть действительным для каждой модели. В этом случае есть не только доказательство полноты, но и такое, которое действительно согласно интуиционистской логике. ^[11]

Отношение к другой логике [ править ]

Интуиционистская логика связана двойственностью с паранепротиворечивой логикой, известной как бразильская , антиинтуиционистская или двойная интуиционистская логика . ^[12]

Подсистема интуиционистской логики с удаленной аксиомой ЛОЖЬ известна как минимальная логика .

Отношение к многозначной логике [ править ]

Работа Курта Гёделя , связанная с многозначной логикой, показала в 1932 году, что интуиционистская логика не является конечнозначной логикой . ^[13] (См. Раздел « Семантика алгебры Гейтинга» выше, где представлена бесконечнозначная логическая интерпретация интуиционистской логики.)

Отношение к промежуточной логике [ править ]

Любая конечная алгебра Гейтинга, не эквивалентная булевой алгебре, определяет (семантически) промежуточную логику . С другой стороны, валидность формул в чистой интуиционистской логике не привязана к какой-либо отдельной алгебре Гейтинга, но относится к любой и всем алгебрам Гейтинга одновременно.

Отношение к модальной логике [ править ]

Любая формула интуиционистской логики высказываний (IPC) может быть переведена в нормальную модальную логику S4 следующим образом:

${\displaystyle {\begin{aligned}\bot ^{*}&=\bot \\A^{*}&=\Box 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)^{*}&=\Box \left(A^{*}\to B^{*}\right)\\(\neg A)^{*}&=\Box (\neg (A^{*}))&&\neg A:=A\to \bot \end{aligned}}}$

и было продемонстрировано ^[14], что переведенная формула действительна в пропозициональной модальной логике S4 тогда и только тогда, когда исходная формула действительна в IPC. Приведенный выше набор формул называется переводом Гёделя – МакКинси – Тарского .

Существует также интуиционистская версия модальной логики S4, называемая конструктивной модальной логикой CS4. ^[15]

Лямбда-исчисление [ править ]

Существует расширенный изоморфизм Карри – Ховарда между IPC и просто типизированным лямбда-исчислением . ^[15]

См. Также [ править ]

• Толкование BHK
• Логика вычислимости
• Конструктивное доказательство
• Переписка Карри – Ховарда
• Семантика игры
• Жилой комплекс
• Промежуточная логика
• Интуиционистская теория типов
• Семантика Крипке
• Линейная логика
• Паранепротиворечивая логика
• Теория релевантности
• Гладкий анализ бесконечно малых

Заметки [ править ]

Ссылки [ править ]

Внешние ссылки [ править ]

• Стэнфордская энциклопедия философии : « Интуиционистская логика » Джоан Московакис
• Интуиционистская логика Ника Бежанишвили и Дика де Йонга (из Института логики, языка и вычислений Амстердамского университета )
• Семантический анализ интуиционистской логики I Сола А. Крипке из Гарвардского университета, Кембридж, Массачусетс, США
• Интуиционистской логики от Дирка ван Дален
• Открытие семантики Э. В. Бет для интуиционистской логики А. С. Трельстра и П. ван Ульсеном
• Выражение запросов к базе данных с помощью интуиционистской логики Энтони Дж. Боннера. Л. Торн Маккарти. Кумар Вадапарти. Университет Рутгерса, факультет компьютерных наук
• Табличный метод интуиционистской логики посредством S4-трансляции проверяет интуиционистскую валидность пропозициональных формул; предоставлено Laboratoire d'Informatique de Grenoble
• Оксфордский справочник по философии математики и логики : «Интуиционизм в математике» Дэвида Чарльза Маккарти