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

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

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

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

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

Обоснование

Одной из причин, по которой классическая логика подвергается критике, является наличие в ней закона исключённого третьего. Эта аксиома идейно противоречит активно изучаемой с начала 20-го века особенности всех известных теорий -- их неполноте. Существуют утверждения, которые могут быть сформулированы на языке теории, но не могут быть ни доказаны, ни опровергнуты. Самыми известными примерами таких утверждений являются континуум-гипотеза и непротиворечивость формальной арифметики (см. Теоремы Гёделя о неполноте).

Ещё задолго до появления теоремы Гёделя о неполноте математика столкнулась с кризисом оснований, проявлявшимся как в грубых парадоксах типа противоречий (например, парадокс Рассела), так и в том, что понятия, изначально считавшиеся тождественными, стали заметно расходиться. Например, понятия "быть построенным" и "существовать". И не смотря на то, что последнее пытались решить избавлением от аксиомы выбора (что привело к изучению системы ZFD), но это не стало решением всех проблем..

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

$\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$.

Основные свойства

1. $\neg \neg \neg A\leftrightarrow \neg A$, что означает отсутствие тройного отрицания.
2. Теорема Гливенко: для любой формулы $\varphi$ языка классической логики выполнено: $\neg \neg \varphi \in Int\leftrightarrow \varphi \in Cl$

См. также

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

Литература

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

• С. П. Одинцов, С. О. Сперанский, С. А. Дробышевич -- Введение в неклассические логики. Учебное пособие.