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

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

Основное отличие от привычного исчисления высказываний заключается в том, что отсутствует закон исключённого третьего.

Схемы аксиом 1-10 и правило «модус поненс» задают интуиционистское исчисление высказываний. Все 12 схем аксиом и все 3 правила вывода задают интуиционистское исчисление предикатов. Интуиционистское исчисление предикатов отличается от классического тем, что в последнем вместо схемы аксиом 10 используется схема аксиом $(\neg \neg A)\to A$.

Логические символы

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

Схемы аксиом

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

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

Правила вывода

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

См. также

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

Литература

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