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

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

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

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

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

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

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

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

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

Синтаксис

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

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

стиле

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

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

• Депутат: от $\phi \to \psi$ и $\phi$ сделать вывод $\psi$

и аксиомы

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

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

• $\forall$-GEN: от $\psi \to \phi$ сделать вывод $\psi \to (\forall x\ \phi )$, если $x$ не является бесплатным в $\psi$
• $\exists$-GEN: от $\phi \to \psi$ сделать вывод $(\exists x\ \phi )\to \psi$, если $x$ не является бесплатным в $\psi$

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

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

Отрицание

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

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

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

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

как в исчислении высказываний § Аксиомы . Альтернативой NOT-1 являются $(\phi \to \neg \chi )\to (\chi \to \neg \phi )$ или $(\phi \to \neg \phi )\to \neg \phi$.

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

Соединительная $\leftrightarrow$ эквивалентность можно рассматривать как аббревиатуру, с $\phi \leftrightarrow \chi$ стоящий за $(\phi \to \chi )\land (\chi \to \phi )$. Альтернативно можно добавить аксиомы

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

МФФ-1 и МФФ-2 при желании можно объединить в одну аксиому. $(\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))$ используя союз.

Расчеты следуют

Основная статья: Секвенционное исчисление

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

Другие производные LK ограничены интуиционистскими выводами, но все же позволяют сделать несколько последовательных выводов. ЖЖ' это один из примеров.

Теоремы

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

$(\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )$

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

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

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

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

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

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

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

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

Перевод формулы

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

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

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

$(\phi \lor \psi )\to \neg (\neg \phi \land \neg \psi )$

$(\phi \lor \psi )\to (\neg \phi \to \neg \neg \psi )$, ослабленный вариант дизъюнктивного силлогизма

соотв.

$(\phi \land \psi )\to \neg (\neg \phi \lor \neg \psi )$

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

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

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

универсальная количественная

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

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

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

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

• $(\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))$

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

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

$(\exists x\ \neg \phi (x))\to \neg (\forall x\,\neg \neg \phi (x))$

Словами: «Если существует сущность $x$ у которого нет собственности $\phi$ следующее , то опровергается : для каждого объекта невозможно доказать , что он не обладает имуществом $\phi$".

Во-вторых,

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

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

• $(\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))$

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

$(\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))$

$(\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))$

Конечно, можно вывести и варианты таких формул, содержащие двойное отрицание в антецеденте. Частным случаем первой формулы здесь является $(\forall x\,\neg \phi (x))\to \neg (\exists x\,\neg \neg \phi (x))$ и это действительно сильнее, чем $\to$-направление пункта эквивалентности, указанного выше. Для простоты обсуждения здесь и далее формулы обычно представляются в ослабленной форме без всех возможных вставок двойных отрицаний в предшествующие.

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

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

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

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

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

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

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

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

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

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

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

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

• $(\phi \to \neg \psi )\leftrightarrow \neg (\phi \land \psi )$

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

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

• $\neg (\phi \to \psi )\leftrightarrow (\neg \neg \phi \land \neg \psi )$

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

• $\neg \neg (\phi \land \psi )\leftrightarrow (\neg \neg \phi \land \neg \neg \psi )$

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

Дизъюнкция

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

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

• $(\neg \phi \lor \psi )\to (\phi \to \psi )$

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

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

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

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

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

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

Эквиваленты

Приведенные выше списки также содержат эквиваленты. Эквивалентность конъюнкции и дизъюнкции вытекает из $(P\lor Q)\to R$ на самом деле сильнее, чем $P\to R$. Обе стороны эквивалентности можно понимать как соединения независимых импликаций. Выше абсурд. $\bot$ используется для $R$. В функциональных интерпретациях он соответствует конструкциям if-предложения . Например, «Нет ( $P$ или $Q$)» эквивалентно «Не $P$, а также нет $Q$".

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

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

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

• $(\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )$
• $(\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )$
• $(\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )$
• $(\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )$

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

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

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

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

Семантика

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

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

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

Гейтинга

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

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

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

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

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

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

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

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

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

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

Основная статья: семантика Крипке

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

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

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

Metalogic

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

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

Связь с другими логиками

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

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

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

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

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

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

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

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

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

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

• $(\neg \phi \to \neg \chi )\to (\chi \to \phi )$

Подробно это описано в статье промежуточную логику .

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

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

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

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

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

${\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. Приведенный выше набор формул называется переводом Гёделя–МакКинси–Тарского . Существует также интуиционистская версия модальной логики S4, называемая конструктивной модальной логикой CS4.

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

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

См. также

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

Ссылки

• Алечина, Наташа; Мендлер, Майкл; Де Пайва, Валерия ; Риттер, Эйке (январь 2003 г.). Категориальная семантика и семантика Крипке для конструктивной модальной логики S4 (PDF) . Материалы 15-го международного семинара по логике информатики. Конспекты лекций по информатике . дои : 10.1007/3-540-44802-0_21 .
• Аояма, Хироши (2004). «ЛК, ЛД, двойная интуиционистская логика и квантовая логика» . Журнал формальной логики Нотр-Дама . 45 (4): 193–213. дои : 10.1305/ndjfl/1099238445 .
• Бежанишвили, Ник; Де Йонг, Дик. «Интуиционистская логика» (PDF) . Амстердамский университет (Институт логики, языка и вычислений).
• Бруннер, ПРО; Карниелли, Уолтер (март 2005 г.). «Антиинтуиционизм и паранепротиворечивость» . Журнал прикладной логики . 3 (1): 161–184. дои : 10.1016/j.jal.2004.07.016 .
• Берджесс, Джон (январь 2014 г.). «Три вида интуиции во взглядах Гёделя на континуум» (PDF) . doi : 10.1017/CBO9780511756306.002 (неактивен 4 июня 2024 г.). {{cite web}}: CS1 maint: DOI неактивен по состоянию на июнь 2024 г. ( ссылка )
• Чагров, Александр; Захарьящев, Михаил (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). Формальные правила интуиционистской логики I, II, III . Труды Прусской академии наук (на немецком языке). стр. 42–56, 57–71, 158–169. В трех частях
• Джапаридзе, Георгий (январь 2009 г.). «В начале была семантика игры?» . Ин Майер, О.; Пиетаринен, А.-В.; Туленхеймо, Т. (ред.). Игры: объединяем логику, язык и философию . Том. 15. Спрингер . стр. 249–350. arXiv : cs/0507045 . дои : 10.1007/978-1-4020-9374-6_11 . ISBN  978-1-4020-9373-9 .
• Крипке, Саул А. (1965). «Семантический анализ интуиционистской логики I» (PDF) . В Кроссли, JN; Даммет, Мэй (ред.). Формальные системы и рекурсивные функции. Материалы восьмого коллоквиума по логике, Оксфорд, июль 1963 г. Исследования по логике и основам математики. Том. 40. Амстердам: Издательство Северной Голландии . стр. 92–130. дои : 10.1016/S0049-237X(08)71685-9 . ISBN  9780444534057 .
• Леви, Мишель (29 апреля 2011 г.), Пропозициональная модальная логика S4 и пропозициональная интуиционистская логика (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). «Исчисление высказываний и топология» . Фундамента Математика . 31 : 103–134. дои : 10.1007/BF00370370 .
• Троэльстра, А.С.; Ван Ульсен, П. «Открытие семантики Э. В. Бет для интуиционистской логики» (PDF) . Институт логики, языка и вычислений (ILLC). Университет Амстердама.

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

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

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

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

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