Twierdzenie o dedukcji – jeżeli
A
{\displaystyle A}
B
∈
Cn
L
(
X
∪
{
A
}
)
{\displaystyle B\in \operatorname {Cn} _{L}(X\cup \{A\})}
formuła zdaniowa
A
→
B
{\displaystyle A\rightarrow B}
Cn
L
(
X
)
{\displaystyle \operatorname {Cn} _{L}(X)}
Cn
L
(
X
)
{\displaystyle \operatorname {Cn} _{L}(X)}
zbiór wszystkich konsekwencji logicznych zbioru formuł zdaniowych
X
{\displaystyle X}
Definicja formalna [ edytuj ] Niech
L
{\displaystyle {\mathcal {L}}}
klasycznego rachunku zdań i niech
S
{\displaystyle {\mathcal {S}}}
rachunkiem zdaniowym w tym języku.
Klasycznym twierdzeniem o dedukcji
S
{\displaystyle {\mathcal {S}}}
Dla dowolnego zbioru formuł
X
{\displaystyle X\,}
L
{\displaystyle {\mathcal {L}}}
α
,
β
{\displaystyle \alpha ,\beta \,}
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 }
F
r
m
(
L
K
R
Z
)
{\displaystyle \mathbf {Frm} ({\mathcal {L}}_{\mathbf {KRZ} })}
r
o
{\displaystyle \mathbf {r_{o}} }
r
⋆
{\displaystyle \mathbf {r} _{\star }}
A
x
K
R
Z
{\displaystyle \mathbf {Ax} _{\mathbf {KRZ} }}
Wówczas
N
C
p
p
∈
C
n
S
(
{
q
}
)
{\displaystyle \mathbf {NCpp} \in \mathbf {Cn} _{\mathfrak {S}}(\{\mathbf {q} \})}
C
q
N
C
p
p
∈
C
n
S
(
∅
)
{\displaystyle \mathbf {CqNCpp} \in \mathbf {Cn} _{\mathfrak {S}}(\emptyset )}
C
n
S
(
∅
)
=
C
n
c
(
∅
)
{\displaystyle \mathbf {Cn} _{\mathfrak {S}}(\emptyset )=\mathbf {Cn} _{c}(\emptyset )}
C
q
N
C
p
p
{\displaystyle \mathbf {CqNCpp} }
Klasyczne twierdzenie o dedukcji jest prawdziwe m.in. w klasycznym i intuicjonistycznym rachunku zdań oraz w rachunku predykatów w ujęciu Endertona .
