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 (\mathrm{\neg }\alpha \to \beta )$	prawo przepełnienia
Ax${}_{13}$   $(\alpha \to \mathrm{\neg }\alpha )\to \mathrm{\neg }\alpha$	prawo redukcji do absurdu

Zwracamy uwagę na brak (silnego) prawa podwójnego przeczenia: $\mathrm{\neg }\mathrm{\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 \mathrm{\neg }\mathrm{\neg }p$	słabe prawo podwójnego przeczenia
3.	$(p\to q)\to (\mathrm{\neg }q\to \mathrm{\neg }p)$	słabe prawo kontrapozycji
4.	$(p\to \mathrm{\neg }q)\to (q\to \mathrm{\neg }p)$	słabe prawo transpozycji
5.	$\mathrm{\neg }(p\vee q)\leftrightarrow (\mathrm{\neg }q\wedge \mathrm{\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 \mathrm{\neg }\mathrm{\neg }p$

1.	$(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p$	Ax${}_{13}$
2.	$[(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p]\to \{p\to [(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p]\}$	Ax${}_1$
3.	$p\to (\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p$	reguła odrywania: 1,3
4.	$\{p\to [(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p\}\to \{[p\to (\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)]\to (p\to \mathrm{\neg }\mathrm{\neg }p)\}$	Ax${}_2$
5.	$[p\to (\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)]\to (p\to \mathrm{\neg }\mathrm{\neg }p)$	reguła odrywania: 3,4
6.	$p\to (\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)$	Ax${}_{12}$
7.	$p\to \mathrm{\neg }\mathrm{\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 {\text{Cn}}_i(X)⟺\beta \in {\text{Cn}}_i(X\cup \{\alpha \})$

gdzie ${\text{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 {\text{Cn}}_i(\{p\to q,q\to s,p\})$	reguła odrywania: $p\to q,p$
2.	$s\in {\text{Cn}}_i(\{p\to q,q\to s,p\})$	reguła odrywania: $q\to s,q$
3.	$p\to s\in {\text{Cn}}_i(\{p\to q,q\to s\})$	twierdzenie o dedukcji
4.	$(q\to s)\to (p\to s)\in {\text{Cn}}_i(\{p\to q\})$	twierdzenie o dedukcji
5.	$(p\to q)\to [(q\to s)\to (p\to s)]\in {\text{Cn}}_i(\mathrm{\varnothing })$	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. ${\text{Cn}}_i(X\cup \{\alpha \vee \beta \})={\text{Cn}}_i(X\cup \{\alpha \})\cap {\text{Cn}}_i(X\cup \{\beta \})$
2. ${\text{Cn}}_i(X\cup \{\alpha \wedge \beta \})={\text{Cn}}_i(X\cup \{\alpha ,\beta \})$
3. $\mathrm{\neg }\alpha \in {\text{Cn}}_i(X)⟺X\cup \{\alpha \}\text{ 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 (\mathrm{\neg }q\to \mathrm{\neg }p)$

Prawo importacji

1.	$s\in {\text{Cn}}_i(\{p\to (q\to s),p,q\})={\text{Cn}}_i(\{p\to (q\to s),p\wedge q\})$
2.	$p\wedge q\to s\in {\text{Cn}}_i(\{p\to (q\to s)\})$
3.	$[p\to (q\to s)]\to (p\wedge q\to s)\in {\text{Cn}}_i(\mathrm{\varnothing })$

Słabe prawo kontrapozycji

1.	$q,\mathrm{\neg }q\in {\text{Cn}}_i(\{p\to q,\mathrm{\neg }q,p\})$
2.	$\{p\to q,\mathrm{\neg }q,p\}\text{ jest sprzeczny }$
3.	$\mathrm{\neg }p\in {\text{Cn}}_i(\{p\to q,\mathrm{\neg }q\})$
4.	$\mathrm{\neg }q\to \mathrm{\neg }p\in {\text{Cn}}_i(\{p\to q\})$
5.	$(p\to q)\to (\mathrm{\neg }q\to \mathrm{\neg }p)\in {\text{Cn}}_i(\mathrm{\varnothing })$

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ń