Интуициони́стская ло́гика
— формальная система, отражающая некоторые способы рассуждений, приемлемые с точки зрения
интуиционизма
. Предложена
А. Гейтингом
в
1930
.
Основное отличие от привычного исчисления высказываний заключается в том, что отсутствует
закон исключённого третьего
.
Схемы аксиом 1-10 и правило «модус поненс» задают
интуиционистское исчисление высказываний
. Все 12 схем аксиом и все 3 правила вывода
задают интуиционистское исчисление предикатов
. Интуиционистское исчисление предикатов отличается от классического тем, что в последнем вместо схемы аксиом 10 используется схема аксиом
(
¬
¬
A
)
→
A
{\displaystyle (\neg \neg A)\to A}
.
.
Логические символы
∧
{\displaystyle \land }
(знак
конъюнкции
),
∨
{\displaystyle \lor }
(знак
дизъюнкции
),
→
{\displaystyle \to }
(знак
импликации
) и
¬
{\displaystyle \neg }
(знак
отрицания
).
Схемы аксиом
Далее через
A
{\displaystyle A}
,
B
{\displaystyle B}
и
C
{\displaystyle C}
обозначаются произвольные пропозициональные формулы.
(
A
→
(
B
→
A
)
)
{\displaystyle (A\to (B\to A))}
(
(
A
→
B
)
→
(
(
B
→
C
)
→
(
A
→
C
)
)
)
{\displaystyle ((A\to B)\to ((B\to C)\to (A\to C)))}
(
A
→
(
B
→
(
A
∧
B
)
)
)
{\displaystyle (A\to (B\to (A\land B)))}
(
(
A
∧
B
)
→
A
)
{\displaystyle ((A\land B)\to A)}
(
(
A
∧
B
)
→
B
)
{\displaystyle ((A\land B)\to B)}
(
A
→
(
A
∨
B
)
)
{\displaystyle (A\to (A\lor B))}
(
B
→
(
A
∨
B
)
)
{\displaystyle (B\to (A\lor B))}
(
(
A
→
C
)
→
(
(
B
→
C
)
→
(
(
A
∨
B
)
→
C
)
)
)
{\displaystyle ((A\to C)\to ((B\to C)\to ((A\lor B)\to C)))}
(
(
A
→
B
)
→
(
(
A
→
(
¬
B
)
)
→
(
¬
A
)
)
)
{\displaystyle ((A\to B)\to ((A\to (\neg B))\to (\neg A)))}
(
(
¬
A
)
→
(
A
→
B
)
)
{\displaystyle ((\neg A)\to (A\to B))}
∀
x
A
(
x
)
→
A
(
y
)
{\displaystyle \forall xA(x)\to A(y)}
A
(
y
)
→
∃
x
A
(
x
)
{\displaystyle A(y)\to \exists xA(x)}
Правила вывода
Modus ponens
:
A
,
(
A
→
B
)
B
{\displaystyle {\frac {A,\;(A\to B)}{B}}}
.
C
→
A
(
x
)
C
→
∀
x
A
(
x
)
{\displaystyle {\frac {C\to A(x)}{C\to \forall xA(x)}}}
если
x
{\displaystyle x}
не является свободной переменной в
C
{\displaystyle C}
.
A
(
x
)
→
C
∃
x
A
(
x
)
→
C
{\displaystyle {\frac {A(x)\to C}{\exists xA(x)\to C}}}
если
x
{\displaystyle x}
не является свободной переменной в
C
{\displaystyle C}
.
См. также
Примечания
В. Е. Плиско
Интуиционистская логика. — Математический энциклопедический словарь. — М.,
Советская энциклопедия
, 1988. — Тираж 150 000 экз. — c. 243
Литература
Ссылки на внешние ресурсы
Словари и энциклопедии
В библиографических каталогах
Группы логик
Компоненты