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

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

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

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

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

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

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

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

Синтаксис

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

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

Слабее классической логики

Интуиционистскую логику можно понимать как ослабление классической логики, означающее, что она более консервативна в том, что позволяет рассуждающему делать выводы, но не допускает никаких новых выводов, которые не могли быть сделаны в рамках классической логики. Каждая теорема интуиционистской логики - это теорема классической логики, но не наоборот. Много тавтологии в классической логике не являются теоремами в интуиционистской логике - в частности, как было сказано выше, одним из ее главных пунктов является недопущение утверждения закона исключенного третьего, чтобы исказить использование неконструктивных доказательство от противного который может использоваться для предоставления утверждений о существовании без предоставления явных примеров объектов, которые он доказывает. Мы говорим «не утверждать», потому что, хотя это не обязательно верно, что закон соблюдается в любом контексте, нельзя привести никакого контрпримера: такой контрпример был бы выводом (предполагающим отрицание закона для определенного утверждения), недопустимым согласно классической логика и, следовательно, не допускается в строгом ослаблении, как интуиционистская логика. В самом деле, двойное отрицание закона сохраняется как тавтология системы: то есть это теорема о том, что ${ 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 фи земля чи к фи}$
• И-2: ${ Displaystyle фи земля чи к чи}$
• И-3: ${ Displaystyle фи к ( чи к ( фи земля чи))}$
• ИЛИ-1: ${ Displaystyle фи к фи лор чи}$
• ИЛИ-2: ${ Displaystyle чи к фи лор чи}$
• ИЛИ-3: ${ Displaystyle ( фи к пси) к (( чи к пси) к (( фи лор чи) к пси))}$
• ЛОЖНЫЙ: ${ displaystyle bot to phi}$

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

• ${ displaystyle forall}$-GEN: от ${ displaystyle psi to phi}$ сделать вывод ${ Displaystyle psi к ( forall x phi)}$, если ${ displaystyle x}$ не бесплатно в ${ displaystyle psi}$
• ${ Displaystyle существует}$-GEN: от ${ displaystyle phi to psi}$ сделать вывод ${ Displaystyle ( существует х phi) к psi}$, если ${ displaystyle x}$ не бесплатно в ${ displaystyle psi}$

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

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

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

Отрицание

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

• НЕ-1 ': ${ Displaystyle ( фи к бот) к lnot phi}$
• НЕ-2 ': ${ Displaystyle lnot phi to ( phi to bot)}$

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

• НЕ-1: ${ Displaystyle ( фи к чи) к (( фи к лнот чи) к лнот фи)}$
• НЕ-2: ${ Displaystyle фи к ( lnot фи к чи)}$

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

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

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

• МКФ-1: ${ Displaystyle ( фи leftrightarrow чи) к ( фи к чи)}$
• МКФ-2: ${ Displaystyle ( фи leftrightarrow чи) к ( чи к фи)}$
• МКФ-3: ${ Displaystyle ( фи к чи) к (( чи к фи) к ( фи leftrightarrow чи))}$

IFF-1 и IFF-2 при желании можно объединить в единую аксиому ${ Displaystyle ( фи leftrightarrow чи) к (( фи к чи) земля ( чи к фи))}$ используя союз.

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

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

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

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

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

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

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

В классической логике высказываний можно взять одно из соединение, дизъюнкция, или значение как примитив, и определить два других в терминах этого вместе с отрицание, например, в Лукасевич с три аксиомы логики высказываний. Все четыре можно даже определить с помощью единственный достаточный оператор такой как Стрела Пирса (NOR) или Инсульт Шеффера (И-НЕ). Точно так же в классической логике первого порядка один из кванторов может быть определен в терминах другого и отрицания.

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

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

• ${ Displaystyle ( фи клин фунт / кв. дюйм) к нег ( нег фи ви нег фунт / кв. дюйм)}$
• ${ displaystyle ( phi vee psi) to neg ( neg phi wedge neg psi)}$
• ${ Displaystyle ( нег фи ви нег пси) к нег ( фи клин пси)}$
• ${ Displaystyle ( нег фи клин нег фунт / кв. дюйм) leftrightarrow neg ( фи ви фунт / кв. дюйм)}$

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

• ${ Displaystyle ( фи клин psi) к neg ( phi to neg psi)}$
• ${ displaystyle ( phi to psi) to neg ( phi wedge neg psi)}$
• ${ Displaystyle ( фи клин нег пси) к нег ( фи к пси)}$
• ${ displaystyle ( phi to neg psi) leftrightarrow neg ( phi wedge psi)}$

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

• ${ Displaystyle ( фи ви пси) к ( нег фи к пси)}$
• ${ Displaystyle ( нег фи ви пси) к ( фи к пси)}$

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

• ${ Displaystyle ( forall x phi (x)) к neg ( существует x neg phi (x))}$
• ${ Displaystyle ( существует х phi (x)) к neg ( forall x neg phi (x))}$
• ${ Displaystyle ( существует х neg phi (x)) к neg ( forall x phi (x))}$
• ${ displaystyle ( forall x neg phi (x)) leftrightarrow neg ( существует x phi (x))}$

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

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

• ${ Displaystyle ( фи leftrightarrow psi) leftrightarrow (( phi to psi) land ( psi to phi))}$
• ${ Displaystyle ( фи к psi) leftrightarrow (( phi lor psi) leftrightarrow psi)}$
• ${ Displaystyle ( фи к psi) leftrightarrow (( phi land psi) leftrightarrow phi)}$
• ${ Displaystyle ( фи земля psi) leftrightarrow (( phi to psi) leftrightarrow phi)}$
• ${ Displaystyle ( фи земля psi) leftrightarrow ((( phi lor psi) leftrightarrow psi) leftrightarrow phi)}$

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

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

• ${ Displaystyle ((п лор д) земля нег р) лор ( нег р земля (д leftrightarrow г)),}$
• ${ displaystyle p to (q land neg r land (s lor t)).}$

Семантика

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

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

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

Семантика гейтинга

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

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

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

${ displaystyle { begin {align} { text {Value}} [ bot] & = emptyset { text {Value}} [ top] & = mathbf {R} { text { Значение}} [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 {align}}}$

где int (Икс) это интерьер из Икс и Икс^∁ его дополнять.

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

${ displaystyle { begin {align} { 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 { Значение}} [A] ^ { complement} cup emptyset right) & = { text {int}} left ({ text {Value}} [A] ^ { complement} right) конец {выровнено}}}$

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

${ displaystyle { begin {align} { text {Value}} [ neg (A land neg A)] & = { text {int}} left ({ text {Value}} [A земля neg A] ^ { complement} right) && { text {Value}} [ neg B] = { text {int}} left ({ text {Value}} [B] ^ { дополнение} 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 { Значение}} [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} конец {выровнено}}}$

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

${ displaystyle { begin {align} { text {Value}} [A lor neg A] & = { text {Value}} [A] cup { text {Value}} [ neg A] & = { text {Значение}} [A] cup { text {int}} left ({ text {Value}} [A] ^ { complement} right) && { text {Значение }} [ 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} конец {выровнено}}}$

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

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

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

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

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

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

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

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

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

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

Отношение к промежуточной логике

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

Отношение к модальной логике

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

${ displaystyle { begin {align} bot ^ {*} & = bot A ^ {*} & = Box A && { text {if}} A { text {простое число (положительный литерал) }} (A клин B) ^ {*} & = A ^ {*} клин B ^ {*} (A vee B) ^ {*} & = A ^ {*} vee B ^ {*} (от A к B) ^ {*} & = Box left (A ^ {*} to B ^ {*} right) ( neg A) ^ {*} & = Box ( neg (A ^ {*})) && neg A: = A to bot end {выравнивается}}}$

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

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

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

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

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

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

Примечания

использованная литература

внешняя ссылка

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