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
|
prawo poprzedzania
|
Ax
|
sylogizm Fregego
|
Ax
|
prawo opuszczania koniunkcji, 1.
|
Ax
|
prawo opuszczania koniunkcji, 2.
|
Ax
|
prawo wprowadzania koniunkcji
|
Ax
|
prawo wprowadzania alternatywy, 1.
|
Ax
|
prawo wprowadzania alternatywy, 2.
|
Ax
|
prawo łączenia implikacji
|
Ax
|
prawo opuszczania równoważności, 1.
|
Ax
|
prawo opuszczania równoważności, 2.
|
Ax
|
prawo wprowadzania równoważności
|
Ax
|
prawo przepełnienia
|
Ax
|
prawo redukcji do absurdu
|
Zwracamy uwagę na brak (silnego) prawa podwójnego przeczenia:
którego dodanie do aksjomatyki INT tworzy aksjomatykę klasycznego rachunku zdań.
W rachunku intuicjonistycznym dowodliwe są m.in. następujące formuły:
1.
|
|
prawo identyczności
|
2.
|
|
słabe prawo podwójnego przeczenia
|
3.
|
|
słabe prawo kontrapozycji
|
4.
|
|
słabe prawo transpozycji
|
5.
|
|
prawo de Morgana, 2.
|
6.
|
|
prawo przechodniości
|
7.
|
|
prawo importacji
|
8.
|
|
prawo eksportacji
|
Dla przykładu zaprezentujemy dowód formuł 1. i 2. w rachunku INT:
- Prawo identyczności
![{\displaystyle p\to p}](https://wikimedia.org/api/rest_v1/media/math/render/svg/edf3d9dfaa106174c31fe6f412ad65c67ea3afbe)
1.
|
|
Ax
|
2.
|
|
Ax
|
3.
|
|
reguła odrywania: 1,2
|
4.
|
|
Ax
|
5.
|
|
reguła odrywania: 3,4
|
- Słabe prawo podwójnego przeczenia
![{\displaystyle p\to \neg \neg p}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fb56efba4129a7fd9ef620e17746d3e1c561dac9)
1.
|
|
Ax
|
2.
|
|
Ax
|
3.
|
|
reguła odrywania: 1,3
|
4.
|
|
Ax
|
5.
|
|
reguła odrywania: 3,4
|
6.
|
|
Ax
|
7.
|
|
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
-
![{\displaystyle \alpha \to \beta \in {\textrm {Cn}}_{i}(X)\;\;\iff \;\;\beta \in {\textrm {Cn}}_{i}(X\cup \{\alpha \})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ac76e0207ca628a7321a9e91a80136dd085d5ebf)
gdzie
oznacza zbiór formuł dowodliwych w INT ze zbioru założeń
Jako ilustrację tego twierdzenia wykażemy dowodliwość w INT prawa przechodniości dla implikacji (p. 6. – wyżej):
1.
|
|
reguła odrywania:
|
2.
|
|
reguła odrywania:
|
3.
|
|
twierdzenie o dedukcji
|
4.
|
|
twierdzenie o dedukcji
|
5.
|
|
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
![{\displaystyle {\textrm {Cn}}_{i}(X\cup \{\alpha \lor \beta \})={\textrm {Cn}}_{i}(X\cup \{\alpha \})\cap {\textrm {Cn}}_{i}(X\cup \{\beta \})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c1d699e1fad25647ffdb971898e08ccd10de8d40)
![{\displaystyle {\textrm {Cn}}_{i}(X\cup \{\alpha \land \beta \})={\textrm {Cn}}_{i}(X\cup \{\alpha ,\beta \})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c14c4f645858558c7a4d144a4d8c7d625a32c9c4)
![{\displaystyle \neg \alpha \in {\textrm {Cn}}_{i}(X)\;\;\iff \;\;X\cup \{\alpha \}{\mbox{ jest sprzeczny}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b94b3712b94d6dc5b5b7ee1b8b77636a41c042e3)
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:
- Prawo importacji
1.
|
|
2.
|
|
3.
|
|
- Słabe prawo kontrapozycji
1.
|
|
2.
|
|
3.
|
|
4.
|
|
5.
|
|
Zarówno klasyczne twierdzenie o dedukcji, jak i jego uogólniona wersja prawdziwe są w klasycznym rachunku zdań.