Z Wikipedii, wolnej encyklopedii
Twierdzenie o dedukcji – jeżeli
jest zdaniem oraz
to formuła zdaniowa
należy do zbioru
gdzie
to zbiór wszystkich konsekwencji logicznych zbioru formuł zdaniowych
Niech
będzie jakimkolwiek językiem rozszerzającym język klasycznego rachunku zdań i niech
będzie rachunkiem zdaniowym w tym języku.
Klasycznym twierdzeniem o dedukcji dla rachunku
nazywamy następujące stwierdzenie:
- Dla dowolnego zbioru formuł
języka
oraz dwu formuł
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 \}).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fafcfcee67d10112d9f4b1f044b85fbc72399fc4)
Prawdziwość twierdzenia o dedukcji wymaga wyprowadzalności reguły odrywania dla spójnika implikacji
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 ,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/df2673f7d5bd518aa3eaaf5bca42a8ca3c7b7113)
gdzie:
– zbiór formuł języka klasycznego rachunku zdań,
– reguła odrywania dla spójnika implikacji,
– reguła podstawiania dla języka klasycznego rachunku zdań,
– zbiór aksjomatów klasycznego rachunku zdań.
Wówczas
chociaż w żadnym wypadku nie jest prawdą, że
bo
a
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.