Twierdzenie o dedukcji

Twierdzenie o dedukcji – jeżeli ${\displaystyle A}$ jest zdaniem oraz ${\displaystyle B\in \operatorname {Cn} _{L}(X\cup \{A\}),}$ to formuła zdaniowa ${\displaystyle A\to B}$ należy do zbioru ${\displaystyle \operatorname {Cn} _{L}(X),}$ gdzie ${\displaystyle \operatorname {Cn} _{L}(X)}$ to zbiór wszystkich konsekwencji logicznych zbioru formuł zdaniowych ${\displaystyle X.}$

Definicja formalna

Niech ${\displaystyle {\mathcal {L}}}$ będzie jakimkolwiek językiem rozszerzającym język klasycznego rachunku zdań i niech ${\displaystyle {\mathcal {S}}}$ będzie rachunkiem zdaniowym w tym języku.

Klasycznym twierdzeniem o dedukcji dla rachunku ${\displaystyle {\mathcal {S}}}$ nazywamy następujące stwierdzenie:

Dla dowolnego zbioru formuł ${\displaystyle X}$ języka ${\displaystyle {\mathcal {L}}}$ oraz dwu formuł ${\displaystyle \alpha ,\beta }$ zachodzi równoważność:

${\displaystyle \mathbf {C} \alpha \beta \in \mathbf {Cn} _{\mathfrak {S}}(X)\quad \Leftrightarrow \quad \beta \in \mathbf {Cn} _{\mathfrak {S}}(X\cup \{\alpha \}).}$

Prawdziwość twierdzenia o dedukcji wymaga wyprowadzalności reguły odrywania dla spójnika implikacji ${\displaystyle \mathbf {C} .}$

Wyprowadzalność tej reguły nie jest niestety warunkiem wystarczającym do jego prawdziwości.

Niech bowiem

${\displaystyle {\mathfrak {S}}=\langle \mathbf {Frm} ({\mathcal {L}}_{\mathbf {KRZ} }),\{\mathbf {r_{o}} ,\mathbf {r} _{\star }\},\mathbf {Ax} _{\mathbf {KRZ} }\rangle ,}$

gdzie:

${\displaystyle \mathbf {Frm} ({\mathcal {L}}_{\mathbf {KRZ} })}$ – zbiór formuł języka klasycznego rachunku zdań,

${\displaystyle \mathbf {r_{o}} }$ – reguła odrywania dla spójnika implikacji,

${\displaystyle \mathbf {r} _{\star }}$ – reguła podstawiania dla języka klasycznego rachunku zdań,

${\displaystyle \mathbf {Ax} _{\mathbf {KRZ} }}$ – zbiór aksjomatów klasycznego rachunku zdań.

Wówczas

${\displaystyle \mathbf {NCpp} \in \mathbf {Cn} _{\mathfrak {S}}(\{\mathbf {q} \}),}$ chociaż w żadnym wypadku nie jest prawdą, że

${\displaystyle \mathbf {CqNCpp} \in \mathbf {Cn} _{\mathfrak {S}}(\emptyset ),}$ bo

${\displaystyle \mathbf {Cn} _{\mathfrak {S}}(\emptyset )=\mathbf {Cn} _{c}(\emptyset ),}$ a ${\displaystyle \mathbf {CqNCpp} }$ nie jest tautologią.

Klasyczne twierdzenie o dedukcji jest prawdziwe m.in. w klasycznym i intuicjonistycznym rachunku zdań oraz w rachunku predykatów w ujęciu Endertona.

Zobacz też

• rachunek zdaniowy
• system formalny