命題論理（の上の理論）のメタ定理として，つぎのものは周知である：
| (T1) | (“演繹定理")
文φから文ψ(註1)が演繹されるとき，φ⊃ψは定理。
|
| (T2) | sen⊃sen1 と sen1⊃sen2 から，sen⊃sen2 が導かれる。
| | (T3) | sen と sen1 から sen∧sen1 が導かれる。
|
また，つぎの定理シェマも周知のものである：
(T4) sen⊃sen
(T5) sen⊃¬¬sen，¬¬sen⊃sen
(T6) ¬sen⊃(sen⊃sen1)
(T7) (sen⊃sen1)⊃(¬sen1⊃¬sen)
(T8) (sen⊃¬sen)⊃¬sen
(T9) (sen⊃sen11)∧(sen1⊃sen11) ⊃((sen∨sen1)⊃sen11)
ここでは，(T4) が既に証明されているときの(T1)(“演繹定理”）の証明と，(T1) から (T8) が既に証明されているときの (T9) の証明を示す(註2)。
“演繹定理”の証明については，それが〈φ⊃ψの証明作成の実効的手続き〉を示すものであるという点を，特に強調しておく。また，(T9)の証明は，変形規則適用の仕方のデモンストレーションを目的とする。
-
“演繹定理”の証明
φからのψの演繹が
φ＾θ1＾････＾θn-1＾ψ （θi は文）
であるとする。
θ1 は，
(1) 換言規則によってφから導かれる
(2) 公理
のいずれかである。(1) の場合，同じ換言規則によってφ⊃φからφ⊃θ1 が導かれる。φ⊃φが定理だからφ⊃θ1も定理。(2)の場合，θ1 と公理 θ1⊃(φ⊃θ1) (S1) に対する分離規則の適用で，φ⊃θ1 が定理として得られる。
いま，φ⊃θk（k＝1,････,i） が定理であるとする。
θi+1 の導出がθi に換言規則を適用することによる導出であるとき，同じ換言規則によってφ⊃θi からφ⊃θi+1 が導出される。仮定によりφ⊃θi は定理だから，φ⊃θi+1 も定理。
θi+1 の導出がθi に対する換言規則の適用によるものでないとき，つぎのいずれかが成り立っている：
- θi+1 は公理；
- 或る k＜i＋1 に対し，θi+1 はθk と同じ；
- 或る k＜i＋1 に対しθk がθi⊃θi+1 と同じで，θi とθi⊃θi+1 に対する分離規則の適用で，θi+1 が導出される；
- θi が或る k＜i に対する文θk⊃θi+1 であって，θk とθk⊃θi+1 に対する分離規則の適用で，θi+1 が導出される；
そしていずれの場合にも，φ⊃θi+1 は定理になる。
実際，(1) の場合，θi+1 と公理 θi+1⊃(φ⊃θi+1) (S1) に対する分離規則の適用で，定理φ⊃θi+1 を得る。
(2) の場合は，φ⊃θk が仮定から定理であることによる。
(3) の場合，仮定からφ⊃(θi⊃θi+1) は定理。公理(φ⊃(θi⊃θi+1))⊃((φ⊃θi)⊃(φ⊃θi+1)) より，(φ⊃θi)⊃(φ⊃θi+1) は定理。さらにφ⊃θi が仮定より定理であるから，φ⊃θi+1 も定理。
(4) の場合，仮定よりφ⊃(θk⊃θi+1) は定理。よって (3) と同じ考え方でφ⊃θi+1 が定理であることを得る。
-
(T9) の証明
| φ∨ψ(仮定) | ←─ | sen∨sen1
| | | ↓(C4)
| | ¬φ⊃ψ | ←─ | ¬sen⊃sen1
| | | ↓
| | ¬φ⊃ψ | ←─ | sen⊃sen1
| | & | | &
| | ψ⊃θ(仮定) | | sen1⊃sen11
| | | ↓(T2)
| | ¬φ⊃θ | ←─ | sen⊃sen11
| | ‖
| | ¬φ⊃θ | ←─ | sen11
| | & | | &
| | φ⊃θ(仮定) | | sen⊃sen1
| | | ↓(T7),(MP)
| | ¬φ⊃θ | ←─ | sen11
| | & | | &
| | ¬θ⊃¬φ | | ¬sen1⊃¬sen
| | ‖
| | ¬φ⊃θ | ←─ | sen1⊃sen11
| | & | | &
| | ¬θ⊃¬φ | | sen⊃sen1
| | | ↓(T2)
| | ¬θ⊃θ | ←─ | sen⊃sen11
| | ‖
| | ¬θ⊃θ | ←─ | sen1⊃sen
| | | ↓(C1)
| | ¬θ⊃¬¬θ | ←─ | sen1⊃¬¬sen
| | | ↓(T8)
| | ¬θ⊃¬¬θ | ←─ | sen1
| | & | | &
| | (¬θ⊃¬¬θ)⊃¬¬θ | | (sen⊃¬sen)⊃¬sen
| | ‖
| | ¬θ⊃¬¬θ | ←─ | sen
| | & | | &
| | (¬θ⊃¬¬θ)⊃¬¬θ | | sen⊃sen1
| | | ↓(MP)
| | ¬¬θ | ←─ | sen1
| | ‖
| | ¬¬θ | ←─ | ¬¬sen
| | | ↓(C1)
| | θ | ←─ | sen
|
(T1) の“演繹定理”により，結局，φ⊃θとψ⊃θから (φ∧ψ)⊃θ が導かれる。
（註１） φ，ψはメタ記号。“演繹定理”の証明の中のφ，ψ，θ，θ1，θn-1，θi，および (T9)の証明の中のφ，ψ，θも同様。
（註２） (T1)から(T8)は，依存関係に従って，例えば (T4), (T5), (T1), (T5), (T6), (T7), (T8), (T3) の順番で証明される。
|