Twierdzenie o dedukcji

Poglądowo

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

Formalnie

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})$ jest zbiorem formuł języka klasycznego rachunku zdań, $\mathbf{r_o}$ jest regułą odrywania dla spójnika implikacji, $\mathbf{r}_\star$ jest regułą podstawiania dla języka klasycznego rachunku zdań oraz $\mathbf{Ax}_\mathbf{KRZ}$ jest zbiorem 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