Intuicjonistyczny rachunek zdań

Intuicjonistyczny rachunek zdań, INT, w wersji inwariantnej — rachunek zdaniowy w języku klasycznego rachunku zdań z regułą odrywania jako jedyną pierwotną regułą wnioskowania oraz aksjomatami następującej postaci:

Ax $_{1}$ $\alpha\to(\beta\to \alpha)$	prawo poprzedzania
Ax $_{2}$ $[\alpha\to(\beta\to \gamma)]\to[(\alpha\to \beta)\to(\alpha\to \gamma)]$	sylogizm Fregego
Ax $_{3}$ $\alpha\wedge \beta\to \alpha$	prawo opuszczania koniunkcji, 1.
Ax $_{4}$ $\alpha\wedge \beta\to \beta$	prawo opuszczania koniunkcji, 2.
Ax $_{5}$ $(\alpha\to \beta)\to[(\alpha\to \gamma)\to(\alpha\to \beta\wedge \gamma)]$	prawo wprowadzania koniunkcji
Ax $_{6}$ $\alpha\to \alpha\vee \beta$	prawo wprowadzania alternatywy, 1.
Ax $_{7}$ $\beta\to \alpha\vee \beta$	prawo wprowadzania alternatywy, 2.
Ax $_{8}$ $(\beta\to \alpha)\to[(\gamma\to \alpha)\to(\beta\vee \gamma\to \alpha)]$	prawo łączenia implikacji
Ax $_{9}$ $(\alpha\leftrightarrow \beta)\to(\alpha\to \beta)]$	prawo opuszczania równoważności, 1.
Ax $_{10}$ $(\alpha\leftrightarrow \beta)\to(\beta\to \alpha)]$	prawo opuszczania równoważności, 2.
Ax $_{11}$ $(\alpha\to \beta)\to[(\beta\to \alpha)\to(\alpha\leftrightarrow \beta)]$	prawo wprowadzania równoważności
Ax $_{12}$ $\alpha\to(\neg \alpha\to \beta)$	prawo przepełnienia
Ax $_{13}$ $(\alpha\to\neg \alpha)\to\neg \alpha$	prawo redukcji do absurdu

Zwracamy uwagę na brak (silnego) prawa podwójnego przeczenia: $\neg\neg p\to p$ , którego dodanie do aksjomatyki INT tworzy aksjomatykę klasycznego rachunku zdań.

W rachunku intuicjonistycznym dowodliwe są m.in. następujące formuły:

1.	$p\to p$	prawo identyczności
2.	$p\to\neg\neg p$	słabe prawo podwójnego przeczenia
3.	$(p\to q)\to(\neg q\to\neg p)$	słabe prawo kontrapozycji
4.	$(p\to\neg q)\to(q\to\neg p)$	słabe prawo transpozycji
5.	$\neg(p\vee q)\leftrightarrow(\neg q\wedge\neg p)$	prawo de Morgana, 2.
6.	$(p\to q)\to[(q\to s)\to(p\to s)]$	prawo przechodniości
7.	$[p\to (q\to s)]\to(p\wedge q\to s)$	prawo importacji
8.	$(p\wedge q\to s)\to[p\to (q\to s)]$	prawo eksportacji

Dla przykładu zaprezentujemy dowód formuł 1. i 2. w rachunku INT:

Prawo identyczności: $p\to p$

1.	$p\to[(p\to p)\to p]$	Ax $_1$
2.	$\{p\to[(p\to p)\to p]\}\to\{[p\to(p\to p)]\to(p\to p)\}$	Ax $_2$
3.	$[p\to(p\to p)]\to(p\to p)$	reguła odrywania: 1,2
4.	$p\to(p\to p)$	Ax $_1$
5.	$p\to p$	reguła odrywania: 3,4

Słabe prawo podwójnego przeczenia: $p\to\neg\neg p$

1.	$(\neg p\to \neg\neg p) \to \neg\neg p$	Ax $_{13}$
2.	$[(\neg p\to \neg\neg p) \to \neg\neg p]\to\{p\to[(\neg p\to \neg\neg p) \to \neg\neg p]\}$	Ax $_{1}$
3.	$p\to(\neg p\to \neg\neg p) \to \neg\neg p$	reguła odrywania: 1,3
4.	$\{p\to[(\neg p\to \neg\neg p) \to \neg\neg p\}\to\{[p\to(\neg p\to\neg\neg p)]\to(p\to\neg\neg p)\}$	Ax $_{2}$
5.	$[p\to(\neg p\to\neg\neg p)]\to(p\to\neg\neg p)$	reguła odrywania: 3,4
6.	$p\to(\neg p\to\neg\neg p)$	Ax $_{12}$
7.	$p\to\neg\neg p$	reguła odrywania: 5,6

Narzędziem, które znakomicie przyspiesza proces dowodzenia, że pewne formuły są tezami INT jest następujące Twierdzenie o Dedukcji:

Twierdzenie o dedukcji

$\alpha\to\beta\in\textrm{Cn}_{i}(X)\;\;\iff\;\;\beta\in\textrm{Cn}_{i}(X\cup\{\alpha\})$

gdzie $\textrm{Cn}_{i}(X)$ oznacza zbiór formuł dowodliwych w INT ze zbioru założeń $X$ .

Jako ilustrację tego twierdzenia wykażemy dowodliwość w INT prawa przechodniości dla implikacji (p. 6. – wyżej):

1.	$q\in\textrm{Cn}_i(\{p\to q,\,q\to s,\,p\})$	reguła odrywania: $p\to q,\,p$
2.	$s\in\textrm{Cn}_i(\{p\to q,\,q\to s,\,p\})$	reguła odrywania: $q\to s,\,q$
3.	$p\to s\in\textrm{Cn}_i(\{p\to q,\,q\to s\})$	twierdzenie o dedukcji
4.	$(q\to s)\to(p\to s)\in\textrm{Cn}_i(\{p\to q\})$	twierdzenie o dedukcji
5.	$(p\to q)\to[(q\to s)\to(p\to s)]\in\textrm{Cn}_i(\emptyset)$	twierdzenie o dedukcji

Dowód tego faktu bez użycia twierdzenia o dedukcji zajmuje ponad 20 linii.

Przestrzegamy przy tym, że użycie twierdzenia o dedukcji pokazuje, iż istnieje dowód danej formuły w rachunku INT nie wskazując jednak tego dowodu eksplicite.

Twierdzenie o dedukcji w przedstawionej wyżej formie nazywa się także czasem klasycznym twierdzeniem o dedukcji w odróżnieniu od następującego uogólnionego twierdzenia o dedukcji:

Uogólnione twierdzenie o dedukcji

$\textrm{Cn}_{i}(X\cup\{\alpha\lor\beta\})=\textrm{Cn}_{i}(X\cup\{\alpha\})\cap\textrm{Cn}_{i}(X\cup\{\beta\})$
$\textrm{Cn}_{i}(X\cup\{\alpha\land\beta\})=\textrm{Cn}_{i}(X\cup\{\alpha,\beta\})$
$\neg\alpha\in\textrm{Cn}_{i}(X)\;\;\iff\;\;X\cup\{\alpha\} \mbox{ jest sprzeczny}$

gdzie zbiór formuł jest sprzeczny oznacza, ze można wywieść z niego dowolną formułę języka rachunku zdań.

jako przykład użycia tej wersji twierdzenia o dedukcji, wykażemy dowodliwość w INT prawa importacji (p. 7. – wyżej) oraz tzw. słabego prawa kontrapozycji: $(p\to q)\to(\neg q\to\neg p)$

Prawo importacji

1.	$s\in\textrm{Cn}_i(\{p\to(q\to s),\,p,\,q\})=\textrm{Cn}_i(\{p\to(q\to s),\,p\land q\})$
2.	$p\land q\to s\in\textrm{Cn}_i(\{p\to(q\to s)\})$
3.	$[p\to(q\to s)]\to(p\land q\to s)\in\textrm{Cn}_i(\emptyset)$

Słabe prawo kontrapozycji

1.	$q,\,\lnot q\in\textrm{Cn}_i(\{p\to q,\,\lnot q,\,p\})$
2.	$\{p\to q,\,\lnot q,\,p\} \mbox{ jest sprzeczny }$
3.	$\lnot p\in\textrm{Cn}_i(\{p\to q,\,\lnot q\})$
4.	$\lnot q\to\lnot p\in\textrm{Cn}_i(\{p\to q\})$
5.	$(p\to q)\to(\lnot q\to\lnot p)\in\textrm{Cn}_i(\emptyset)$