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

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

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

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

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

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

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

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

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

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

Синтаксис

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

Синтаксис формул интуиционистской логики аналогичен логике высказываний или логике первого порядка . Однако интуиционистские связки не поддаются определению друг через друга так же, как в классической логике , поэтому их выбор имеет значение. В интуиционистской логике высказываний (IPL) принято использовать →, ∧, ∨, ⊥ в качестве основных связок, рассматривая ¬ 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: из вывода , если несвободен в ${\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: , если термин свободен для замены переменной в (т. е. если ни одно появление какой-либо переменной в не становится связанным в ) ${\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 )}$

Существует несколько альтернатив, если кто-то хочет опустить связку (ложь). Например, можно заменить три аксиомы ЛОЖЬ, НЕ-1' и НЕ-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' ^[6] является одним из примеров.

Теоремы

Теоремы чистой логики — это утверждения, доказуемые с помощью аксиом и правил вывода. Например, использование THEN-1 в THEN-2 уменьшает его до . Формальное доказательство последнего с использованием системы Гильберта приведено на этой странице. С for это, в свою очередь, подразумевает . Другими словами: «Если это обстоятельство подразумевает, что это абсурдно, то если оно действительно так, то это не так». Ввиду симметрии утверждения фактически получено ${\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 )}$

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

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

Он просто «не подтверждает» закон исключенного третьего, поскольку, хотя закон не обязательно соблюдается в любом контексте, контрпример также не может быть приведен. Таким контрпримером был бы вывод (выводящий об отрицании закона для определенного предложения), запрещенный классической логикой и, следовательно, недопустимый в строгом ослаблении, таком как интуиционистская логика. Формально это простая теорема, справедливая для любых двух предложений. Считая любое установленное ложным, это действительно показывает, что двойное отрицание закона сохраняется как тавтология уже в минимальной логике . Таким образом, исчисление высказываний всегда совместимо с классической логикой. Если предположить, что закон подразумевает суждение, то, дважды применяя противопоставление и используя дважды отрицаемое исключенное третье, можно доказать дважды отрицаемые варианты различных строго классических тавтологий. Ситуация более сложная для формул логики предикатов, когда некоторые количественные выражения отрицаются. ${\displaystyle {\big (}(\psi \lor (\psi \to \varphi ))\to \varphi {\big )}\leftrightarrow \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \neg \neg (\psi \lor \neg \psi )}$

Аналогично вышеизложенному, из modus ponens в форме следует . Связь между ними всегда можно использовать для получения новых формул: ослабленная посылка приводит к сильному импликации, и наоборот. Например, обратите внимание, что если выполняется, то и , но схема в другом направлении будет подразумевать принцип исключения двойного отрицания. Предложения, для которых возможно устранение двойного отрицания, также называются устойчивыми. Интуиционистская логика доказывает стабильность только для ограниченных типов высказываний, например высказываний отрицаемой формы. Формула, для которой исключены средние значения, может быть доказана устойчивой с помощью дизъюнктивного силлогизма , который более подробно обсуждается ниже. Обратное, однако, в общем случае неверно, если только рассматриваемое исключенное среднее утверждение не является устойчивым само по себе. Даже слабее, чем is , что само по себе подразумевает три эквивалентных утверждения , и . Используя дизъюнктивный силлогизм, предыдущие четыре действительно эквивалентны. Это также дает интуиционистски действительный вывод , поскольку, таким образом, он эквивалентен тождеству . ${\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 \phi }$ ${\displaystyle \neg \neg (\psi \to \phi )}$ ${\displaystyle \psi \to (\neg \neg \phi )}$ ${\displaystyle \neg \phi \to \neg \psi }$ ${\displaystyle (\neg \neg \psi )\to (\neg \neg \phi )}$ ${\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 )}$

Действительно, более сильные их варианты, например, с заменой all на на предшествующих сторонах, все еще остаются в силе, как будет обсуждаться. Однако ни одно из этих пяти последствий не может быть изменено без немедленного исключения среднего (рассмотрим для ) соответственно. исключение двойного отрицания (считайте true ). Следовательно, левые части не являются возможным определением правых частей. ${\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). При этом экзистенциальный и двойственный его вариант задается принципом независимости предпосылки (ИП). Более того, в классическом понимании приведенное выше утверждение эквивалентно более дизъюнктивной форме, обсуждаемой ниже. Однако с конструктивной точки зрения утверждения о существовании обычно труднее найти. ${\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 \neg \phi \land \neg \neg \psi )\to \neg (\neg \phi \lor \neg \psi )}$ ${\displaystyle (\neg \phi \lor \psi )\to \neg (\phi \land \neg \psi )}$ ${\displaystyle (\neg \phi \land \psi )\to \neg (\phi \lor \neg \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 )}$

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

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

Сродни modus ponens, явно уже в минимальной логике, и эта теорема даже не предполагает отрицаний. Классически это эквивалентность. В интуиционистской логике варианты с участием получаются следующим образом. Во-первых, обратите внимание, что для подразумевания можно использовать две разные формулы, упомянутые выше . Последние представляют собой формы разделительного силлогизма для отрицаемых суждений . Усиленная форма все еще сохраняется в интуиционистской логике: ${\displaystyle (\phi \lor \psi )\to ((\phi \to \psi )\to \psi )}$ ${\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 \phi }$ ${\displaystyle \neg \neg \phi }$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$

Рассмотрение вместо в приведенной выше форме силлогизма показывает, как исключенное среднее подразумевает исключение двойного отрицания. ${\displaystyle \neg \neg \psi }$ ${\displaystyle \phi }$

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

${\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-предложения . Так, например, «Не ( или )» эквивалентно «Не , а также не ». ${\displaystyle (P\lor Q)\to R}$ ${\displaystyle P\to R}$ ${\displaystyle \bot }$ ${\displaystyle R}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$

Сама эквивалентность обычно определяется как комбинация импликаций, а затем эквивалентна ей.

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

Семантика

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Металогика

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

В интуиционистской логике или фиксированной теории, использующей логику, может возникнуть ситуация, когда импликация всегда сохраняется метатеоретически, но не в языке. Например, в чистом исчислении высказываний, если доказуемо, то доказуемо и . Другой пример: то, что доказуемость всегда означает, что это так и есть . Кто-то говорит, что система закрыта в соответствии с этими последствиями как правила , и они могут быть приняты. ${\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 (\phi \to \chi )\to ((\neg \phi \to \chi )\to \chi )}$
• ${\displaystyle \neg \neg \phi \to \phi }$(Устранение двойного отрицания)
• ${\displaystyle ((\phi \to \chi )\to \phi )\to \phi }$( закон Пирса )
• ${\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]

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

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

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

Примечания

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

Рекомендации

• Алечина, Наташа; Мендлер, Майкл; Де Пайва, Валерия ; Риттер, Эйке (январь 2003 г.). Категориальная семантика и семантика Крипке для конструктивной модальной логики S4 (PDF) . Материалы 15-го международного семинара по логике информатики. Конспекты лекций по информатике . дои : 10.1007/3-540-44802-0_21.

• Аояма, Хироши (2004). «LK, LJ, двойная интуиционистская логика и квантовая логика». Журнал формальной логики Нотр-Дама . 45 (4): 193–213. дои : 10.1305/ndjfl/1099238445 .

• Бежанишвили, Ник; Де Йонг, Дик. «Интуиционистская логика» (PDF) . Амстердамский университет (Институт логики, языка и вычислений).

• Бруннер, ПРО; Карниелли, Уолтер (март 2005 г.). «Антиинтуиционизм и паранепротиворечивость». Журнал прикладной логики . 3 (1): 161–184. дои : 10.1016/j.jal.2004.07.016 .

• Берджесс, Джон (январь 2014 г.). «Три вида интуиции во взглядах Гёделя на континуум» (PDF) . дои : 10.1017/CBO9780511756306.002.

• Чагров, Александр; Захарьящев, Михаил (1997). Модальная логика . Оксфордские руководства по логике. Том. 35. Издательство Оксфордского университета . стр. XV, 605. ISBN. 0-19-853779-4.

• Констебль, Р.; Бикфорд, М. (2014). «Интуиционистская полнота логики первого порядка». Анналы чистой и прикладной логики . 165 : 164–198. arXiv : 1110.1614 . дои : 10.1016/j.apal.2013.07.009. S2CID  849930.

• Ван Дален, Дирк (2001). «Интуиционистская логика». В Гобле, Лу (ред.). Руководство Блэквелла по философской логике . Нью-Йорк: Издательство Блэквелл . стр. 224–257. дои : 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 г.). «В начале была семантика игры?». Ин Майер, О.; Пиетаринен, А.-В.; Туленхеймо, Т. (ред.). Игры: объединяем логику, язык и философию. Спрингер . стр. 249–350.

• Крипке, Саул А. (1965). «Семантический анализ интуиционистской логики I» (PDF) . В Кроссли, JN; Даммет, Мэй (ред.). Формальные системы и рекурсивные функции. Материалы восьмого коллоквиума по логике, Оксфорд, июль 1963 г. Исследования по логике и основам математики. Том. 40. Амстердам: Издательство Северной Голландии . стр. 92–130. дои : 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). «Модальные аналоги медведевской логики конечных задач не являются конечно аксиоматизируемыми». Студия Логика . 49 (3): 365–385. дои : 10.1007/BF00370370.

• Соренсен, Мортен Х.; Уржичин, Павел (2006). «Глава 2: Интуиционистская логика». Лекции по изоморфизму Карри-Говарда . Исследования по логике и основам математики. Том. 149 (1-е изд.). Амстердам: Эльзевир . ISBN 978-0-444-52077-7.

• Такеути, Гаиси (2013) [1975]. Теория доказательств (Второе изд.). Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-49073-1.

• Тарский, Альфред (1938). «Der Aussagenkalkül und die Topologie». Фундамента Математика . 31 : 103–134. дои : 10.1007/BF00370370.

• Троэльстра, А.С.; Ван Ульсен, П. «Открытие семантики Э. В. Бет для интуиционистской логики» (PDF) . Институт логики, языка и вычислений (ILLC). Университет Амстердама.

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

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

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

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

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