Intuicjonistyczny rachunek zdań

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacji, wyszukiwania

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

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, ze 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ż[edytuj | edytuj kod]