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 explicite.

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

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

gdzie zbiór formuł jest sprzeczny oznacza, że 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 )$

Zarówno klasyczne twierdzenie o dedukcji, jak i jego uogólniona wersja prawdziwe są w klasycznym rachunku zdań.

Zobacz też

• logika intuicjonistyczna
• semantyka algebraiczna
• semantyka Kripkego intuicjonistycznego rachunku zdań