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

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

Синтаксис

Синтаксис формул в интуиционистской логике сходен с синтаксисом логики высказываний или логики первого порядка. Разница заключается в том, что многие тавтологии этих классических логик не могут быть доказаны в рамках логики интуиционистской. В качестве примеров можно привести не только закон исключённого третьего ($P \and \neg P$), но и закон Пирса ($((P \rightarrow Q) \rightarrow P) \rightarrow P$) и даже закон отрицания отрицания В классической логике оба выражения $P \rightarrow \neg \neg P$ и $\neg \neg P \rightarrow P$ являются теоремами. В интуиционистской логике только первое выражение является теоремой: отрицание отрицания может быть выведено, но не может быть удалено.

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

Аксиоматика

Используемое правило вывода — Modus Ponens. Система аксиом следующая:

• THEN-1: $\phi \rightarrow (\chi \rightarrow \phi)$
• THEN-2: $(\phi \rightarrow (\chi \rightarrow \psi)) \rightarrow ((\phi \rightarrow \chi) \rightarrow (\phi \rightarrow \psi))$
• AND-1: $\phi \and \chi \rightarrow \phi$
• AND-2: $\phi \and \chi \rightarrow \chi$
• AND-3: $\phi \rightarrow (\chi \rightarrow (\phi \and \chi))$
• OR-1: $\phi \rightarrow \phi \or \chi$
• OR-2: $\chi \rightarrow \phi \or \chi$
• OR-3: $(\phi \rightarrow \psi) \rightarrow ((\chi \rightarrow \psi) \rightarrow (\phi \or \chi \rightarrow \psi))$
• NOT-1: $(\phi \rightarrow \chi) \rightarrow ((\phi \rightarrow \neg \chi) \rightarrow \neg \phi)$
• NOT-2: $\phi \rightarrow (\neg \phi \rightarrow \chi)$

Для того чтобы сделать приведённую систему аксиом совместимой с логикой предикатов первого порядка, добавляется правило обобщения и следующий набор аксиом:

• PRED-1: $(\forall x Z(x)) \rightarrow Z(t)$
• PRED-2: $Z(t) \rightarrow (\forall x Z(x))$
• PRED-3: $(\forall x (W \rightarrow Z(x)) \rightarrow (W \rightarrow \forall x Z(x))$
• PRED-4: $(\forall x (Z(x) \rightarrow W)) \rightarrow (\forall x Z(x) \rightarrow W)$

Взаимная определяемость операций

В классической пропозициональной логике (логике высказываний) возможно построить базис операций, который позволит определять одни операции через другие. Например, базисом являются три операции Лукасевича — конъюнкция, дизъюнкция и отрицание. Более того, существуют базисы, состоящие из одной операции, а потому перечисленные операции можно определить через такие однооператорные базисы. К ним, к примеру, относятся: стрелка Пирса (NOR — не ИЛИ) и штрих Шеффера (NAND — не И). Абсолютно также в классической логике первого порядка один из кванторов может быть определён через другой при помощи отрицания.

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

1. Связь конъюнкции и дизъюнкции:
   • $(\phi \wedge \psi) \to \neg (\neg \phi \vee \neg \psi)$
   • $(\phi \vee \psi) \to \neg (\neg \phi \wedge \neg \psi)$
   • $(\neg \phi \vee \neg \psi) \to \neg (\phi \wedge \psi)$
   • $(\neg \phi \wedge \neg \psi) \leftrightarrow \neg (\phi \vee \psi)$
2. Связь конъюнкции и импликации:
   • $(\phi \wedge \psi) \to \neg (\phi \to \neg \psi)$
   • $(\phi \to \psi) \to \neg (\phi \wedge \neg \psi)$
   • $(\phi \wedge \neg \psi) \to \neg (\phi \to \psi)$
   • $(\phi \to \neg \psi) \leftrightarrow \neg (\phi \wedge \psi)$
3. Связь дизъюнкции и импликации:
   • $(\phi \vee \psi) \to (\neg \phi \to \psi)$
   • $(\neg \phi \vee \psi) \to (\phi \to \psi)$
   • $\neg (\phi \to \psi) \to \neg (\neg \phi \vee \psi)$
   • $\neg (\phi \vee \psi) \leftrightarrow \neg (\neg \phi \to \psi)$
4. Связь кванторов всеобщности и существования:
   • $(\forall x \ \phi(x)) \to \neg (\exist x \ \neg \phi(x))$
   • $(\exist x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))$
   • $(\exist x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))$
   • $(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exist x \ \phi(x))$

Для разъяснения можно рассмотреть следующие примеры. В интуиционистской логике высказывание «a или b» является более сильным, нежели высказывание «если не a, то b», поскольку из первого следует второе, но не наоборот (в классической логике эти высказывания тождественны). С другой стороны, высказывание «не (a и b)» эквивалентно высказыванию «не a или не b», поскольку каждое из них может следовать из другого.

Исчисление следствий

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

Семантика

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

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

В классической логике часто обсуждаются значения истинности, которые могут принимать переменные. Такие значения обычно выбираются из множества значений алфавита булевой алгебры. Операции конъюнкции и дизъюнкции обозначаются в булевой алгебре символами $\and$ и $\or$ соответственно, так что формула $A \and B$ обозначает дизъюнкцию двух значений истинности ($A$ и $B$) в булевой алгебре. В этом случае имеется теорема, которая гласит, что формула является правильной в классической логике тогда и только тогда, когда её значений равно $1$ для любых значений истинности входящих в неё переменных.

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

Можно показать, что для того чтобы доказать правильность формулы, достаточно найти простую алгебру Хейтинга, элементы которой являются множествами на простой плоскости $R^2$. В этой алгебре операции $\and$ и $\or$ соответствуют пересечению и объединению множеств, а значением формулы $A \rightarrow B$ является выражение $(A^C \cap B)^{\circ}$, то есть внутренность пересечения множества $B$ и дополнения множества $A$. Самым нижним элементом является пустое множество, самым верхним — универсум $R^2$. Отрицание обычно определяется как $\neg A \equiv A \rightarrow \empty$, поэтому отрицание редуцируется в выражение $A^{C \circ}$, то есть внутренность дополнения множества $A$.

Например, формула $\neg (A \and \neg A)$ правильная, поскольку безразлично, какое множество будет выбрано в качестве значения множества $A$, значением этой формулы будет вся двумерная плоскость: $$Value (\neg (A \and \neg A)) =$$ $$(Value (A \and \neg A))^{C \circ} =$$ $$(Value (A) \cap Value (\neg A))^{C \circ} =$$ $$(X \cap (Value (A))^{C \circ})^{C \circ} =$$ $$(X \cap X^{C \circ})^{C \circ}$$

Одна теорема топологии говорит о том, что $X^{C \circ}$ является подмножеством $X^C$, поэтому пересечение множеств пусто: $$\empty^{C \circ} = (R^2)^{\circ} = R^2$$

Таким образом формула является тавтологией при любых значениях истинности входящих в неё переменных.

Также можно показать, что закон исключённого третьего неправилен в интуиционистской логике. Для этого значением терма $A$ необходимо сделать множество $\{ y \mid y > 0 \}$. В этом случае значением отрицания $\neg A$ будет внутренность множества $\{ y \mid y \leq 0\}$, что есть $\{ y \mid y < 0\}$. Значением формулы $A \or \neg A$ (закон исключённого третьего), то есть значение объединения множеств $\{ y \mid y > 0 \}$ и $\{ y \mid y < 0 \}$, что есть $\{ y \mid y \neq 0 \}$. В свою очередь последнее полученное выражение не тождественно всей плоскости $R^2$.

Описанная выше бесконечная алгебра Хейтинга позволяет проверить правильность всех формул в интуиционистской логике независимо от того, какие значения истинности приписаны переменным в формулах. Обратно, для неправильной формулы существует способ задания значений истинности переменным формулы, который ведёт к неправильной интерпретации этой формулы. Также можно показать, что ни одна из конечных алгебр Хейтинга не обладает этим свойством.

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

На основе своей семантики модальной логики Сол Крипке создал иную семантику для интуиционистской логики, известную по его имени — «семантика Крипке» или «относительная семантика».

См. также

• Изоморфизм Карри-Говарда
• Интуиционизм
• Интуиционистская теория типов
• Классическая логика
• Конструктивное доказательство
• Линейная логика

Ссылки и литература

• Стэндфордская энциклопедия философии: «Интуиционистская логика».
• Van Dalen, Dirk, Intuitionistic Logic, in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell, 2001.