Twierdzenie o dedukcji

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

Definicja formalna

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

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

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

$\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 $\mathbf {C} .$

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

Niech bowiem

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

gdzie:

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

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

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

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

Wówczas

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

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

$\mathbf {Cn} _{\mathfrak {S}}(\emptyset )=\mathbf {Cn} _{c}(\emptyset ),$ a $\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