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