Интуиционистское исчисление высказываний

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

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

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

$\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. $(A\to ((\neg A)\to B))$

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

Modus ponens: $\frac{A,\;(A\to B)}{B}$.