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

Интуициони́стская ло́гика — формальная система, отражающая некоторые способы рассуждений, приемлемые с точки зрения интуиционизма. Предложена А. Гейтингом в 1930 году.

В интуиционистской логике Int в отличии от классической отсутствует закон исключённого третьего ${\displaystyle A\lor \lnot A}$, известный со времен Аристотеля.

Множество формул, содержащее аксиомы 1-10 и замкнутое относительно modus ponens, составляет теоремы интуиционистской пропозициональной логики Int.

Все 12 аксиом и все 3 правила вывода задают интуиционистское исчисление предикатов. Интуиционистское исчисление предикатов отличается от классического тем, что в последнем вместо схемы аксиом 10 используется схема аксиом ${\displaystyle \neg \neg A\to A}$^[1].

Во-первых, элиминация закона исключенного третьего, из которого выводимо снятие двойного отрицания ${\displaystyle \neg \neg A\to A}$, меняет понятие существование объекта.

Пусть, например, ${\displaystyle \alpha (x)}$ пропозициональная функция в некоторой арифметике целых чисел. Доказывая утверждение

${\displaystyle \land }$ (знак конъюнкции), ${\displaystyle \lor }$ (знак дизъюнкции), ${\displaystyle \to }$ (знак импликации) и ${\displaystyle \neg }$ (знак отрицания).

Далее через ${\displaystyle A}$, ${\displaystyle B}$ и ${\displaystyle C}$ обозначаются произвольные пропозициональные формулы.

1. ${\displaystyle A\to (B\to A)}$
2. ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$
3. ${\displaystyle A\to (B\to (A\land B))}$
4. ${\displaystyle (A\land B)\to A}$
5. ${\displaystyle (A\land B)\to B}$
6. ${\displaystyle A\to (A\lor B)}$
7. ${\displaystyle B\to (A\lor B)}$
8. ${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$
9. ${\displaystyle (A\to B)\to ((A\to (\neg B))\to (\neg A))}$
10. ${\displaystyle \neg A\to (A\to B)}$
11. ${\displaystyle \forall xA(x)\to A(y)}$
12. ${\displaystyle A(y)\to \exists xA(x)}$

1. Modus ponens: ${\displaystyle {\frac {A,\;(A\to B)}{B}}}$.
2. ${\displaystyle {\frac {C\to A(x)}{C\to \forall xA(x)}}}$ если ${\displaystyle x}$ не является свободной переменной в ${\displaystyle C}$.
3. ${\displaystyle {\frac {A(x)\to C}{\exists xA(x)\to C}}}$если ${\displaystyle x}$ не является свободной переменной в ${\displaystyle C}$.

• Интуиционизм
• Теорема Гливенко

• Гейтинг А. Интуиционизм. — М., 1965.
• Клини С. К. Введение в метаматематику. — М., 1957.
• Новиков П. С. Конструктивная математическая логика с точки зрения классической. — М., 1977.
• Драгалин А. Г. Математический интуиционизм. Введение в теорию доказательств. — М., 1979.
• H. H. Непейвода. Интуиционистская логика // Новая философская энциклопедия : в 4 т. / пред. науч.-ред. совета В. С. Стёпин. — 2-е изд., испр. и доп. — М. : Мысль, 2010. — 2816 с.