数学の基礎

　本文第１節で導入した自然推論の推論体系は、論理記号を導入する推論規則と消去する推論規則に分かれていますが、“最も効率のよい証明は何か”という問題を考える際は、折角導入した命題を“消去”してしまうというのはムダであり、消去という操作が一切出てこない証明が得られれば、それが最も効率がよい証明ということになります。
　そこで、消去規則を、それと同等な、ある種の“導入”規則に置き換えることを考えてみましょう。

　一般に、直観主義論理における論理記号 s の消去規則は次の形をしています：

(A3-1)

Γ ® As Γ1 ® P1 ¼  Γn ® Pn ————–  Γ ® Q

　ただし A_s は論理記号 s を陽に含む唯一の命題を表し、Γ_i は Γ そのもの、あるいは Γ にある命題を１個追加した形を持つ仮定を表します。
　さて、この推論規則は、構造に関する推論規則を用いると、次の推論規則：

(A3-2)

Γ1 ® P1 ¼  Γn ® Pn ————— Γ, As ® Q

と同等であることが示せます。
　実際、(A3-1) を推論規則に採用し、(A3-2) の上段が成り立っているとします。このとき推論規則 ( 仮 定 ) により Γ, A_s ® A_s が得られ、(A3-2) の上段のそれぞれに推論規則 ( 増 ) を適用すれば Γ_i , A_s ® P_i が得られますが、仮定 Γ に A_s を追加したものを Δ と書けば、これらはそれぞれ Δ ® A_s 及び Δ_i ® P_i と書けます。
　ゆえに、(A3-1) を、Γ のところに Δ を代入して適用すれば Δ ® Q が得られますが、これは (A3-2) の下段の式に他なりません。これは、(A3-1) から (A3-2) が導出できたことを意味しています。

　今度は逆に (A3-2) を推論規則に採用し、(A3-1) の上段が成り立っているとします。
　このとき、(A3-2) の上段がすべて成り立っているので、下段の式すなわち Γ, A_s ® Q が成り立ちますが、これと (A3-1) の最上段の式 Γ ® A_s に対して推論規則 ( 切 断 ) を適用すれば、(A3-1) の下段が得られます。
　これは、(A3-2) から (A3-1) が導出できたことを意味していますから、以上で (A3-1) と (A3-2) が同等であることがわかりました。

　ところで、(A3-2) は

(A3-3)

Γ1 ® P1 ¼  Γn ® Pn  Γ, Q ® R —————  Γ, As ® R

とも同等です。ただし、R というメタ変数は、すべての Γ_i において、Γ に付け加える命題を表すメタ変数とは異なるものとします。
　実際、(A3-3) で R に Q を代入すれば、上段最後の式は Γ, Q ® Q となって推論規則 ( 仮 定 ) から導出できるので、推論図式からは落とすことができ、その結果得られる図式は、メタ変数 R に関する仮定により、(A3-2) に一致します。
　逆に (A3-2) を推論規則に仮定し、(A3-3) の上段が成り立っているとすると、(A3-2) の上段がすべて成り立っているのでその下段の式 Γ, A_s ® Q が成り立ちまずが、これと、Γ, Q ® R に ( 増 ) と ( 換 ) を適用して得られる Γ, A_s , Q ® R に対して推論規則 ( 切 断 ) を適用すれば、Γ, A_s ® R すなわち (A3-2) の下段が得られます。
　以上により、(A3-1)~(A3-3) の３つの推論規則はすべて同等であることがわかりました。

　ところで (A3-2) あるいは (A3-3) は、当該論理記号 s を陽に含む命題が ® の左側に導入されています。そこで、これらの推論規則を (s 左) とよぶことにします。
　これに対し、導入規則 (s 導入) は、当該論理記号を陽に含む命題が ® の右側に導入されるので、これを (s 右) ともよぶことにします。

　さて、論理記号 Ú , $ については (A3-2) を、論理記号 Ù , Þ , " については (A3-3) を (s 左) として採用することにすれば、

(Ù 左)	(Ú 左)	(Þ 左)	(" 左)	($ 左)
Γ, P ® R ——————–  Γ, P Ù Q ® R     Γ, Q ® R ——————–  Γ, P Ù Q ® R	Γ, P ® R Γ, Q ® R ——————–  Γ, P Ú Q ® R	Γ ® P Γ, Q ® R ——————— Γ, P Þ Q ® R	Γ, (T | x)P ® R ———————– Γ, "xP ® R	Γ, P ® R —————— Γ, $xP ® R   ( x¢Γ , R )

という、各論理記号の消去規則と同等な推論規則群が得られます。

　次に、(^ 消去) を前提にして、Ø に関する推論図を考えてみましょう。
　Γ, P ® ^ が定理ならば、(^ 消去) により Γ, P ® Q と Γ, P ® Ø Q が得られるので、(Ø 導入) により Γ ® Ø P が得られます。すなわち

(A3-4)

Γ, P ® ^ —————  Γ ® Ø P

という推論規則が得られます。これを (Ø 右) とよぶことにします。
　また、Γ ® P が定理なら、( 増 ) により Γ, Ø P ® P が得られ、( 仮 定 ) により Γ, Ø P ® Ø P が得られるので、(弱Ø消去) により Γ, Ø P ® R が得られ、特に R に ^ を代入すればΓ, Ø P ® ^ が得られます。すなわち

(A3-5)

Γ ® P —————–  Γ, Ø P ® ^

という推論規則が得られます。これを (Ø 左) とよぶことにします。

　逆に、同じ前提のもとで、(Ø 左) と (Ø 右) のペアから (Ø 導入) と (弱Ø消去) を導くことができます。
　実際、Γ, P ® Q と Γ, P ® Ø Q が共に成り立っているとします。このとき最初の式に (Ø 左) を適用すれば、Γ, P, Ø Q ® ^ が得られますが、これと Γ, P ® Ø Q に ( 切 断 ) を適用すれば Γ, P ® ^ が得られ、これに (Ø 右) を適用すれば Γ ® Ø P が得られます。これは (Ø 導入) が得られたことを意味します。
　次に Γ ® P と Γ ® Ø P が共に成り立っているとします。このとき最初の式に (Ø 左) を適用すれば、Γ, Ø P ® ^ が得られ、これと Γ ® Ø P に ( 切 断 ) を適用すれば Γ ® ^ が得られ、これに (^ 消去) を適用すれば Γ ® Q が得られます。これは (弱Ø消去) が得られたことを意味します。

　さて、ここで Γ ® ^ というsequent を Γ ® とも書くことにします。すると、推論規則 (^ 消去) は

(A3-6)

Γ ®    ———–  Γ ® P

と書くことができます。これはsequentの右辺について推論規則 ( 増 ) を適用した形になっているので、この推論図を ( 増 右 ) とよぶことにし、推論規則 (^ 消去) を ( 増 右 ) で置き換えることにします。それに伴って、本来の ( 増 ) は ( 増 左 ) ともよぶことにします。
　なお、s が Ù , Ú , Þ , " , $ の場合に対して既に得られた (s 左) において、R に ^ を代入すれば、この規約によって、これらの推論図から R を“消した”推論図が得られることに注意します。

　次に、推論規則 ( 仮 定 ) すなわち Γ, P ® P で、特に Γ を空に取れば、

(A3-7)

P ® P

が得られます。これを始式とよびます。逆に、明らかに始式と ( 増 左 ) により ( 仮 定 ) が導出されるので、推論規則 ( 仮 定 ) をこの始式で置き換えることにします。

　次に、推論規則 ( 切 断 ) を若干変形します。
　Γ ® P と Δ, P ® Q が成り立っていれば、推論規則 ( 増 ) と ( 換 ) により Γ, Δ ® P と Γ, Δ, P ® Q が得られますが、これと推論規則 ( 切 断 ) により Γ, Δ ® Q が得られます。以上を図式で表すと、

(A3-8)

Γ ® P Δ, P ® Q —————– Γ, Δ ® Q

となります。なお、変形後の ( 切 断 ) においても Q に ^ を代入すると、形式上 Q を“消した”推論図が得られることに注意します。

　同様に、推論規則 (Þ 左) も若干変形します。
　Γ ® P と Δ, Q ® R が成り立っているとすれば、推論規則 ( 増 ) と ( 換) により Γ, Δ ® P と Γ, Δ, Q ® R が得られ、これと推論規則 (Þ 左) により Γ, Δ, P Þ Q ® R が得られます。以上を図式で表すと、

(A3-9)

Γ ® P Δ, Q ® R ————————–  Γ, Δ, P Þ Q ® R

となります。

　以上により、直観主義論理の推論体系は、次の構造に関する推論規則群：

	左	右
増	Γ ® Δ ————– Γ, P ® Δ	Σ ® Π ————– Σ ® P, Π
減	Γ, P, P ® Δ ——————– Γ, P ® Δ	Σ ® P, P, Π ——————– Σ ® P, Π
換	Γ, P, Q, Δ ® Θ ———————— Γ, Q, P, Δ ® Θ	Σ ® Π, P, Q, Ξ ———————— Σ ® Π, Q, P, Ξ
切断	Γ ® P, Δ         Θ, P ® Λ ———————————– Γ, Θ ® Δ, Λ
代入	Γ ® Δ ———————— (T | x)Γ ® (T | x)Δ
始式	P ® P

と、論理記号に関する推論規則群：

記号	左	右
Ù	Γ, P ® Δ ——————– Γ, P Ù Q ® Δ     Γ, Q ® Δ ——————– Γ, P Ù Q ® Δ	Σ ® P, Π         Σ ® Q, Π ———————————– Σ ® P Ù Q, Π
Ú	Γ, P ® Δ         Γ, Q ® Δ ———————————– Γ, P Ú Q ® Δ	Σ ® P, Π ——————– Σ ® P Ú Q, Π     Σ ® Q, Π ——————– Σ ® P Ú Q, Π
Þ	Γ ® P, Δ         Θ, Q ® Λ ———————————– Γ, Θ, P Þ Q ® Δ, Λ	Σ, P ® Q, Π ——————— Σ ® P Þ Q, Π
Ø	Γ ® P, Δ —————— Γ, Ø P ® Δ	Σ, P ® Π —————— Σ ® Ø P, Π
"	Γ, (T | x)P ® Δ ———————– Γ, "xP ® Δ	Σ ® P, Π ——————   ( x¢Σ, Π  )  Σ ® "xP, Π
$	Γ, P ® Δ ——————   ( x¢Γ, Δ )  Γ, $xP ® Δ	Σ ® (T | x)P, Π ———————– Σ ® $xP, Π

において、各sequents の ® の右辺は１個以下の命題からなるという条件を満たすような推論体系と同等であることがわかりました。ただし、上段が複数の式からなる場合、上下に積み重ねる代わりに左右に並べてあります（なお、( 減 ) と ( 換 ) の“右”はこの制約条件のもとでは意味がありませんが、左右の対称性を保つために付け加えました）。
　この推論体系を (LJ ) とよびます。(LJ ) では ^ は論理記号とはみなされず、自然推論の (^ 消去) に対応する推論規則は、( 増 右 ) として構造に関する推論規則に組み込まれています。

　ところで、上記の (LJ ) の推論規則は、® の右辺の命題が１個以下であるという制約を除けば、左右が全く対称な形をしています。
　すなわち (Ù 右) の左右を入れ替えれば (Ú 左) になり、(Ú 右) の左右を入れ替えれば (Ù 左) になり、(Ø 右) の左右を入れ替えれば (Ø 左) になり、(" 右) の左右を入れ替えれば ($ 左) になり、($ 右) の左右を入れ替えれば (" 左) になっています。

　そこで、上記の (LJ ) の推論規則において、“® の右辺が１個以下の命題からなる”という制約条件を外した推論体系を (LK) とよびます。

　まず (LK) では、古典論理で証明可能なsequent Γ ® P はすべて証明可能です。
　実際、始式 P ® P に (Ø 右) を適用すれば ® Ø P, P が得られ、更に (Ø 左) を用いれば ØØ P ® P が得られます。
　ゆえに、もし Γ ® ØØ P が証明可能なら、これと ØØ P ® P に対して ( 切 断 ) を適用すれば Γ ® P が得られ、これは (Ø 消去) が導出できることを意味します。
　他の直観主義論理と共通の推論はすべて導出できるのですから、以上により (LK) では古典論理で証明可能なsequentがすべて証明できることがわかりました。

　さて、古典論理では、Γ ® P が証明可能なら、(Ø 左) により Γ, Ø P ® は証明可能ですが、逆も成り立ちます。
　実際、Γ, Ø P ® が証明可能なら、(Ø 右) により Γ ® ØØ P が得られ、これと ØØ P ® P に対して ( 切 断 ) を適用すれば Γ ® P が導かれるからです。
　すなわち古典論理では、Δ が一個の命題からなる場合、sequent Γ ® Δ と Γ, Ø Δ ® は一方が証明可能なら他方も証明可能です。
　そこで、Δ が２個以上の命題からなる場合でも、Ø Δ で Δ を構成するすべての命題に Ø を付けたものを表すことにして、sequent Γ ® Δ を、sequent Γ, Ø Δ ® のことであると定義することができます。
　このとき (LK) で証明可能なsequentは古典論理でも証明可能であることがわかります。
　実際、( 増 ) , ( 減 ) , ( 換 ) については ® の右辺をすべて Ø を付けて左辺に移項した図式は古典論理で証明可能であり、( 切 断 ) については Δ と Λ をすべて Ø を付けて左辺に移項した図式は古典論理で証明可能であり、論理記号に関する推論規則群は、Δ と Λ をすべて Ø を付けて左辺に移項した図式が同様に古典論理で証明可能だからです。
　以上により、古典論理の推論体系と (LK) は同等であることがわかりました。

　さて、(LK) , (LJ ) についても本文第２節メタ定理１及びメタ定理２と同じ性質が成り立ちます：

(A3-10)

P を、(LJ ) 又は (LK) における推論規則の全部又は一部のみを推論規則に採用した理論における証明文とし、x を変数、y を P に現れず、x と異なる変数とすれば、( y | x)P も証明文である。

(A3-11)

(LJ ) 又は (LK) における推論規則の全部又は一部のみを推論規則に採用した理論では、推論規則 ( 代 入 ) は導出可能である。すなわちsequent Φ が定理のとき、x が変数、T が項なら (T | x)Φ も定理である。

　これらの証明は、本文第２節メタ定理１、メタ定理２の証明と全く同様なので省略します。なお、(A3-11) の事実があるため、多くの教科書では始めから ( 代 入 ) を推論規則から落としています。
　ところがこれに対し、同節メタ定理３に対応する ( 増 ) の導出のような主張は成り立ちません。
　なぜなら、自然推論で基本的だった推論規則 ( 仮 定 ) を導くとき、始式から ( 左 増 ) を本質的に用いていますし、また (LJ ) における ( 右 増 ) は ^ に関する消去規則そのものですから、やはり他から導出することはできないからです。

　一方、同節メタ定理４に対応する次の性質：

Gentzenの基本定理 　(LJ ) 又は (LK) における推論規則の全部又は ( 増 ) , ( 減 ) , ( 換 ) をすべて含む一部のみを推論規則に採用した理論では、推論規則 ( 切 断 ) は導出可能である。

は成立します。ただしその証明は同節メタ定理４の証明とはかなり違います。
　なぜなら、自然推論の場合には、( 増 ) 以外の推論規則を適用すると、仮定は減りこそすれ増えることがなく、このことを証明で本質的に用いたのですが、(LJ ) や (LK) ではこの事実そのものが成り立たないからです。

　Gentzenの基本定理の証明に先立って、若干の言葉の定義と準備をしておきましょう。

　上で挙げた (LK ) 又は (LJ ) の推論規則において、命題列 Γ , Δ , Θ , Λ , Σ , Π , Ξ の部分をすべて消し去ったとき、下段に残る命題列をその推論規則の主部、上段に残る命題列をその推論規則の副部とよぶことにします。
　また、(" 右) と ($ 左) のところに出てくる変数 x をこれらの推論規則の固有変数とよび、また ( 切 断 ) の上段の副部のことをこの推論規則の固有部分ともよぶことにします。

　ここで、(LK ) 及び (LJ ) の推論規則には、Gentzenの基本定理の証明において本質的な、次の性質があることを確かめておきましょう：

(A3-12)

s を任意の論理記号とする。上記一覧表の推論規則 (s 左) の任意の一つを選んで λ と書き、推論規則 (s 右) の任意の一つを選んで ρ と書くことにする。このとき、λ と ρ の下段同士にこれらの主部を固有部分とする ( 切 断 ) を適用して得られるsequentは、λ と ρ の上段に出てくるsequent同士にこれらの副部を固有部分とする ( 切 断 ) と、( 換 ) を（更に λ 又は ρ が固有変数を持つときはこれらに加えて ( 代 入 ) を）それぞれ何回か適用することによっても得られる。

　言葉で書くとややこしいですが、具体的に確かめてみることにしましょう。

　まず s が論理記号 Ù の場合を考えます。
　このとき λ は (Ù 左) の２つある中から選ぶことになりますが、どちらでも同じですから左側の方を選ぶことにします。一方、ρ は (Ù 右) です。
　これらの下段のsequentは Γ, P Ù Q ® Δ と Σ ® P Ù Q, Π ですから、これらに主部 P Ù Q を固有部分とする ( 切 断 ) を適用すれば、sequent Σ, Γ ® Π, Δ が得られます。
　一方 λ と ρ の上段のsequentは Γ, P ® Δ と Σ ® P, Π と Σ ® Q, Π の３つですから、第１と第２のsequentに副部 P を固有部分とする ( 切 断 ) を適用すれば、下段のときと同じsequent Σ, Γ ® Π, Δ が得られます。
　λ として (Ù 左) の右側を選んだ場合でも同様です（ただし上段の方は副部として Q を含む２つのsequentに ( 切 断 ) を適用します）。

　次に s が論理記号 Ú の場合を考えます。
　これの推論規則は Ù のそれと完全に左右対称で、上の証明も左右対称ですから、この場合も成り立つことがわかります。

　次に s が論理記号 Þ である場合を考えます。
　この場合、λ は (Þ 左) 、ρ は (Þ 右) です。
　これらの下段のsequentは Γ, Θ, P Þ Q ® Δ, Λ と Σ ® P Þ Q, Π ですから、これらに主部 P Þ Q を固有部分とする ( 切 断 ) を適用すれば、sequent Σ, Γ, Θ ® Π, Δ, Λ が得られます。
　一方 λ と ρ の上段のsequentは Γ ® P, Δ と Θ, Q ® Λ と Σ, P ® Q, Π の３つですから、まず第１と第３のsequentに副部 P を固有部分とする ( 切 断 ) を適用すれば Γ, Σ ® Δ, Q, Π が得られますが、これに ( 換 ) を何回か施せば Σ, Γ ® Q, Π, Δ が得られ、続けてこれと第２のsequentに副部 Q を固有部分とする ( 切 断 ) を適用することにより、下段のときと同じsequent Σ, Γ, Θ ® Π, Δ, Λ が得られます。

　次に s が論理記号 Ø の場合を考えます。
　この場合、λ は (Ø 左) 、ρ は (Ø 右) です。
　これらの下段のsequentは Γ, Ø P ® Δ と Σ ® Ø P, Π ですから、これらに主部 Ø P を固有部分とする ( 切 断 ) を適用することにより、sequent Σ, Γ ® Π, Δ が得られます。
　一方 λ と ρ の上段のsequentは Γ ® P, Δ と Σ, P ® Π ですから、これらのsequentに副部 P を固有部分とする ( 切 断 ) を適用することにより Γ, Σ ® Δ, Π が得られますが、これに ( 換 ) を何回か施せば、下段のときと同じsequent Σ, Γ ® Π, Δ が得られます。

　次に s が量化記号 " の場合を考えます。
　この場合、λ は (" 左) 、ρ は (" 右) です。
　これらの下段のsequentは Γ, "xP ® Δ と Σ ® "xP, Π ですから、これらに主部 "xP を固有部分とする ( 切 断 ) を適用することによって、sequent Σ, Γ ® Π, Δ が得られます。
　一方 λ と ρ の上段のsequentは Γ, (T | x)P ® Δ と Σ ® P, Π で、２番目のsequentは固有変数 x を持つ、すなわち Σ と Π は固有変数 x を含みません。従ってこの２番目のsequentに ( 代 入 ) を適用すれば Σ ® (T | x)P, Π が得られるので、これと１番目のsequentに副部 (T | x)P を固有部分とする ( 切 断 ) を適用することにより、下段のときと同じsequent Σ, Γ ® Π, Δ が得られます。

　最後に s が量化記号 $ の場合を考えます。
　これの推論規則は " のそれと完全に左右対称で、上の証明も左右対称ですから、この場合も成り立つことがわかります。

　これですべての論理記号に対する確認が終わったので、(A3-12) が成り立つことが確かめられました。

　さて、以上の準備のもとでGentzenの基本定理を証明します。

　一般に、推論規則の上段は１個以上のsequentから成りますが、その第 i 番目のsequentの左辺の副部を α_i と書き、右辺の副部を β_i と書き、下段のsequentの左辺の主部を α 、右辺の主部を β と書けば、この推論規則の上段第 i 番目のsequent は一般に { Γ_i , α_i } ® { β_i , Δ_i } と書け、下段のsequentは { Γ, α } ® { β, Δ } と書けます。ただし、一般に { Σ } で命題列 Σ の順番を入れ替えて得られるある命題列を表すことにします。以上のような表示を、当該推論規則を構成するsequentの分離表示とよぶことにしましょう。
　さて、上記の表を眺めると、Γ_i がすべて Γ に一致し、Δ_i がすべて Δ に一致している推論規則の一群があります（ ( 切 断 ) , ( 代 入 ) , (Þ 左) 以外のすべて）。これを第１種の推論規則とよぶことにしましょう。
　一方、Γ_i をすべて並べると Γ になり、Δ_i をすべて並べると Δ になるような推論規則の一群があります（ ( 切 断 ) と (Þ 左) ）。これを第２種の推論規則とよぶことにしましょう。

　次に、命題 R を１個以上並べて得られる命題列を一般に R^# で表すことにします。もし R^# を含むsequentが定理ならば、これに ( 減 ) と ( 換 ) を何回かほどこせば、このsequentの R^# のところを R に置き換えたsequentが定理として得られます。

　ゆえに、(LK ) 又は (LJ ) の ( 減 ) と ( 換 ) を推論規則に持つ推論体系では、( 切 断 ) を推論規則に採用することと、次の ( 混 )：

(A3-13)

Γ ® { R#, Δ }       { Θ, R# } ® Λ ——————————————– Γ, Θ ® Δ, Λ

を推論規則に採用することは同じことです。
　以下、上段で Γ ® { R^#, Δ } と書かれたsequentを Φ と略記し、{ Θ, R^# } ® Λ と書かれたsequentを Ψ と略記することにします。また、上段で R^# と書かれた部分を、この推論規則 ( 混 ) の固有部分とよぶことにします。
　また一般に、命題列 Σ から (A3-13) の固有部分の構成要素である R をすべて取り除いて得られる命題列を Σ* と書くことにします。明らかに Φ の右辺の一部 Δ' に対する Δ'* は Δ の一部になり、Ψ の左辺の一部 Θ' に対する Θ'* は Θ の一部になります。

　ところで既に注意したように、( 代 入 ) はメタ定理として他の推論規則から導出できます。
　従ってGentzenの基本定理を証明するには、(LK ) 又は (LJ ) の推論規則のうち、少なくとも ( 増 ) と ( 減 ) と ( 換 ) は推論規則に採用し、( 切 断 ) と ( 混 ) と ( 代 入 ) は推論規則に採用しないという推論体系において (A3-13) の推論図式が導出できること、すなわち Φ と Ψ が証明可能なら Γ, Θ ® Δ, Λ も証明可能であることを確かめれば十分です。

　さて、(A3-13) の ( 混 ) の固有部分の構成要素 R の中に登場する論理記号の個数 n （同じ記号でも場所が違えば別として数える）を、この ( 混 ) の次数とよぶことにします。
　また、(A3-13) の上段のsequent Φ と Ψ が共に証明されているとき、それぞれの証明文 P と Q が存在しますが、必要ならば、証明文を Φ 又は Ψ までで“打ち切る”ことにより、これらのsequentは証明文の最後に書かれていると仮定することができます。
　ここで P と Q の長さ（すなわち証明文を構成するsequentの個数）の和を k とするとき、この ( 混 ) は階数が k 以下であるということにします。なお、ある l < k に対して階数が l 以下であることを、階数が k 未満であるということにします。

　以下、(A3-13) の上段 Φ と Ψ が共に証明可能で (A3-13) の次数が n 、階数が k 以下のとき、(A3-13) の下段が定理になることを、まず次数 n に関する帰納法で、更に同じ n の中では k に関する帰納法で証明します。
　言い換えると、上段のsequentが共に証明可能で、次数が n 未満、又は次数が n で階数が k 未満であるような ( 混 ) の下段のsequentは必ず証明可能であると仮定して、(A3-13) の下段のsequentが定理になることを証明します。

　さて、まず Φ が始式である場合を考えます。この場合、Γ は R で、Δ は空ですから、( 混 ) の下段 Γ, Θ ® Δ, Λ は R, Θ ® Λ となり、これは Ψ から推論規則 ( 減 ) と ( 換 ) のみによって証明可能ですから、この場合には証明されました。
　対称性により、Ψ が始式である場合についても同様です。
　従って、あとは Φ と Ψ が共に、ある推論規則を適用して得られた場合を考えれば十分です。

( CASE 1 )
　最初に、Φ がある推論規則 (A) を適用して得られたsequentで、(A3-13) の固有部分 R^# と (A) の主部が重ならない場合を考えます。

　(A) の上段の各sequent Φ_i の分離表示を { Γ_i , α_i } ® { β_i , Δ_i } とし、下段 Φ の分離表示を { Γ', α } ® { β, Δ' } とすると、{ β, Δ' } は { R^#, Δ } で、仮定により主部 β は固有部分 R^# と重ならないので Δ に含まれ、従って Δ' は R^# を含むことがわかります。
　また Φ_i は証明文 P の中に現れるので、その現れたところで証明文を“打ち切って”得られる証明文を P_i とすれば、これは P より短い Φ_i の証明文になっています。

　ここで、(LJ ) の場合について若干補足しておきます。
　Φ の右辺である { R^#, Δ } と { β, Δ' } は１個以下の命題からなるので、Δ' は R １個のみから成り、従って β と Δ と Δ'* は空です。
　しかも (A) が第１種なら、すべての i に対して Γ_i は Γ' で、Δ_i は Δ' で R １個からなるので、その結果 β_i も Δ_i* も空です。
　また (A) が第２種なら、ある１つの i に対して Δ_i は R １個のみからなり、その結果 β_i と Δ_i* は空であり、他の i に対しては Δ_i が空です。

　また、(A) が (" 右) か ($ 左) の場合は、(A) の固有変数 x を P にも Θ にも Λ にも現れない変数 z に退避変換する、すなわち Φ_i を (z | x)Φ_i に置き換えておくことにします。このとき (z | x)P_i は (z | x)Φ_i の証明になっており、その長さは P_i の長さと同じです。また、Φ_i は副部以外が x を含まないので、(z | x)Φ_i に固有変数を z とする推論規則 (A) を適用すると、置き換えなかった場合と同じsequent Φ が得られます。

　ここで、Δ_i が R を含むような i に対しては、Φ_i と Ψ すなわち { Γ_i , α_i } ® { β_i , Δ_i } と { Θ, R^# } ® Λ を上段に持ち、Δ_i に現れるすべての R と R^# と書いた部分を固有部分とする ( 混 ) を考えることができますが、この ( 混 ) の次数は n で、階数は k 未満なので、帰納法の仮定により、この ( 混 ) を適用して得られる { Γ_i , Θ, α_i } ® { β_i , Δ_i*, Λ } は証明可能です。これを φ_i と書きます。
　また Δ_i が R を含まないような i に対しては、Δ_i* は Δ_i ですから、Φ_i は { Γ_i , α_i } ® { β_i , Δ_i* } と書けるので、これを φ_i と書きます。なお、(A) が第１種のときは Δ_i は Δ' なので R を含み、従ってこのケースは生じないことに注意します。
　なお、いずれの場合も、(A) が (" 右) か ($ 左) の場合は Γ_i , Θ, Δ_i*, Λ が固有変数を含まないことに注意します。
　ゆえに、必要なら各 φ_i に何回か ( 換 ) を適用した上で推論規則 (A) を適用し、必要なら ( 減 ) を何回か適用すれば { Γ', Θ, α } ® { β, Δ'*, Λ } が得られますが、Γ は { Γ', α } で、{ β, Δ'* } は R^# と重ならないので Δ に含まれ、従って更に ( 増 ) と ( 換 ) を何回か適用すれば (A3-13) 下段の Γ, Θ ® Δ, Λ が得られます。

( CASE 2 )
　次に、Ψ がある推論規則 (B) を適用して得られ、(A3-13) の固有部分 R^# と (B) の主部が重ならない場合を考えます。

　この場合は ( CASE 1 ) の議論を左右すべて入れ替えて適用すれば、(LK ) の場合については左右が完全に対称ですから、この場合も成り立つことがわかります。
　一方、(LJ ) の場合を考えるために、( CASE 1 ) において (LJ ) とは逆に、「sequentの左辺は高々１個の命題からなる」という制約条件を付けて考えることにすると、Ψ の左辺である { Θ, R^# } は１個以下の命題からなるので Θ は空となり、( CASE 1 ) の議論がこの場合にも適用可能であることがわかります。

　以上により、あとは Φ が Φ_i から推論規則 (A) を適用して得られ、(A3-13) の固有部分 R^# と (A) の主部が重なり、かつ Ψ が Ψ_j から推論規則 (B) を適用して得られ、(A3-13) の固有部分 R^# と (B) の主部が重なる場合を考えれば十分であることがわかりました。
　そこで、推論規則 (A) と (B) の種類によって場合分けを行いますが、(A) の主部は (A3-13) の固有部分と重なるので Φ の右辺にあり、従って (A) は必ず (〜 右) と書かれた推論規則に限られ、同様に (B) は必ず (〜 左) と書かれた推論規則に限られることに注意します。

( CASE 3 )
　まず (A) が ( 増 右 ) , ( 減 右 ) , ( 換 右 ) の場合は、(A) の下段のsequent Φ が Γ ® { R^# , Δ } で、R は (A) の主部に含まれますから、(A) の上段のsequent Φ' は Γ ® { R°, Δ } と書けます。ただし R° は R を０個以上並べた命題列を表します。
　もし R° が空なら、Φ' は Γ ® { Δ } なので、これに ( 換 ) と ( 増 ) を何度か適用することにより (A3-13) 下段の Γ, Θ ® Δ, Λ が得られます。
　また、もし R° が空でなければ、１個以上の R を含むので、Φ' と、Ψ すなわち { Θ, R^# } ® Λ に対して R° 及び R^# と書かれた部分を固有部分に持つ ( 混 ) を考えると、Φ' は Φ より短い証明を持つので、この ( 混 ) は次数が n で階数は k 未満です。
　ゆえに、帰納法の仮定により、この ( 混 ) の下段 Γ, Θ ® Δ, Λ は証明可能で、このsequentは (A3-13) の下段に他なりません。

( CASE 4 )
　上と全く対称的な議論により、(B) が ( 増 左 ) , ( 減 左 ) , ( 換 左 ) のいずれかである場合には全く同様に証明できます。

( CASE 5 )
　従って、あと残るのは、(A) と (B) が共に論理記号に関する推論規則である場合のみとなります。しかも論理記号に関する推論規則の形から明らかなように、(A) と (B) は同一の論理記号 s に対する (s 右) と (s 左) でなければなりません。

　(A) の上段の各sequent Φ_i の分離表示を Γ_i , α_i ® β_i , Δ_i とし、下段 Φ の分離表示を Γ', α ® β, Δ' とすると、{ β, Δ' } は { R^#, Δ } なので、仮定により、主部 β は (A3-13) の固有部分 R^# と重なり、従って R １個から成ります。また α と β* は空です。
　また、(B) の上段の各sequent Ψ_j の分離表示を Θ_j , γ_j ® δ_j , Λ_j とし、下段 Ψ の分離表示を Θ', γ ® δ, Λ' とすると、{ Θ', γ } は { Θ, R^# } なので、仮定により、主部 γ は (A3-13) の固有部分 R^# と重なり、従って R １個から成ります。また δ と γ* は空です。
　一方、Φ_i は証明文 P の中に現れるので、その現れたところで証明文を“打ち切って”得られる証明文を P_i とすれば、これは P より短い Φ_i の証明文になっています。
　また、Ψ_j は証明文 Q の中に現れるので、その現れたところで証明文を“打ち切って”得られる証明文を Q _j とすれば、これは Q より短い Ψ_j の証明文になっています。

　ここでも (LJ ) の場合について若干補足しておきます。
　Φ の右辺である { R^#, Δ } と { β, Δ' } は１個以下の命題からなるので Δ' と Δ は空で、従ってすべての Δ_i も空であることがわかります。

　そこで、Δ_i が R を含むような i に対しては、Φ_i と Ψ に対して Δ_i と Θ' と γ に現れるすべての R を固有部分とする ( 混 ) を考えると、その次数は n で、階数は k より小さいので、帰納法の仮定により、この ( 混 ) を適用して得られる Γ_i , α_i , Θ'* ® β_i , Δ_i*, Λ' は証明可能です。そこで、これに何回か ( 換 ) を施した Θ'*, Γ_i , α_i ® β_i , Δ_i*, Λ' を φ_i と書きます。なお、(LJ ) のときは、このケースは生じないことに注意します。
　また Δ_i が R を含まないような i に対しては、Δ_i が Δ_i* とも書けるので、(LJ ) の場合は Φ_i すなわち Γ_i , α_i ® β_i , Δ_i* を φ_i と書き、(LK ) の場合はこれに ( 増 ) と ( 換 ) を何回か適用して得られる Θ'*, Γ_i , α_i ® β_i , Δ_i*, Λ' を φ_i と書きます。
　対称的に、Θ_j が R を含むような j に対しては、Φ と Ψ_j に対して β と Δ' と Θ_j に現れるすべての R を固有部分とする ( 混 ) を考えると、その次数は n で、階数は k より小さいので、帰納法の仮定により、この ( 混 ) を適用して得られる Γ', Θ_j*, γ_j ® Δ'*, δ_j , Λ_j は証明可能です。そこで、これに ( 換 ) を何回か施した Γ', Θ_j*, γ_j ® δ_j , Λ_j , Δ'* を ψ_j と書きます。
　また Θ_j が R を含まないような j に対しては、Θ_j が Θ_j* とも書けるので、Ψ_j すなわち Θ_j*, γ_j ® δ_j , Λ_j に ( 増 ) と ( 換 ) を何回か適用して得られる Γ', Θ_j*, γ_j ® δ_j , Λ_j , Δ'* を ψ_j と書きます。

　そこで φ_i や ψ_j に (A) や (B) の副部を固有部分とする ( 切 断 ) を適用すると、これらの ( 切 断 ) は ( 混 ) の一種であり、その固有部分を構成する命題は、(A) や (B) の副部なので、その次数は (A) や (B) の主部を構成する R の次数である n より小さい値を持っています。
　ゆえに帰納法の仮定により、これらの ( 切 断 ) を適用して得られたsequentはすべて証明可能です。

　ここで (LK ) の場合、φ_i の全体を上段に持つ推論規則 (A) の下段は { Θ'*^#, Γ' } ® R, { Δ'*, Λ' ^# } であり、ψ_j の全体を上段に持つ推論規則 (B) の下段は { Γ' ^#, Θ'* }, R ® { Λ', Δ'*^# } です。ただし ^# は、同じ命題列を１回以上繰り返し並べた命題列を表します。
　ゆえに、これらに (A) と (B) の主部 R を固有部分とする ( 切 断 ) を適用した { Θ'*^#, Γ', Γ' ^#, Θ'* } ® { Δ'*, Λ' ^#, Λ', Δ'*^# } は、(A3-12) により φ_i や ψ_j に (A) や (B) の副部を固有部分とする ( 切 断 ) を適用すれば得られるので、前段落の結果により証明可能ですが、このsequentに ( 換 ) と ( 減 ) を何回か適用して得られる Γ', Θ'* ® Δ'*, Λ' も証明可能で、従って更に必要なら ( 増 ) と ( 換 ) を何回か適用して得られる Γ, Θ ® Δ, Λ も証明可能です。

　また、(LJ ) の場合、φ_i の全体を上段に持つ推論規則 (A) の下段は、α と Δ_i* が空で β が R なので Γ' ® R となり、ψ_j の全体を上段に持つ推論規則 (B) の下段は、δ と Δ'* が空で γ が R なので { Γ' ^#, Θ'* }, R ® Λ' となります。
　ゆえに、これらに (A) と (B) の主部 R を固有部分とする ( 切 断 ) を適用した { Γ', Γ' ^#, Θ'* } ® Λ' は、(A3-12) により φ_i や ψ_j に (A) や (B) の副部を固有部分とする ( 切 断 ) を適用すれば得られるので、前々段落の結果により証明可能ですが、これに ( 換 ) と ( 減 ) を何回か適用して得られる Γ', Θ'* ® Λ' も証明可能で、従って更に ( 増 ) と ( 換 ) を何回か適用して得られる Γ, Θ ® Δ, Λ も証明可能です。

　以上により、Gentzenの基本定理は証明されました。

　さて、Gentzenの基本定理は、構造に関する推論規則が導出可能であるということを意味する多くのメタ定理（本文第２節メタ定理１〜４参照）の一つに過ぎないように見えますが、このGentzenの基本定理の意味するところはそれらとは異なり、かなり強力です。
　なぜなら、(LK) 及び (LJ ) においては、( 切 断 ) 以外の推論規則は、下段が上段より“複雑”になる一方であり、( 切 断 ) だけがその例外になっているからです。Gentzenの基本定理によれば、証明可能な命題は ( 切 断 ) を用いなくても証明できる、すなわち複雑になる一方の証明が存在するということです。

　Gentzenの基本定理の応用例として、(LK) でも (LJ ) でも矛盾、すなわち ® の両辺とも空であるようなsequentは証明できないことがわかります。
　実際、もし ® が証明可能であるとすると、Gentzenの基本定理により、これは ( 切 断 ) なしで証明できるはずですが、( 切 断 ) 以外の推論規則の下段のsequentの両辺が共に空になることはありえないからです。

　また、ある証明可能なsequent Φ に現れる論理記号の全体を s₁,¼, s_n とすると、Φ は構造に関する推論規則と s₁,¼, s_n に関する推論規則のみを使って証明できることがわかります。
　実際、Gentzenの基本定理により、( 切 断 ) を使わない Φ の証明 P が存在します。なお、必要ならば、P から使われないsequentをすべて取り除いておくものとします。
　ところで一般に、論理記号 s に関する推論規則を用いると、その結果得られるsequentには必ず s が含まれることが上記の一覧表から明らかにわかります。
　一方、( 切 断 ) 以外の推論規則では、その上段のどのsequentに出てくる論理記号もすべて下段のsequentに出てくるので、結局 P で論理記号 s に関する推論規則を用いていれば、Φ には s が含まれていることがわかります。

　特に、直観主義論理の自然推論で証明可能な、あるsequent Φ に現れる論理記号の全体を s₁,¼, s_n とすると、Φ は (LJ ) において、( 切 断 ) 以外の構造に関する推論規則と、これらの論理記号の推論規則、すなわち (s_i 右) と (s_i 左) のみによって証明できます。
　一方、直観主義論理では、構造に関する推論規則を用いると、(s 導入) と (s 消去) のペアは (s 右) と (s 左) のペアと同等なのでした。
　ところが、本文第２節メタ定理１〜４によれば、自然推論では ( 換 ) と ( 仮 定 ) 以外の構造に関する推論規則はすべて導出可能なので、直観主義論理の自然推論で証明可能なsequentは、そこに現れる論理記号に関する自然推論の推論規則と ( 換 ) , ( 仮 定 ) のみによって証明できることがわかりました。