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:
{| cellspacing=25 | 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: {| cellspacing=15 | 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 {| cellspacing=15 | 1.
| Ax |- | 2. | | Ax |- | 3. | | reguła odrywania: 1,2 |- | 4. | | Ax |- | 5. | | reguła odrywania: 3,4
Słabe prawo podwójnego przeczenia {| cellspacing=15 | 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
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
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 {| cellspacing=15 | 1.
| 2.
| 3.
Słabe prawo kontrapozycji {| cellspacing=15 | 1.
| 2.
| 3.
| 4.
| 5.
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ń
Kategoria:Logika matematyczna