Twierdzenie o dedukcji – jeżeli
A
{\displaystyle A}
jest zdaniem oraz
B
∈
Cn
L
(
X
∪
{
A
}
)
{\displaystyle B\in \operatorname {Cn} _{L}(X\cup \{A\})}
, to formuła zdaniowa
A
→
B
{\displaystyle A\rightarrow B}
należy do zbioru
Cn
L
(
X
)
{\displaystyle \operatorname {Cn} _{L}(X)}
, gdzie
Cn
L
(
X
)
{\displaystyle \operatorname {Cn} _{L}(X)}
to zbiór wszystkich konsekwencji logicznych zbioru formuł zdaniowych
X
{\displaystyle X}
.
Niech
L
{\displaystyle {\mathcal {L}}}
będzie jakimkolwiek językiem rozszerzającym język klasycznego rachunku zdań i niech
S
{\displaystyle {\mathcal {S}}}
będzie rachunkiem zdaniowym w tym języku.
Klasycznym twierdzeniem o dedukcji dla rachunku
S
{\displaystyle {\mathcal {S}}}
nazywamy następujące stwierdzenie:
Dla dowolnego zbioru formuł
X
{\displaystyle X\,}
języka
L
{\displaystyle {\mathcal {L}}}
oraz dwu formuł
α
,
β
{\displaystyle \alpha ,\beta \,}
zachodzi równoważność:
C
α
β
∈
C
n
S
(
X
)
⇔
β
∈
C
n
S
(
X
∪
{
α
}
)
{\displaystyle \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
C
{\displaystyle \mathbf {C} }
.
Wyprowadzalność tej reguły nie jest niestety warunkiem wystarczającym do jego prawdziwości.
Niech bowiem
S
=
⟨
F
r
m
(
L
K
R
Z
)
,
{
r
o
,
r
⋆
}
,
A
x
K
R
Z
⟩
{\displaystyle {\mathfrak {S}}=\langle \mathbf {Frm} ({\mathcal {L}}_{\mathbf {KRZ} }),\{\mathbf {r_{o}} ,\mathbf {r} _{\star }\},\mathbf {Ax} _{\mathbf {KRZ} }\rangle }
, gdzie
F
r
m
(
L
K
R
Z
)
{\displaystyle \mathbf {Frm} ({\mathcal {L}}_{\mathbf {KRZ} })}
jest zbiorem formuł języka klasycznego rachunku zdań,
r
o
{\displaystyle \mathbf {r_{o}} }
jest regułą odrywania dla spójnika implikacji,
r
⋆
{\displaystyle \mathbf {r} _{\star }}
jest regułą podstawiania dla języka klasycznego rachunku zdań oraz
A
x
K
R
Z
{\displaystyle \mathbf {Ax} _{\mathbf {KRZ} }}
jest zbiorem aksjomatów klasycznego rachunku zdań.
Wówczas
N
C
p
p
∈
C
n
S
(
{
q
}
)
{\displaystyle \mathbf {NCpp} \in \mathbf {Cn} _{\mathfrak {S}}(\{\mathbf {q} \})}
, chociaż w żadnym wypadku nie jest prawdą, że
C
q
N
C
p
p
∈
C
n
S
(
∅
)
{\displaystyle \mathbf {CqNCpp} \in \mathbf {Cn} _{\mathfrak {S}}(\emptyset )}
, bo
C
n
S
(
∅
)
=
C
n
c
(
∅
)
{\displaystyle \mathbf {Cn} _{\mathfrak {S}}(\emptyset )=\mathbf {Cn} _{c}(\emptyset )}
, a
C
q
N
C
p
p
{\displaystyle \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 .