Twierdzenie o dedukcji

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

Definicja formalna

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

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

Dla dowolnego zbioru formuł $X\,$$X\,$ języka ${\mathcal {L}}$$\mathcal{L}$ oraz dwu formuł $\alpha ,\beta \,$$\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 \})$$\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}$$\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$${\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} })$$\mathbf {Frm} ({\mathcal {L}}_{\mathbf {KRZ} })$ jest zbiorem formuł języka klasycznego rachunku zdań, $\mathbf {r_{o}}$$\mathbf {r_{o}}$ jest regułą odrywania dla spójnika implikacji, $\mathbf {r} _{\star }$$\mathbf {r} _{\star }$ jest regułą podstawiania dla języka klasycznego rachunku zdań oraz $\mathbf {Ax} _{\mathbf {KRZ} }$$\mathbf {Ax} _{\mathbf {KRZ} }$ jest zbiorem aksjomatów klasycznego rachunku zdań.

Wówczas $\mathbf {NCpp} \in \mathbf {Cn} _{\mathfrak {S}}(\{\mathbf {q} \})$$\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 )$$\mathbf {CqNCpp} \in \mathbf {Cn} _{\mathfrak {S}}(\emptyset )$, bo $\mathbf {Cn} _{\mathfrak {S}}(\emptyset )=\mathbf {Cn} _{c}(\emptyset )$$\mathbf {Cn} _{\mathfrak {S}}(\emptyset )=\mathbf {Cn} _{c}(\emptyset )$, a $\mathbf {CqNCpp}$$\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