Twierdzenie o dedukcji

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacji, wyszukiwania

Poglądowo[edytuj | edytuj kod]

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[edytuj | edytuj kod]

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 klasycznymintuicjonistycznym rachunku zdań oraz w rachunku predykatów w ujęciu Endertona.

Zobacz też[edytuj | edytuj kod]