Twierdzenie o dedukcji

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

Definicja formalna

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ł $X$ języka $ℒ$ oraz dwu formuł $α, β$ zachodzi równoważność:

𝐂 α β \in {𝐂 𝐧}_{𝔖} (X) \Leftrightarrow β \in {𝐂 𝐧}_{𝔖} (X \cup {α}) .

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

𝔖 = ⟨ 𝐅 𝐫 𝐦 (ℒ_{𝐊 𝐑 𝐙}), {𝐫_{𝐨}, 𝐫_{⋆}}, {𝐀 𝐱}_{𝐊 𝐑 𝐙} ⟩,

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

𝐍 𝐂 𝐩 𝐩 \in {𝐂 𝐧}_{𝔖} ({𝐪}),

chociaż w żadnym wypadku nie jest prawdą, że

𝐂 𝐪 𝐍 𝐂 𝐩 𝐩 \in {𝐂 𝐧}_{𝔖} (\emptyset),

bo

{𝐂 𝐧}_{𝔖} (\emptyset) = {𝐂 𝐧}_{c} (\emptyset),

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.