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

Различные системы символической логики

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

Формализованная интуиционистская логика была первоначально разработана Арендом Гейтингом для предоставления формальной основы для программы интуиционизма LEJ Brouwer . С точки зрения теории доказательств исчисление Гейтинга является ограничением классической логики, в которой были удалены закон исключенного третьего и исключение двойного отрицания. Однако исключенное третье и исключение двойного отрицания все еще могут быть доказаны для некоторых предложений в каждом конкретном случае, но не выполняются универсально, как в классической логике. Стандартным объяснением интуиционистской логики является интерпретация BHK . ^[1]

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

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

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

Интуиционистская логика — это широко используемый инструмент в разработке подходов к конструктивизму в математике. Использование конструктивистской логики в целом было спорной темой среди математиков и философов (см., например, спор Брауэра–Гильберта ). Распространенным возражением против их использования является вышеупомянутое отсутствие двух центральных правил классической логики, закона исключенного третьего и исключения двойного отрицания. Дэвид Гильберт считал их настолько важными для практики математики, что писал:

«Отнять принцип исключенного третьего у математика было бы то же самое, что, скажем, запретить астроному пользоваться телескопом или боксёру пользоваться кулаками. Запретить утверждения о существовании и принцип исключенного третьего равносильно полному отказу от науки математики». ^[4]

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

Синтаксис

Решетка Ригера–Нишимуры. Ее узлы — пропозициональные формулы от одной переменной с точностью до интуиционистской логической эквивалентности , упорядоченные интуиционистской логической импликацией.

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

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

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

В пропозициональной логике правило вывода — modus ponens

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

и аксиомы таковы

• ТОГДА-1: ${\displaystyle \psi \to (\phi \to \psi )}$
• ТОГДА-2: ${\displaystyle {\big (}\chi \to (\phi \to \psi ){\big )}\to {\big (}(\chi \to \phi )\to (\chi \to \psi ){\big )}}$
• И-1: ${\displaystyle \phi \land \chi \to \phi }$
• И-2: ${\displaystyle \phi \land \chi \to \chi }$
• И-3: ${\displaystyle \phi \to {\big (}\chi \to (\phi \land \chi ){\big )}}$
• ИЛИ-1: ${\displaystyle \phi \to \phi \lor \chi }$
• ИЛИ-2: ${\displaystyle \chi \to \phi \lor \chi }$
• ИЛИ-3: ${\displaystyle (\phi \to \psi )\to {\Big (}(\chi \to \psi )\to {\big (}(\phi \lor \chi )\to \psi ){\Big )}}$
• ЛОЖЬ: ${\displaystyle \bot \to \phi }$

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

• ${\displaystyle \forall }$-GEN: из infer , если не является свободным в ${\displaystyle \psi \to \phi }$ ${\displaystyle \psi \to (\forall x\ \phi )}$ ${\displaystyle x}$ ${\displaystyle \psi }$
• ${\displaystyle \exists }$-GEN: из infer , если не является свободным в ${\displaystyle \phi \to \psi }$ ${\displaystyle (\exists x\ \phi )\to \psi }$ ${\displaystyle x}$ ${\displaystyle \psi }$

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

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

Отрицание

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

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

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

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

как в Исчислении высказываний § Аксиомы . Альтернативами NOT-1 являются или . ${\displaystyle (\phi \to \neg \chi )\to (\chi \to \neg \phi )}$ ${\displaystyle (\phi \to \neg \phi )\to \neg \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 ))}$

Последовательное исчисление

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

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

Теоремы

Теоремы чистой логики — это утверждения, доказуемые из аксиом и правил вывода. Например, использование THEN-1 в THEN-2 сводит его к . Формальное доказательство последнего с использованием системы Гильберта приведено на этой странице. При , это, в свою очередь, подразумевает . Другими словами: «Если из того, что имеет место, следует, что абсурдно, то если имеет место, то получается, что это не так». Благодаря симметрии утверждения фактически получено ${\displaystyle {\big (}\chi \to (\phi \to \psi ){\big )}\to {\big (}\phi \to (\chi \to \psi ){\big )}}$ ${\displaystyle \bot }$ ${\displaystyle \psi }$ ${\displaystyle (\chi \to \neg \phi )\to (\phi \to \neg \chi )}$ ${\displaystyle \chi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \chi }$

${\displaystyle (\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )}$

При объяснении теорем интуиционистской логики в терминах классической логики это можно понимать как ее ослабление: она более консервативна в том, что она позволяет рассуждающему делать выводы, не допуская при этом никаких новых выводов, которые не могли бы быть сделаны в рамках классической логики. Каждая теорема интуиционистской логики является теоремой в классической логике, но не наоборот. Многие тавтологии в классической логике не являются теоремами в интуиционистской логике — в частности, как сказано выше, одна из главных целей интуиционистской логики состоит в том, чтобы не утверждать закон исключенного третьего, чтобы испортить использование неконструктивного доказательства от противного , которое может быть использовано для предоставления утверждений о существовании без предоставления явных примеров объектов, существование которых оно доказывает.

Двойные отрицания

Двойное отрицание не подтверждает закон исключенного третьего (PEM); хотя PEM не обязательно соблюдается в любом контексте, контрпример также не может быть приведен. Такой контрпример был бы выводом (выводом отрицания закона для определенного предложения), запрещенным в классической логике, и, таким образом, PEM не допускается в строгом ослаблении, подобном интуиционистской логике. Формально, это простая теорема, что для любых двух предложений. Рассматривая любое установленное как ложное, это действительно показывает, что двойное отрицание закона сохраняется как тавтология уже в минимальной логике . И теперь, поскольку установлено, что оно противоречиво, исключенное третье даже не будет доказуемо для всех дизъюнкций исключенного третьего. И это также означает, что исчисление высказываний всегда совместимо с классической логикой. ${\displaystyle {\big (}(\psi \lor (\psi \to \varphi ))\to \varphi {\big )}\leftrightarrow \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \neg \neg (\psi \lor \neg \psi )}$ ${\displaystyle \neg (\psi \lor \neg \psi )}$

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

Двойное отрицание и импликация

Подобно вышесказанному, из modus ponens в форме следует . Связь между ними всегда можно использовать для получения новых формул: Ослабленная предпосылка приводит к сильному следствию, и наоборот. Например, обратите внимание, что если выполняется, то выполняется , но схема в другом направлении будет подразумевать принцип исключения двойного отрицания. Предложения, для которых возможно исключение двойного отрицания, также называются устойчивыми . Интуиционистская логика доказывает устойчивость только для ограниченных типов предложений. Формула, для которой выполняется исключенное среднее, может быть доказана устойчивой с помощью дизъюнктивного силлогизма , который более подробно обсуждается ниже. Обратное, однако, не выполняется в общем случае, если только рассматриваемое исключенное среднее утверждение само по себе не является устойчивым. ${\displaystyle \psi \to ((\psi \to \varphi )\to \varphi )}$ ${\displaystyle \psi \to \neg \neg \psi }$ ${\displaystyle (\neg \neg \psi )\to \phi }$ ${\displaystyle \psi \to \phi }$

Можно доказать, что импликация эквивалентна , независимо от предложений. В качестве особого случая следует, что предложения отрицаемой формы ( здесь) являются стабильными, т.е. всегда действительны. ${\displaystyle \psi \to \neg \phi }$ ${\displaystyle \neg \neg \psi \to \neg \phi }$ ${\displaystyle \psi =\neg \phi }$ ${\displaystyle \neg \neg \neg \phi \to \neg \phi }$

В общем, сильнее, чем , что сильнее, чем , что само по себе подразумевает три эквивалентных утверждения , и . Используя дизъюнктивный силлогизм, предыдущие четыре действительно эквивалентны. Это также дает интуиционистски обоснованный вывод , поскольку он, таким образом, эквивалентен тождеству . ${\displaystyle \neg \neg \psi \to \phi }$ ${\displaystyle \psi \to \phi }$ ${\displaystyle \neg \neg (\psi \to \phi )}$ ${\displaystyle \psi \to (\neg \neg \phi )}$ ${\displaystyle (\neg \neg \psi )\to (\neg \neg \phi )}$ ${\displaystyle \neg \phi \to \neg \psi }$ ${\displaystyle \neg \neg (\neg \neg \phi \to \phi )}$

Когда выражает утверждение, то его двойное отрицание просто выражает утверждение, что опровержение было бы непоследовательным. Доказав такое простое двойное отрицание, оно также все еще помогает отрицать другие утверждения посредством введения отрицания , как тогда . Экзистенциальное утверждение с двойным отрицанием не обозначает существование сущности со свойством, а скорее абсурдность предполагаемого несуществования любой такой сущности. Также все принципы в следующем разделе, включающие квантификаторы, объясняют использование импликаций с гипотетическим существованием в качестве предпосылки. ${\displaystyle \psi }$ ${\displaystyle \neg \neg \psi }$ ${\displaystyle \psi }$ ${\displaystyle (\phi \to \neg \psi )\to \neg \phi }$

Формула перевода

Ослабление утверждений путем добавления двух отрицаний перед кванторами существования (и атомами) также является основным шагом в переводе с двойным отрицанием . Он представляет собой вложение классической логики первого порядка в интуиционистскую логику: формула первого порядка доказуема в классической логике тогда и только тогда, когда ее перевод Гёделя–Гентцена доказуем интуиционистски. Например, любая теорема классической пропозициональной логики формы имеет доказательство, состоящее из интуиционистского доказательства с последующим одним применением устранения двойного отрицания. Таким образом, интуиционистскую логику можно рассматривать как средство расширения классической логики с конструктивной семантикой. ${\displaystyle \psi \to \phi }$ ${\displaystyle \psi \to \neg \neg \phi }$

Невзаимоопределяемость операторов

Уже минимальная логика легко доказывает следующие теоремы, связывающие конъюнкцию и дизъюнкцию с импликацией с использованием отрицания :

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

${\displaystyle (\phi \lor \psi )\to (\neg \phi \to \neg \neg \psi )}$, ослабленный вариант разделительного силлогизма

соотв.

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

${\displaystyle (\phi \land \psi )\to \neg (\phi \to \neg \psi )}$и аналогично ${\displaystyle (\phi \to \psi )\to \neg (\phi \land \neg \psi )}$

Действительно, более сильные варианты этих выражений все еще сохраняются — например, антецеденты могут быть дважды отрицаемы, как отмечено, или все могут быть заменены на на сторонах антецедентов, как будет обсуждаться. Однако ни одно из этих пяти импликаций не может быть отменено без немедленного подразумевания исключенного третьего (рассмотреть для ) соответственно устранения двойного отрицания (рассмотреть истинное ). Следовательно, левые стороны не составляют возможного определения правых сторон. ${\displaystyle \psi }$ ${\displaystyle \neg \neg \psi }$ ${\displaystyle \neg \psi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$

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

Экзистенциальная и универсальная квантификация

Во-первых, когда в предложении не является свободным , то ${\displaystyle x}$ ${\displaystyle \varphi }$

${\displaystyle {\big (}\exists x\,(\phi (x)\to \varphi ){\big )}\,\,\to \,\,{\Big (}{\big (}\forall x\ \phi (x){\big )}\to \varphi {\Big )}}$

Когда область дискурса пуста, то по принципу взрыва экзистенциальное утверждение подразумевает что угодно. Когда область содержит по крайней мере один термин, то, предполагая исключенное третье для , обратное вышеуказанному импликации становится также доказуемо, то есть две стороны становятся эквивалентными. Это обратное направление эквивалентно парадоксу пьющего (DP). Более того, его экзистенциальный и дуальный вариант задается принципом независимости предпосылок (IP). Классически, приведенное выше утверждение, кроме того, эквивалентно более дизъюнктивной форме, обсуждаемой далее ниже. Однако конструктивно утверждения о существовании, как правило, труднее найти. ${\displaystyle \forall x\,\phi (x)}$

Если область дискурса не пуста и, более того, независима от , такие принципы эквивалентны формулам в исчислении высказываний. Здесь формула тогда просто выражает тождество . Это каррированная форма modus ponens , которая в особом случае с как ложным высказыванием приводит к закону принципа непротиворечивости . ${\displaystyle \phi }$ ${\displaystyle x}$ ${\displaystyle (\phi \to \varphi )\to (\phi \to \varphi )}$ ${\displaystyle ((\phi \to \varphi )\land \phi )\to \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \neg (\phi \land \neg \phi )}$

Рассмотрение ложного предложения для первоначального вывода приводит к важному ${\displaystyle \varphi }$

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

Другими словами: «Если существует сущность , не обладающая свойством , то опровергается следующее : Каждая сущность обладает свойством ». ${\displaystyle x}$ ${\displaystyle \phi }$ ${\displaystyle \phi }$

Квантификаторная формула с отрицаниями также немедленно следует из принципа непротиворечивости, выведенного выше, каждый пример которого сам по себе уже следует из более частного . Чтобы вывести противоречие, заданное , достаточно установить его отрицание (в отличие от более сильного ), и это делает доказательство двойных отрицаний также ценным. К тому же, исходная квантификаторная формула на самом деле все еще верна с ослаблением до . И поэтому, на самом деле, верна более сильная теорема: ${\displaystyle \neg (\neg \neg \phi \land \neg \phi )}$ ${\displaystyle \neg \phi }$ ${\displaystyle \neg \neg \phi }$ ${\displaystyle \phi }$ ${\displaystyle \forall x\ \phi (x)}$ ${\displaystyle \forall x{\big (}(\phi (x)\to \varphi )\to \varphi {\big )}}$

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

Другими словами: «Если существует сущность, не обладающая свойством , то опровергается следующее : для каждой сущности невозможно доказать , что она не обладает свойством ». ${\displaystyle x}$ ${\displaystyle \phi }$ ${\displaystyle \phi }$

Во-вторых,

${\displaystyle {\big (}\forall x\,(\phi (x)\to \varphi ){\big )}\,\,\leftrightarrow \,\,{\big (}(\exists x\ \phi (x))\to \varphi {\big )}}$

где применяются аналогичные соображения. Здесь экзистенциальная часть всегда является гипотезой, и это эквивалентность. Рассматривая частный случай снова,

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

Доказанное преобразование можно использовать для получения двух дополнительных следствий: ${\displaystyle (\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )}$

${\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 (\forall x\,\neg \phi (x))\to \neg (\exists x\,\neg \neg \phi (x))}$ ${\displaystyle \to }$

Имеются более общие варианты. Включая предикат и каррирование, следующее обобщение также влечет за собой связь между импликацией и конъюнкцией в исчислении предикатов, обсуждаемом ниже. ${\displaystyle \psi }$

${\displaystyle {\big (}\forall x\ \phi (x)\to (\psi (x)\to \varphi ){\big )}\,\,\leftrightarrow \,\,{\Big (}{\big (}\exists x\ \phi (x)\land \psi (x){\big )}\to \varphi {\Big )}}$

Если предикат решительно ложен для всех , то эта эквивалентность тривиальна. Если решительно истинен для всех , схема просто сводится к ранее заявленной эквивалентности. На языке классов и частный случай этой эквивалентности с ложью уравнивает две характеристики непересекаемости : ${\displaystyle \psi }$ ${\displaystyle x}$ ${\displaystyle \psi }$ ${\displaystyle x}$ ${\displaystyle A=\{x\mid \phi (x)\}}$ ${\displaystyle B=\{x\mid \psi (x)\}}$ ${\displaystyle \varphi }$ ${\displaystyle A\cap B=\emptyset }$

${\displaystyle \forall (x\in A).x\notin B\,\,\leftrightarrow \,\,\neg \exists (x\in A).x\in B}$

Дизъюнкция против конъюнкции

Существуют конечные вариации формул квантификаторов, содержащие всего два предложения:

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

Первый принцип не может быть отменен: рассмотрение для подразумевало бы слабое исключенное третье, т. е. утверждение . Но интуиционистская логика сама по себе даже не доказывает . Так, в частности, не существует принципа дистрибутивности для отрицаний, выводящих утверждение из . Для неформального примера конструктивного прочтения рассмотрим следующее: из неопровержимого доказательства того, что не было случая, когда и Алиса, и Боб явились на свою дату, нельзя вывести неопровержимое доказательство, связанное с любым из двух лиц, что этот человек не явился. Отрицаемые предложения сравнительно слабы, в том смысле, что классически действительный закон Де Моргана , допускающий дизъюнкцию из единственной отрицательной гипотезы, автоматически не выполняется конструктивно. Интуиционистское пропозициональное исчисление и некоторые из его расширений вместо этого демонстрируют свойство дизъюнкции , подразумевая, что один из дизъюнктов любой дизъюнкции по отдельности также должен быть выводим. ${\displaystyle \neg \psi }$ ${\displaystyle \phi }$ ${\displaystyle \neg \psi \lor \neg \neg \psi }$ ${\displaystyle \neg \psi \lor \neg \neg \psi \lor (\neg \neg \psi \to \psi )}$ ${\displaystyle \neg \phi \lor \neg \psi }$ ${\displaystyle \neg (\phi \land \psi )}$

Обратные варианты этих двух и эквивалентные варианты с дважды отрицаемыми антецедентами уже были упомянуты выше. Импликации к отрицанию конъюнкции часто можно доказать непосредственно из принципа непротиворечия. Таким образом можно также получить смешанную форму импликаций, например . Конкатенируя теоремы, мы также находим ${\displaystyle (\neg \phi \lor \psi )\to \neg (\phi \land \neg \psi )}$

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

Обратное доказать невозможно, поскольку это доказывало бы слабость принципа исключенного третьего.

В логике предикатов принцип постоянной области недействителен: не подразумевает более сильного . Однако распределительные свойства выполняются для любого конечного числа предложений. О варианте закона Де Моргана относительно двух экзистенциально замкнутых разрешимых предикатов см. LLPO . ${\displaystyle \forall x{\big (}\varphi \lor \psi (x){\big )}}$ ${\displaystyle \varphi \lor \forall x\,\psi (x)}$

Союз против импликации

Из общей эквивалентности следует также импорт-экспорт , выражающий несовместимость двух предикатов с помощью двух различных связок:

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

Из-за симметрии конъюнктивной связки это снова подразумевает уже установленное . Формула эквивалентности для отрицаемой конъюнкции может быть понята как частный случай каррирования и декаррирования. Еще много соображений относительно двойных отрицаний снова применимы. И обе необратимые теоремы, связывающие конъюнкцию и импликацию, упомянутые во введении, следуют из этой эквивалентности. Одна из них является обратной и выполняется просто потому, что сильнее, чем . ${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$ ${\displaystyle (\phi \to \psi )\to \neg (\phi \land \neg \psi )}$ ${\displaystyle \phi \to \psi }$ ${\displaystyle \phi \to \neg \neg \psi }$

Теперь при использовании принципа из следующего раздела справедлив также его следующий вариант с большим количеством отрицаний слева:

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

Следствием этого является то, что

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

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

Уже минимальная логика доказывает, что исключенное среднее эквивалентно consequentia mirabilis , примеру закона Пирса . Теперь сродни modus ponens, очевидно, уже в минимальной логике, которая является теоремой, даже не включающей отрицания. В классической логике эта импликация на самом деле является эквивалентностью. Принимая форму , исключенное среднее вместе с взрывом, как видно, влечет за собой закон Пирса. ${\displaystyle (\phi \lor \psi )\to ((\phi \to \psi )\to \psi )}$ ${\displaystyle \phi }$ ${\displaystyle \psi \to \varphi }$

В интуиционистской логике получаются варианты указанной теоремы, включающие , следующим образом. Во-первых, отметим, что две различные формулы для упомянутого выше могут быть использованы для того, чтобы подразумевать . Последние являются формами дизъюнктивного силлогизма для отрицаемых предложений, . Усиленная форма все еще имеет место в интуиционистской логике: ${\displaystyle \bot }$ ${\displaystyle \neg (\phi \land \psi )}$ ${\displaystyle (\neg \phi \vee \neg \psi )\to (\phi \to \neg \psi )}$ ${\displaystyle \neg \psi }$

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

Как и в предыдущих разделах, позиции и могут быть изменены, что дает более сильный принцип, чем тот, который упомянут во введении. Так, например, интуиционистски "Или или " является более сильной пропозициональной формулой, чем "Если не , то ", тогда как они классически взаимозаменяемы. Импликация, как правило, не может быть изменена на противоположную, поскольку это немедленно подразумевает исключенное третье. ${\displaystyle \neg \phi }$ ${\displaystyle \phi }$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$

Непротиворечивость и взрыв вместе также доказывают более сильный вариант . И это показывает, как исключенное среднее для подразумевает устранение двойного отрицания для него. Для фиксированного это следствие, как правило, не может быть обращено. (Однако, как всегда конструктивно верно, отсюда следует, что предположение об устранении двойного отрицания для всех таких дизъюнкций также подразумевает классическую логику.) ${\displaystyle (\neg \phi \lor \psi )\to (\neg \neg \phi \to \psi )}$ ${\displaystyle \psi }$ ${\displaystyle \psi }$ ${\displaystyle \neg \neg (\psi \lor \neg \psi )}$

Конечно, формулы, установленные здесь, могут быть объединены для получения еще большего количества вариаций. Например, дизъюнктивный силлогизм, представленный как обобщение,

${\displaystyle {\Big (}{\big (}\exists x\ \neg \phi (x){\big )}\lor \varphi {\Big )}\,\,\to \,\,{\Big (}{\big (}\forall x\ \phi (x){\big )}\to \varphi {\Big )}}$

Если какой-либо термин вообще существует, то антецедент здесь даже подразумевает , что в свою очередь само по себе также подразумевает заключение здесь (это снова самая первая формула, упомянутая в этом разделе). ${\displaystyle \exists x{\big (}\phi (x)\to \varphi {\big )}}$

Основная часть обсуждения в этих разделах применима точно так же и к минимальной логике. Но что касается дизъюнктивного силлогизма с общим , минимальная логика может в лучшем случае доказать , где обозначает . Вывод здесь можно упростить только до использования взрыва. ${\displaystyle \psi }$ ${\displaystyle (\neg \phi \lor \psi )\to (\neg \neg \phi \to \psi ')}$ ${\displaystyle \psi '}$ ${\displaystyle \neg \neg \psi \land (\psi \lor \neg \psi )}$ ${\displaystyle \psi }$

Эквивалентности

Приведенные выше списки также содержат эквивалентности. Эквивалентность, включающая конъюнкцию и дизъюнкцию, вытекает из того, что она на самом деле сильнее, чем . Обе стороны эквивалентности можно понимать как конъюнкции независимых импликаций. Выше абсурдность используется для . В функциональных интерпретациях она соответствует конструкциям с условием if . Так, например, «Not ( or )» эквивалентно «Not , and also not ». ${\displaystyle (P\lor Q)\to R}$ ${\displaystyle P\to R}$ ${\displaystyle \bot }$ ${\displaystyle R}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$

Эквивалентность сама по себе обычно определяется как конъюнкция ( ) импликаций ( ) и эквивалентна ей следующим образом: ${\displaystyle \land }$ ${\displaystyle \to }$

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

С его помощью такие связки в свою очередь становятся определяемыми из него:

• ${\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 )}$

В свою очередь, и являются полными базами интуиционистских связок, например. ${\displaystyle \{\lor ,\leftrightarrow ,\bot \}}$ ${\displaystyle \{\land ,\leftrightarrow ,\neg \}}$

Функционально полные связки

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

• ${\displaystyle {\big (}(P\lor Q)\land \neg R{\big )}\lor {\big (}\neg P\land (Q\leftrightarrow R){\big )}}$
• ${\displaystyle P\to {\big (}Q\land \neg R\land (S\lor T){\big )}}$

Семантика

Семантика несколько сложнее, чем в классическом случае. Модельная теория может быть задана алгебрами Гейтинга или, что эквивалентно, семантикой Крипке . В 2014 году модельная теория Тарского-подобная была доказана Бобом Констеблем как полная , но с другим понятием полноты, чем в классическом случае. ^[8]

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

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

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

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

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

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

${\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}}}$

При таких назначениях интуиционистски верными формулами являются именно те, которым присвоено значение всей строки. ^[9] Например, формула ¬( 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}}}$

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

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

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

Семантика, подобная Тарскому

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

Металоджик

Допустимые правила

В интуиционистской логике или фиксированной теории, использующей логику, может возникнуть ситуация, когда импликация всегда сохраняется метатеоретически, но не в языке. Например, в чистом пропозициональном исчислении, если is доказуемо, то so is . Другой пример — то, что быть доказуемым всегда означает, что so is . Говорят, что система закрыта относительно этих импликаций как правил , и они могут быть приняты. ${\displaystyle (\neg A)\to (B\lor C)}$ ${\displaystyle (\neg A\to B)\lor (\neg A\to C)}$ ${\displaystyle (A\to B)\to (A\lor C)}$ ${\displaystyle {\big (}(A\to B)\to A{\big )}\lor {\big (}(A\to B)\to C{\big )}}$

Отношение к другим логикам

Паранепротиворечивая логика

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

Подсистема интуиционистской логики с удаленной аксиомой ЛОЖЬ (соответственно НЕ-2) известна как минимальная логика , и некоторые различия были подробно рассмотрены выше.

Промежуточные логики

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

Так, например, для схемы, не включающей отрицания, рассмотрим классически допустимую . Принятие этой интуиционистской логики дает промежуточную логику, называемую логикой Гёделя-Даммета. ${\displaystyle (A\to B)\lor (B\to A)}$

Отношение к классической логике

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

• ${\displaystyle \phi \lor \neg \phi }$(Закон исключенного третьего)
• ${\displaystyle \neg \neg \phi \to \phi }$(Устранение двойного отрицания)
• ${\displaystyle (\neg \phi \to \phi )\to \phi }$( Consequentia mirabilis , см. также закон Пирса )

Существуют также различные переформулировки или формулировки в виде схем с двумя переменными (например, закон Пирса). Одна из них примечательна — это (обратный) закон противопоставления

• ${\displaystyle (\neg \phi \to \neg \chi )\to (\chi \to \phi )}$

Они подробно описаны в статье по промежуточной логике .

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

Многозначная логика

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

Модальная логика

Любая формула интуиционистской пропозициональной логики (ИПЛ) может быть переведена на язык нормальной модальной логики 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}}}$

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

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

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

Смотрите также

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

• Философский портал

Примечания

1. Van Atten 2022.
2. Шехтман 1990.
3. Джапаридзе 2009.
4. Ван Хейеноорт : Гильберт (1927), стр.476
5. Бежанишвили и Де Йонг, с. 8.
6. Такеути 2013.
7. Чагров и Захарьящев 1997, стр. 58–59.
8. Констебль и Бикфорд 2014.
9. Sørensen & Urzyczyn 2006, с. 42.
10. Тарский 1938.
11. Расёва и Сикорски 1963, стр. 385–386.
12. Крипке 1965.
13. Мошовакис 2022.
14. Аояма 2004.
15. Берджесс 2014.
16. Леви 2011, стр. 4–5.
17. Алечина и др. 2003.

Ссылки

• Алечина, Наташа; Мендлер, Михаэль; Де Пайва, Валерия ; Риттер, Эйке (январь 2003 г.). Категориальная и Крипке-семантика для конструктивной модальной логики S4 (PDF) . Труды 15-го международного семинара по логике компьютерных наук. Конспект лекций по информатике . doi :10.1007/3-540-44802-0_21.
• Аояма, Хироши (2004). «LK, LJ, Двойственная интуиционистская логика и квантовая логика». Notre Dame Journal of Formal Logic . 45 (4): 193–213. doi : 10.1305/ndjfl/1099238445 .
• Бежанишвили, Ник; Де Йонг, Дик. «Интуиционистская логика» (PDF) . Амстердамский университет (Институт логики, языка и вычислений).
• Бруннер, АБМ; Карниелли, Уолтер (март 2005 г.). «Антиинтуиционизм и паранепротиворечивость». Журнал прикладной логики . 3 (1): 161–184. doi : 10.1016/j.jal.2004.07.016 .
• Берджесс, Джон (январь 2014 г.). «Интуиции трех видов во взглядах Гёделя на континуум» (PDF) . doi :10.1017/CBO9780511756306.002 (неактивен 2024-06-04).{{cite web}}: CS1 maint: DOI inactive as of June 2024 (link)
• Чагров, Александр; Захарьящев, Михаил (1997). Модальная логика . Oxford Logic Guides. Том 35. Oxford University Press . С. XV, 605. ISBN 0-19-853779-4.
• Констебль, Р.; Бикфорд, М. (2014). «Интуиционистская полнота логики первого порядка». Annals of Pure and Applied Logic . 165 : 164–198. arXiv : 1110.1614 . doi : 10.1016/j.apal.2013.07.009. S2CID  849930.
• Ван Дален, Дирк (2001). «Интуиционистская логика». В Goble, Lou (ред.). The Blackwell Guide to Philosophical Logic . Нью-Йорк: Blackwell Publishing . стр. 224–257. doi :10.1002/9781405164801.ch11. ISBN 9780631206934.
• Хейтинг, Аренд (1930). Die formalen Regeln der intuitionistischen Logik I, II, III . Sitzungsberichte der preussischen Akademie der Wissenschaften (на немецком языке). стр. 42–56, 57–71, 158–169. В трех частях
• Джапаридзе, Георгий (январь 2009). «В начале была игровая семантика?». В Majer, O.; Pietarinen, A.-V.; Tulenheimo, T. (ред.). Игры: унификация логики, языка и философии. Том 15. Springer . С. 249–350. arXiv : cs/0507045 . doi :10.1007/978-1-4020-9374-6_11. ISBN 978-1-4020-9373-9.
• Крипке, Саул А. (1965). "Семантический анализ интуиционистской логики I" (PDF) . В Crossley, JN; Dummett, MAE (ред.). Формальные системы и рекурсивные функции. Труды Восьмого логического коллоквиума Оксфорд, июль 1963 г. Исследования по логике и основаниям математики. Том 40. Амстердам: North-Holland Publishing Company . стр. 92–130. doi :10.1016/S0049-237X(08)71685-9. ISBN 9780444534057.
• Леви, Мишель (29 апреля 2011 г.), Logique modale propositionnelle S4 et logique intuitioniste propositionnelle (PDF) (на французском языке)
• Расёва, Хелена; Сикорский, Роман (1963). Математика метаматематики . Математическая монография. Варшава: Państwowe Wydawn. Наукове. п. 519.
• Шехтман, Валентин (1990). «Модальные аналоги логики Медведева конечных задач не являются конечно аксиоматизируемыми». Studia Logica . 49 (3): 365–385. doi :10.1007/BF00370370.
• Sørensen, Morten H.; Urzyczyn, Paweł (2006). "глава 2: Интуиционистская логика". Лекции об изоморфизме Карри-Ховарда . Исследования по логике и основаниям математики. Том 149 (1-е изд.). Амстердам: Elsevier . ISBN 978-0-444-52077-7.
• Takeuti, Gaisi (2013) [1975]. Теория доказательств (Второе издание). Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-49073-1.
• Тарский, Альфред (1938). «Der Aussagenkalkül und die Topologie». Фундамента Математика . 31 : 103–134. дои : 10.1007/BF00370370.
• Troelstra, AS; Van Ulsen, P. "Открытие семантики EW Beth для интуиционистской логики" (PDF) . Институт логики, языка и вычислений (ILLC). Амстердамский университет.

Внешние ссылки

• Ван Аттен, Марк (4 мая 2022 г.). «Развитие интуиционистской логики». В Zalta, Edward N. (ред.). Стэнфордская энциклопедия философии .

• Маккарти, Дэвид Чарльз (2009). «Интуиционизм в математике». В Шапиро, Стюарт (ред.). Оксфордский справочник по философии математики и логики . стр. 356–386. doi :10.1093/oxfordhb/9780195325928.003.0010. ISBN 978-0-19-532592-8.

• Мошовакис, Джоан (16 декабря 2022 г.). «Интуиционистская логика». В Zalta, Edward N. (ред.). Стэнфордская энциклопедия философии .

• «Метод таблиц для интуиционистской логики через S4-перевод». Лаборатория информатики в Гренобле . проверяет интуиционистскую валидность пропозициональных формул