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
1
{\displaystyle _{1}}
α
→
(
β
→
α
)
{\displaystyle \alpha \to (\beta \to \alpha )}
prawo poprzedzania
Ax
2
{\displaystyle _{2}}
[
α
→
(
β
→
γ
)
]
→
[
(
α
→
β
)
→
(
α
→
γ
)
]
{\displaystyle [\alpha \to (\beta \to \gamma )]\to [(\alpha \to \beta )\to (\alpha \to \gamma )]}
sylogizm Fregego
Ax
3
{\displaystyle _{3}}
α
∧
β
→
α
{\displaystyle \alpha \wedge \beta \to \alpha }
prawo opuszczania koniunkcji, 1.
Ax
4
{\displaystyle _{4}}
α
∧
β
→
β
{\displaystyle \alpha \wedge \beta \to \beta }
prawo opuszczania koniunkcji, 2.
Ax
5
{\displaystyle _{5}}
(
α
→
β
)
→
[
(
α
→
γ
)
→
(
α
→
β
∧
γ
)
]
{\displaystyle (\alpha \to \beta )\to [(\alpha \to \gamma )\to (\alpha \to \beta \wedge \gamma )]}
prawo wprowadzania koniunkcji
Ax
6
{\displaystyle _{6}}
α
→
α
∨
β
{\displaystyle \alpha \to \alpha \vee \beta }
prawo wprowadzania alternatywy, 1.
Ax
7
{\displaystyle _{7}}
β
→
α
∨
β
{\displaystyle \beta \to \alpha \vee \beta }
prawo wprowadzania alternatywy, 2.
Ax
8
{\displaystyle _{8}}
(
β
→
α
)
→
[
(
γ
→
α
)
→
(
β
∨
γ
→
α
)
]
{\displaystyle (\beta \to \alpha )\to [(\gamma \to \alpha )\to (\beta \vee \gamma \to \alpha )]}
prawo łączenia implikacji
Ax
9
{\displaystyle _{9}}
(
α
↔
β
)
→
(
α
→
β
)
]
{\displaystyle (\alpha \leftrightarrow \beta )\to (\alpha \to \beta )]}
prawo opuszczania równoważności, 1.
Ax
10
{\displaystyle _{10}}
(
α
↔
β
)
→
(
β
→
α
)
]
{\displaystyle (\alpha \leftrightarrow \beta )\to (\beta \to \alpha )]}
prawo opuszczania równoważności, 2.
Ax
11
{\displaystyle _{11}}
(
α
→
β
)
→
[
(
β
→
α
)
→
(
α
↔
β
)
]
{\displaystyle (\alpha \to \beta )\to [(\beta \to \alpha )\to (\alpha \leftrightarrow \beta )]}
prawo wprowadzania równoważności
Ax
12
{\displaystyle _{12}}
α
→
(
¬
α
→
β
)
{\displaystyle \alpha \to (\neg \alpha \to \beta )}
prawo przepełnienia
Ax
13
{\displaystyle _{13}}
(
α
→
¬
α
)
→
¬
α
{\displaystyle (\alpha \to \neg \alpha )\to \neg \alpha }
prawo redukcji do absurdu
Ax
14
{\displaystyle _{14}}
¬
¬
α
→
α
{\displaystyle \neg \neg \alpha \to \alpha }
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
{
A
x
1
,
…
,
A
x
13
}
{\displaystyle \{\mathbf {Ax} _{1},\dots ,\mathbf {Ax} _{13}\}}
o formułę
A
x
14
.
{\displaystyle \mathbf {Ax} _{14}.}
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
A
x
12
−
A
x
14
{\displaystyle \mathbf {Ax} _{12}-\mathbf {Ax} _{14}}
przyjąć
Ax
12
′
{\displaystyle _{12}'}
(
α
→
β
)
→
(
¬
β
→
¬
α
)
{\displaystyle (\alpha \to \beta )\to (\neg \beta \to \neg \alpha )}
prawo kontrapozycji
Ax
13
′
{\displaystyle _{13}'}
α
↔
¬
¬
α
{\displaystyle \alpha \leftrightarrow \neg \neg \alpha }
prawo podwójnego przeczenia
Niektórzy autorzy wręcz ograniczają język KRZ np. do
→
{\displaystyle \to }
i
¬
{\displaystyle \neg }
traktując pozostałe spójniki jako wtórne:
Df
∨
{\displaystyle _{\vee }}
(
α
∨
β
)
:≡
(
¬
α
→
β
)
{\displaystyle (\alpha \vee \beta ):\equiv (\neg \alpha \to \beta )}
Df
∧
{\displaystyle _{\wedge }}
(
α
∧
β
)
:≡
¬
(
α
→
¬
β
)
{\displaystyle (\alpha \wedge \beta ):\equiv \neg (\alpha \to \neg \beta )}
Df
↔
{\displaystyle _{\leftrightarrow }}
(
α
↔
β
)
:≡
¬
[
(
α
→
β
)
→
¬
(
β
→
α
)
]
{\displaystyle (\alpha \leftrightarrow \beta ):\equiv \neg [(\alpha \to \beta )\to \neg (\beta \to \alpha )]}
Wówczas np. wykazanie prawa przemienności alternatywy sprowadza się do dowodliwości formuły
(
¬
α
→
β
)
↔
(
¬
β
→
α
)
,
{\displaystyle (\neg \alpha \to \beta )\leftrightarrow (\neg \beta \to \alpha ),}
a dowodliwość praw de Morgana , to dowodliwość formuł
¬
¬
(
α
→
¬
β
)
↔
(
¬
¬
α
→
¬
β
)
{\displaystyle \neg \neg (\alpha \to \neg \beta )\leftrightarrow (\neg \neg \alpha \to \neg \beta )}
oraz
¬
(
¬
α
→
β
)
↔
¬
(
¬
α
→
¬
¬
β
)
{\displaystyle \neg (\neg \alpha \to \beta )\leftrightarrow \neg (\neg \alpha \to \neg \neg \beta )}
W KRZ podobnie jak w INT prawdziwe są klasyczne Twierdzenie o dedukcji :
α
→
β
∈
Cn
c
(
X
)
⟺
β
∈
Cn
c
(
X
∪
{
α
}
)
{\displaystyle \alpha \to \beta \in {\textrm {Cn}}_{c}(X)\;\;\iff \;\;\beta \in {\textrm {Cn}}_{c}(X\cup \{\alpha \})}
oraz uogólnione twierdzenie o dedukcji :
Cn
c
(
X
∪
{
α
∨
β
}
)
=
Cn
c
(
X
∪
{
α
}
)
∩
Cn
c
(
X
∪
{
β
}
)
{\displaystyle {\textrm {Cn}}_{c}(X\cup \{\alpha \lor \beta \})={\textrm {Cn}}_{c}(X\cup \{\alpha \})\cap {\textrm {Cn}}_{c}(X\cup \{\beta \})}
Cn
c
(
X
∪
{
α
∧
β
}
)
=
Cn
c
(
X
∪
{
α
,
β
}
)
{\displaystyle {\textrm {Cn}}_{c}(X\cup \{\alpha \land \beta \})={\textrm {Cn}}_{c}(X\cup \{\alpha ,\beta \})}
¬
α
∈
Cn
c
(
X
)
⟺
X
∪
{
α
}
jest sprzeczny
{\displaystyle \neg \alpha \in {\textrm {Cn}}_{c}(X)\;\;\iff \;\;X\cup \{\alpha \}{\text{ jest sprzeczny}}}
gdzie
Cn
c
(
X
)
{\displaystyle {\textrm {Cn}}_{c}\,(X)}
oznacza zbiór formuł dowodliwych w KRZ ze zbioru założeń
X
.
{\displaystyle X.}
Wynika to z faktu, że w dowodzie obu tych twierdzeń korzysta się z aksjomatów o numerach nie przekraczających liczby
13.
{\displaystyle 13.}
W odróżnieniu jednak od INT, w przypadku KRZ trzeci punkt ostatniego twierdzenia może także przyjąć postać:
4.
α
∈
Cn
c
(
X
)
⟺
X
∪
{
¬
α
}
jest sprzeczny
{\displaystyle \alpha \in {\textrm {Cn}}_{c}(X)\;\;\iff \;\;X\cup \{\neg \alpha \}{\text{ jest sprzeczny}}}
Jako przykład użycia tej wersji twierdzenia o dedukcji, wykażemy dowodliwość w KRZ tzw. silnego prawa kontrapozycji :
(
¬
p
→
¬
q
)
→
(
q
→
p
)
{\displaystyle (\neg p\to \neg q)\to (q\to p)}
oraz prawa wyłączonego środka :
p
∨
¬
p
.
{\displaystyle p\vee \neg p.}
1.
q
,
¬
q
∈
Cn
c
(
{
¬
p
→
¬
q
,
q
,
¬
p
}
)
{\displaystyle q,\neg q\in {\textrm {Cn}}_{c}(\{\neg p\to \neg q\,,q,\,\neg p\})}
2.
Cn
c
(
{
¬
p
→
¬
q
,
q
,
¬
p
}
)
{\displaystyle {\textrm {Cn}}_{c}(\{\neg p\to \neg q\,,q,\,\neg p\})}
jest sprzeczny
3.
p
∈
Cn
c
(
{
¬
p
→
¬
q
,
q
}
)
{\displaystyle p\in {\textrm {Cn}}_{c}(\{\neg p\to \neg q\,,q\})}
4.
q
→
p
∈
Cn
c
(
{
¬
p
→
¬
q
}
)
{\displaystyle q\to p\in {\textrm {Cn}}_{c}(\{\neg p\to \neg q\})}
5.
(
¬
p
→
¬
q
)
→
(
q
→
p
)
∈
Cn
c
(
∅
)
{\displaystyle (\neg p\to \neg q)\to (q\to p)\in {\textrm {Cn}}_{c}(\emptyset )}
1.
p
→
p
∨
¬
p
∈
Cn
c
(
∅
)
{\displaystyle p\to p\vee \neg p\in {\textrm {Cn}}_{c}(\emptyset )}
2.
p
∨
¬
p
∈
Cn
c
(
{
p
}
)
{\displaystyle p\vee \neg p\in {\textrm {Cn}}_{c}(\{p\})}
3.
Cn
c
(
{
p
,
¬
(
p
∨
¬
p
)
}
)
{\displaystyle {\textrm {Cn}}_{c}(\{p,\neg (p\vee \neg p)\})}
– sprzeczny
4.
¬
p
∈
Cn
c
(
{
¬
(
p
∨
¬
p
)
}
)
{\displaystyle \neg p\in {\textrm {Cn}}_{c}(\{\neg (p\vee \neg p)\})}
5.
¬
p
→
p
∨
¬
p
∈
Cn
c
(
∅
)
{\displaystyle \neg p\to p\vee \neg p\in {\textrm {Cn}}_{c}(\emptyset )}
6.
p
∨
¬
p
∈
Cn
c
(
{
¬
p
}
)
{\displaystyle p\vee \neg p\in {\textrm {Cn}}_{c}(\{\neg p\})}
7.
Cn
c
(
{
¬
p
,
¬
(
p
∨
¬
p
)
}
)
{\displaystyle {\textrm {Cn}}_{c}(\{\neg p,\neg (p\vee \neg p)\})}
– sprzeczny
8.
¬
¬
p
∈
Cn
c
(
{
¬
(
p
∨
¬
p
)
}
)
{\displaystyle \neg \neg p\in {\textrm {Cn}}_{c}(\{\neg (p\vee \neg p)\})}
9.
Cn
c
(
{
¬
(
p
∨
¬
p
)
}
)
{\displaystyle {\textrm {Cn}}_{c}(\{\neg (p\vee \neg p)\})}
– sprzeczny
10.
p
∨
¬
p
∈
Cn
c
(
∅
)
{\displaystyle p\vee \neg p\in {\textrm {Cn}}_{c}(\emptyset )}
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
B
2
,
{\displaystyle {\mathcal {B}}_{2},}
czyli nie jest ona tautologią klasyczną.