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

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

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

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

Валерий Иванович Гливенко доказал, что в рамках интуиционистской логики двойное отрицание каждого истинного предложения классической логики доказуемо в логике Брауэра.

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

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

Схемы аксиом

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

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

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

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

См. также

• Интуиционизм

Литература

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