演繹定理の証明
演繹定理（Deduction Theorem）
A1, …, An-1, An → B なら A1, …, An-1 → An⊃B
A1, …, An-1 → An⊃B なら A1, …, An-1, An → B
１）証明とは何か、仮定からの演繹とは何か、を確認する。
「証明」とは、有限な式の列を言う。その式の列の各行は、
a) 公理であるか、
b) それ以前の式に推理規則（A と A⊃B から B を得る）を適用した式であるか、
のどちらかである。
この式の列の最後の式を定理といい、この式の列をその定理の証明という。
「仮定（A1,…,An-1,An）からの（Bの）演繹」とは、次のような式の列を言う。その式の列の各行は、
a) 公理であるか、
b) 仮定（A1,…,An-1,An）のどれかであるか、
c) それ以前の式に推理規則を適用した式であるか、
のどれかである。
このとき、式 B は仮定 A1,…,An-1,An から演繹されたという。
２）演繹定理とは何か？
（略）
３）演繹定理の証明
（１）A1,…,An-1,An→B なら A1,…,An-1→An⊃B を証明する。
いま、A1,…,An-1,An→B が成立していると仮定する。
すると、Ｂの式の証明が存在する。それを C1,C2,…,Cm とする。（CmがB である。）
a) 今この式の列の中の任意の Ci について、i＝1 の時
C1 は、(１)公理か、(2)仮定（A1,…,An-1）の一つであるか、(3)An そのものである。
(１)公理と(2)仮定（A1,…,An-1,）の場合、
それぞれ →C1 A1,…,An-1→C1 であるから
公理1 →C1⊃（An⊃C1） と推理規則（MP）によって
A1,…,An-1→An⊃C1 つまり
A1,…,An-1→An⊃B
(3)Anの場合、
定理によって An⊃An（=C1） だから、 →An⊃C1
つまり A1,…,An-1→An⊃Ci
b) i＞1 の時
いま任意の式 Ci について、それ以前の式 Ck については、数学的帰納法の仮定として、
A1,…,An-1→An⊃Ck が成立していると仮定する。
すると次の四つの場合が考えられる。
(1) Ci は、公理である
(2) Ci は、仮定（A1,…,An-1,An）のどれかである
(3) Ci は、Anそのものである
(4) Ci は、それ以前の式に推理規則（A と A⊃B
から B を得る）を適用した式である
(1)(2)(3)の場合は、i＝1 の場合と同じ。
(4)の場合、
Ci はそれ以前の式 Ch と Cj から推理規則によって得られたとする。
すると、そのどちらか一方（Cj とする）は、Ch⊃ Ci という形をしているはずである。
帰納法の仮定により A1,…,An-1 → An⊃Ch (x)
及び A1,…,An-1 → An⊃（Ch⊃Ci） (y)
公理2 →（An⊃（Ch⊃Cj））⊃（（An⊃Ch）⊃（An⊃Cj） を使って(y)から
A1,…,An-1 → （An⊃Ch）⊃（An⊃Ci） (z)
推理規則により(x)と(z)から A1,…,An-1 → An⊃Ci
a)とｂ）から
A1,…,An-1,An→B を証明する式の列（C1,C2,…,Cm ）のどれにおいても、それに対応して
A1,…,An-1→An⊃B を証明する式の列（An⊃C1,An⊃C2,…,An⊃Cm ）が存在する。ゆえに、
A1,…,An-1,An → B なら A1,…,An-1 → An⊃B
（２）A1,…,An-1→An⊃B なら A1,…,An-1,An→B を証明する。
いま、A1,…,An-1 → An⊃B が成立していると仮定する。
すると、An⊃Ｂの式の証明が存在する。それを C1,C2,…,Cm とする。（CmがAn⊃Bである。）
この式の列に Cm+1,Cm+2 として、An とB を加える。
この新たな式の列は A1,…,An-1,Anという仮定の下での B の証明である。
（Anは仮定であり、An⊃B とAn からMPにより B が得られる。）
つまり、A1,…,An-1,An → B