Klasyczny rachunek zdań – najpopularniejszy system formalny logiki matematycznej, w którym formuły reprezentujące zdania logiczne mogą być tworzone z formuł atomowych za pomocą wymienionego niżej zbioru aksjomatów.
Klasyczny rachunek zdań, KRZ, 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
|
Ax
|
silne prawo podwójnego przeczenia
|
Związek z intuicjonistycznym rachunkiem zdań[edytuj | edytuj kod]
W tej formie aksjomatyka ta jest rozszerzeniem aksjomatyki intuicjonistycznego rachunku zdań, którą stanowią formuły
o formułę
Przykłady dowodu w systemie formalnym klasycznego rachunku zdań znaleźć można w artykule dot.
intuicjonistycznego rachunku zdań. Ponieważ KRZ jest rozszerzeniem INT tylko o jeden aksjomat,
zamieszczone tam dowody są także poprawnymi dowodami w klasycznym rachunku zdań.
Gdyby chcieć uprawiać KRZ w oderwaniu od INT, można zamiast aksjomatów
przyjąć
Ax
|
prawo kontrapozycji
|
Ax
|
prawo podwójnego przeczenia
|
Niektórzy autorzy wręcz ograniczają język KRZ np. do
i
traktując pozostałe spójniki jako wtórne:
Df
|
Df
|
Df
|
Wówczas np. wykazanie prawa przemienności alternatywy sprowadza się do dowodliwości formuły
a dowodliwość praw de Morgana, to dowodliwość formuł
![{\displaystyle \neg \neg (\alpha \to \neg \beta )\leftrightarrow (\neg \neg \alpha \to \neg \beta )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8e0784f9cd2d2441af5b1bedd4420d047331c1b2)
oraz
![{\displaystyle \neg (\neg \alpha \to \beta )\leftrightarrow \neg (\neg \alpha \to \neg \neg \beta )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/17f14ffe16aedbc472a0b03f68cc13eb4baeb786)
W KRZ podobnie jak w INT prawdziwe są klasyczne Twierdzenie o dedukcji:
![{\displaystyle \alpha \to \beta \in {\textrm {Cn}}_{c}(X)\;\;\iff \;\;\beta \in {\textrm {Cn}}_{c}(X\cup \{\alpha \})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/367a9f97a773e14e47d040112d4004945e8c046c)
oraz uogólnione twierdzenie o dedukcji:
![{\displaystyle {\textrm {Cn}}_{c}(X\cup \{\alpha \lor \beta \})={\textrm {Cn}}_{c}(X\cup \{\alpha \})\cap {\textrm {Cn}}_{c}(X\cup \{\beta \})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/446a0db7e1c73b148945d387003a3aa7d801e695)
![{\displaystyle {\textrm {Cn}}_{c}(X\cup \{\alpha \land \beta \})={\textrm {Cn}}_{c}(X\cup \{\alpha ,\beta \})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e95d3745790d562b5532de301cddf53492869157)
![{\displaystyle \neg \alpha \in {\textrm {Cn}}_{c}(X)\;\;\iff \;\;X\cup \{\alpha \}{\text{ jest sprzeczny}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/31df83cf31975c6bb15aa33853558b2358549dd7)
gdzie
oznacza zbiór formuł dowodliwych w KRZ ze zbioru założeń
Wynika to z faktu, że w dowodzie obu tych twierdzeń korzysta się z aksjomatów o numerach nie przekraczających liczby
W odróżnieniu jednak od INT, w przypadku KRZ trzeci punkt ostatniego twierdzenia może także przyjąć postać:
- 4.
![{\displaystyle \alpha \in {\textrm {Cn}}_{c}(X)\;\;\iff \;\;X\cup \{\neg \alpha \}{\text{ jest sprzeczny}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0ff3673a9ccf06e341dfa95c5ae553ae1c84cc7a)
Jako przykład użycia tej wersji twierdzenia o dedukcji, wykażemy dowodliwość w KRZ tzw. silnego prawa kontrapozycji:
![{\displaystyle (\neg p\to \neg q)\to (q\to p)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4a3e269db70453359b0db5a71a861aca67164920)
oraz prawa wyłączonego środka:
![{\displaystyle p\vee \neg p.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/49d957561fab33a3d0d40536070547903f8dcd10)
1.
|
|
2.
|
|
jest sprzeczny
|
3.
|
|
4.
|
|
5.
|
|
1.
|
|
2.
|
|
3.
|
|
– sprzeczny
|
4.
|
|
5.
|
|
6.
|
|
7.
|
|
– sprzeczny
|
8.
|
|
9.
|
|
– sprzeczny
|
10.
|
|
Formuła języka klasycznego rachunku zdań jest tezą KRZ jeśli jest ona prawdziwa dowolnej algebrze Boole’a.
W szczególności jeśli formuła nie jest tezą KRZ, to można ją obalić w dwuelementowej algebrze Boole’a
czyli nie jest ona tautologią klasyczną.