Intuicjonistyczny rachunek zdań

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

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:

1.    Ax
2.    Ax
3.    reguła odrywania: 1,2
4.    Ax
5.    reguła odrywania: 3,4

Słabe prawo podwójnego przeczenia:

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

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

Zobacz też[edytuj]