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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

и аксиомы

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle {\begin{aligned}\bot ^{*}&=\bot \\A^{*}&=\Box A&&{\text{if }}A{\text{ is prime (a positive literal)}}\\(A\wedge B)^{*}&=A^{*}\wedge B^{*}\\(A\vee B)^{*}&=A^{*}\vee B^{*}\\(A\to B)^{*}&=\Box \left(A^{*}\to B^{*}\right)\\(\neg A)^{*}&=\Box (\neg (A^{*}))&&\neg A:=A\to \bot \end{aligned}}}$

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

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

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

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

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

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

Примечания [ править ]

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

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

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