数学の基礎

付録２．形式化の原理と直観主義論理

　推論規則というのは推論の大もとになる規則ですから、それ自身が何かから導けるというものではありません。つまり勝手な推論規則を定めてやれば、それをもとに推論体系が作れるわけです。
　しかしながら、本文第１節で与えた直観主義論理の一群の推論規則は、実は勝手に定めたものではなく、

　ある構文論的な概念に注目し、その概念自身と、その概念が持つ構文論的な性質を、論理記号及び推論規則の形で理論内部の概念に翻訳する。

という、形式化の原理とでも言うべき一貫した指導原理に貫かれているのです。
　以下、「（変数も論理記号も含まない）項」、「（変数も論理記号も含まない）命題」、「sequent」、「構造に関する推論規則」、「変数」、「論理記号」、「論理記号に関する推論規則」という論理における基本的な概念を、これから説明する形式化の原理によって次々に導入していく様子を見ていくことにしましょう。

　まず最初は（変数も論理記号も含まない）項についてです。
　これは、その定義により、定項（＝０変項関数記号）から始めて関数記号を次々に施していって得られる論理式を意味しますが、これは要するに、考察している理論における対象を表しています。すなわち定項とは当該理論ではそれ以上説明しない根源的な対象を、関数記号を含む項はこれらの根源的な対象からある定められた方法で派生的に定義された対象を表すことになります。

　次は（変数も論理記号も含まない）命題についてです。
　これは、その定義により、いくつかの項に述語記号を施して得られる論理式ですから、それらの項に関する何らかの性質を表しています。

　次はsequentと構造に関する推論規則についてです。
　理論における推論というのは、要するに「正しい命題」を次々に書き下していく行為のことです。
　その際、どういう命題を“正しい命題”とみなすかを決めるのが推論規則ですが、その規則というのは、結局のところ、“どの命題とどの命題が正しいときどの命題が正しくなるか”ということを定めることに他なりません。
　そこで、「命題 A₁ ,¼, A_n が正しいとき R は正しい」と推論できるとき、これを A₁ ,¼, A_n ® R と略記することにします。このとき

(A2-1) 　Γ ® R が成り立てば Γ ® R が成り立つ。

が同語反復として自明に成り立ちます。ただし A₁ ,¼, A_n と書く代わりにこれを Γ と略記しました。
　さて、

　命題 A₁ ,¼, A_n がすべて正しいものとする。ここで更に命題 B₁ ,¼, B_m がすべて正しいとき、命題 R は正しい。

ということを、二通りの言い方で表現してみましょう。
　一つの表現方法は、とにかく

　A₁ ,¼, A_n , B₁ ,¼, B_m がすべて正しいときに R が正しい。

ということですから、これは

(A2-2a) 　Γ, Δ ® R が成り立つ。

と表現することができます。ただし、B₁ ,¼, B_m と書く代わりにこれを Δ と略記しました。
　一方、これはまた

　Γ が正しいという前提の下で、B₁ ,¼, B_m がすべて正しければ、同じ前提 Γ の下で R が正しい。

と言い換えることもできますから、同じことを

(A2-2b) 　Γ ® B₁ と Γ ® B₂ と … と Γ ® B_m が成り立てば Γ ® R が成り立つ。

とも表現することができます。
　さて、(A2-2a) と (A2-2b) は、同じことの言い換えに過ぎないはずですから、ある状況の下で一方が成り立つなら他方も成り立つはずです。

　そこで、まずこの同等性を Δ が R 一個からなる場合に適用すると、(A2-2b) は (A2-1) により自明に成り立ちます。従って、同等性によりこの場合の (A2-2a) も成り立つはずです。すなわち

(A2-3) 　Γ, R ® R が成り立つ。

ということがわかります。

　次に、Γ ® R が成り立っているという前提の下で (A2-2a) と (A2-2b) の同等性を考えると、(A2-2b) の方は (A2-1) により自明に成り立ちますから、同じ前提 Γ ® R のもとで (A2-2a) も成り立たなければなりません。従って特に Δ が P 一個からなる場合を考えると

(A2-4) 　Γ ® R が成り立てば Γ, P ® R が成り立つ。

ということがわかります。

　次に、Γ, Δ ® R が成り立っているという前提の下で (A2-2a) と (A2-2b) の同等性を考えると、今度は (A2-2a) の方が (A2-1) により自明に成り立ちますから (A2-2b) も成り立たなければなりません。従って特に Δ が P 一個からなる場合を考えると

(A2-5) 　Γ, P ® R と Γ ® P が成り立てば Γ ® R が成り立つ。

ということがわかります。
　また、この (A2-5) の Γ を Γ, P に書き換えると

(A2-6) 　Γ, P, P ® R と Γ, P ® P が成り立てば Γ, P ® R が成り立つ。

ということがわかりますが、２番目の Γ, P ® P は (A2-3) により常に成り立つので、この前提は実は不要です。すなわち

(A2-7) 　Γ, P, P ® R が成り立てば Γ, P ® R が成り立つ。

ということがわかります。

　最後に、Δ を P, Δ, Q, Θ に置き換えた場合と Q, Δ, P, Θ に置き換えた場合を考えると、このどちらの場合についても (A2-2b) は同じ意味になります。従って (A2-2a) と (A2-2b) の同等性により、この両者に対する (A2-2a) も互いに同等でなければなりません。すなわち

(A2-8) 　Γ, P, Δ, Q, Θ ® R が成り立つことと Γ, Q, Δ, P, Θ ® R が成り立つことは同じことである。

ということがわかります。

　ところで Γ ® R のカンマや ® は、理論内部で使う文字ではなく、言葉を省略したもの（メタ記号）に過ぎません。
　そこで、この記法を形式化することにします。すなわちカンマと ® を理論内部で用いる文字として正式に追加し、命題をカンマで区切って並べた Γ と命題 R を ® で結んだ Γ ® R という文字列のことをsequentとよび、sequentを定められた規則に従って並べる行為を改めて証明文とよび、証明文に現れたsequentを定理とよぶことにします。
　更にこの形式化において、性質 (A2-1),(A2-3),(A2-4),(A2-5),(A2-7),(A2-8) をそのまま推論規則に採用することにします。これらが第１節で順に ( 同一 ) , ( 仮定 ) , ( 増 ) , ( 切断 ) , ( 減 ) , ( 換 ) と名付けた構造に関する推論規則に他なりません。

　次は変数についてです。
　（変数も論理記号も含まない）項 T に対する性質を表す命題群から構成されたsequent S が、項 T が具体的に何であるかには無関係な論法で証明される場合があります。
　この場合、項 T 、項 S 、… に対して同じ性質からなるsequentをいちいち別々に証明するのはわずらわしく、できればこれを一度に証明できれば便利です。そこで、このsequentの項 T のところを x と書いて、あたかも x が項を表すものとして証明すれば、証明は一回で済みます。
　そこで、x のような“モノ”を形式化した概念として、実際にアルファベットやそれにダッシュを付けた文字を変数とよんで、「変数も項である」と新たに定めることにします。すると、変数を含んだ証明文が与えられたとき、この中で変数のところに勝手な項を代入したものは、本来の意味での証明文になっているはずです。すなわち変数を含んだsequent S が定理なら、その中の変数 x に項 T を代入して得られるsequentも定理です。この事実を推論規則として明記したものが ( 代入 ) に他なりません。

　最後は論理記号と論理記号に関する推論規則についてです。
　以下、自然推論で考察を続けることにします。すなわち、ある公理系 Γ のもとで成り立つ命題 P を、その公理系の定理である、あるいは P が成り立つといい、考えている公理系 Γ に命題 Q を追加した公理系 Γ, Q で命題 R が成り立つとき、Q├ R が成り立つということにします。
　このように、P あるいは Q├ R の形の記述を何段か重ねて横棒を引き、その下に一個の命題を書いたものを、自然推論の推論図とよび、横棒の上段がすべて成り立つときに下段の命題が成り立つとき、この推論図は導出可能であるといいます。

　さて、ある公理系のもとで、命題 P と Q が共に成り立っているとします。この超数学的な状態のことを、P かつ Q 、あるいは P Ù Q と表現することにしましょう。
　ところで証明という行為は、すでに得られた定理を用いて次々に新たな定理を見つけていくプロセスのことに他なりません。そこで、証明文に関する上記の超数学的な状態を、そこから新たにどんな命題 R が導出できるか、という観点で特徴付けてみましょう。そのために、「命題 P と Q が共に成り立っているとき、新たに命題 R が得られる」ということを２通りの方法で表現してみましょう：

(A2-9a) P
Q
——–
R
が成り立つ。

(A2-9b) P Ù Q
———
R が成り立つ。

　これら２つの条件は同じことを意味しています。ただし (A2-9b) の P Ù Q というのは、命題ではなく、「命題 P と Q が共に成り立っている」ことを意味する超数学的な省略記号です。しかし、もしこれが超数学的な省略記号などではなく、一個の命題として扱えたとしたら大変便利です。
　そこで、２つの命題 P と Q を結び付けて一つの命題を作る Ù という２変項の論理接続詞を新たに追加することによって、P Ù Q を命題に“昇格”させることにしましょう。ただしそうすると、今度は (A2-9a) と (A2-9b) の同等性は自動的には成り立たなくなるので、両者が普遍的に同等になるような推論規則を追加することにします。
　ただし、(A2-9a) と (A2-9b) が普遍的に同等であるとは、一般に A や B├ C の形の特定の定理（群）が成り立つ、という形の任意の条件（空でもよい）を考えるとき、この条件を満たす任意の公理系で (A2-9a) が導出可能なら、その同じ条件を満たす任意の公理系で (A2-9b) が導出可能であり（このことを略して (A2-9a) Þ (A2-9b) と表現することにします）、その逆も成り立つ（これを (A2-9b) Þ (A2-9a) と略記します）という意味です。
　そこで、(A2-9b) Þ (A2-9a) の成立を丁度保証する推論規則のことを導入規則といい、逆に (A2-9a) Þ (A2-9b) の成立を丁度保証する推論規則のことを消去規則ということにします。

　すなわち推論規則 a が導入規則であるとは、「a を用いると (A2-9b) Þ (A2-9a) が導かれ、逆に (A2-9b) Þ (A2-9a) が成り立つような推論体系のもとでは a が導出可能である」という意味で、本文第１節で与えた ( Ù 導入) という推論規則がそのような導入規則 a になっています。
　実際、( Ù 導入) と (A2-9b) を仮定すると、(A2-9a) の上段から ( Ù 導入) により P Ù Q が導かれ、更に (A2-9b) により R が導かれるので、確かに (A2-9a) が導出されることがわかります。
　逆に (A2-9b) Þ (A2-9a) が成り立つような推論体系では、R に P Ù Q を代入すれば (A2-9b) は自明に成り立つので、仮定により R に P Ù Q を代入した (A2-9a) が成り立ち、これは推論規則 ( Ù 導入) が成り立つということに他なりません。

　同様に、推論規則 b が消去規則であるとは、「b を用いると (A2-9a) Þ (A2-9b) が導かれ、逆に (A2-9a) Þ (A2-9b) が成り立つような推論体系のもとでは b が導出可能である」という意味で、本文第１節で与えた ( Ù 消去) という推論規則がそのような消去規則 b になっています。
　実際、( Ù 消去) と (A2-9a) を仮定すると、P Ù Q から２個ある ( Ù 消去) によりそれぞれ P と Q が得られ、従って (A2-9a) により R が得られますが、これは (A2-9b) が得られたことを意味します。
　逆に (A2-9a) Þ (A2-9b) が成り立つような推論体系では、R にまず P を代入すれば、(A2-9a) は自明に成り立つので、仮定により (A2-9b) が成り立ち、これは２つある推論規則 ( Ù 消去) の最初のものに他なりません。同様に R に Q を代入すれば ( Ù 消去) の２番目のものが得られます。

　以上のような手順によって論理接続詞 Ù とその導入規則、消去規則を追加する行為を、P Ù Q という概念の形式化とよぶことにします。

　次に、ある公理系のもとで、命題 P か Q の少なくとも一方が成り立っているとします。この状態のことを、P 又は Q 、あるいは P Ú Q と表現することにし、この概念を形式化します。
　すなわち２変項論理接続詞 Ú と、「命題 P か Q の少なくとも一方が成り立っているとき命題 R が成り立つ」ということを意味する

(A2-10a) P
——
R と Q
——
R が成り立つ。

(A2-10b) P Ú Q
———
R が成り立つ。

という２つの条件が普遍的に同等になるような推論規則を追加することにします。

　このとき、本文第１節で与えた ( Ú 導入) という推論規則が Ú の導入規則になります。
　実際、( Ú 導入) と (A2-10b) を仮定すると、(A2-10a) のいずれの上段からも、( Ú 導入) により P Ú Q が導かれ、更に (A2-10b) により R が導かれるので、確かに (A2-10a) が導出されることがわかります。
　逆に (A2-10b) Þ (A2-10a) が成り立つような推論体系では、R に P Ú Q を代入すれば (A2-10b) は自明に成り立つので、仮定により R に P Ú Q を代入した (A2-10a) が成り立ち、これは推論規則 ( Ú 導入) が成り立つということに他なりません。

　また、本文第１節で与えた ( Ú 消去) という推論規則が Ú の消去規則になります。
　実際、( Ú 消去) と (A2-10a) を仮定すると、P を公理に追加した公理系において、P が成り立つことと (A2-10a) の左の推論図から、R が得られます。これは、もとの公理系で P├ R が成り立つことを意味しますが、同様に (A2-10a) の右の推論図を使って Q├ R が導かれるので、もし P Ú Q が成り立てば、( Ú 消去) により R が得られ、これは (A2-10b) が得られたことを意味します。
　逆に (A2-10a) Þ (A2-10b) が成り立つような推論体系では、P Ú Q と P├ R と Q├ R が成り立てば、P のとき P├ R と ( 切断 ) から R が得られ、Q のとき Q├ R と ( 切断 ) から R が得られるので、これは (A2-10a) が成り立つことを意味し、従って仮定から (A2-10b) が成り立ちますが、その上段は成り立っているので R が得られ、これは ( Ú 消去) が導出できたことを意味します。

　次に、ある公理系のもとで、命題 P を公理に追加したら Q が成り立ったとします。この状態のことを、P ならば Q 、あるいは P Þ Q と表現することにし、この概念を形式化します。
　すなわち２変項論理接続詞 Þ と、「命題 P を公理に追加したら Q が成り立ったとき命題 R が成り立つ」ということを意味する

(A2-11a) P├ Q
———–
R が成り立つ。

(A2-11b) P Þ Q
———–
R が成り立つ。

という２つの条件が普遍的に同等になるような推論規則を追加することにします。

　このとき、本文第１節で与えた ( Þ 導入) という推論規則が Þ の導入規則になります。
　実際、( Þ 導入) と (A2-11b) を仮定すると、(A2-11a) の上段から ( Þ 導入) により P Þ Q が導かれ、更に (A2-11b) により R が導かれるので、確かに (A2-11a) が導出されることがわかります。
　逆に (A2-11b) Þ (A2-11a) が成り立つような推論体系では、R に P Þ Q を代入すれば (A2-11b) は自明に成り立つので、仮定により R に P Þ Q を代入した (A2-11a) が成り立ち、これは推論規則 ( Þ 導入) が成り立つということに他なりません。

　また、本文第１節で与えた ( Þ 消去) という推論規則が Þ の消去規則になります。
　実際、( Þ 消去) と (A2-11a) を仮定すると、P Þ Q が成り立てば、P を仮定すると ( Þ 消去) により Q が得られ、これは P├ Q が成り立つことを意味しますから、(A2-11a) により R が得られ、これは (A2-11b) が得られたことを意味します。
　逆に (A2-11a) Þ (A2-11b) が成り立つような推論体系では、P Þ Q と P が成り立てば、(A2-11a) の上段と P に ( 切断 ) を適用すれば Q が得られます。これは R に Q を代入した (A2-11a) が成り立つことを意味するので、仮定により R に Q を代入した (A2-11b) が成り立ちますが、その上段は成り立っているのですから、下段すなわち Q が得られ、これは ( Þ 消去) が導出できたことを意味します。

　次に、ある公理系のもとで、P に現れない自由変数 z すなわち P にも公理にも現れない変数 z に対して命題 (z | x)P が成り立ったとします。これは、変数 z と任意の項 T に対して推論規則 ( 代入 ) を適用することにより (T | z)(z | x)P すなわち (T | x)P が成り立つことを意味するので、この状態のことを、すべての x に対して P 、あるいは "xP と表現することにし、この概念を形式化します。
　すなわち命題型量化記号 " と、「P に現れない自由変数 z に対して命題 (z | x)P が成り立っているとき命題 R が成り立つ」ということを意味する

(A2-12a) P に現れない自由変数 z に対して (z | x)P
———–
R が成り立つ。

(A2-12b) "xP
———
R が成り立つ。

という２つの条件が普遍的に同等になるような推論規則を追加することにします。

　このとき、本文第１節で与えた ( " 導入) という推論規則が " の導入規則になります。
　実際、( " 導入) と (A2-12b) を仮定すると、(A2-12a) の上段から ( " 導入) により "z(z | x)P すなわち "xP が導かれ、更に (A2-12b) により R が導かれるので、確かに (A2-12a) が導出されることがわかります。
　逆に (A2-12b) Þ (A2-12a) が成り立つような推論体系では、R に "xP を代入すれば (A2-12b) は自明に成り立つので、仮定により R に "xP を代入した (A2-12a) が成り立ちます。一方、自由変数 x に対して P が成り立ったとすると、P にも公理にも現れない変数 z を任意に選び、推論規則 ( 代入 ) を変数 x と項 z に対して適用することによりにより、(z | x)P すなわち (A2-12a) の上段が得られ、従って R に "xP を代入した (A2-12a) の下段、すなわち "xP が得られますが、これは推論規則 ( " 導入) が導出できたことを意味します。

　また、本文第１節で与えた ( " 消去) という推論規則が " の消去規則になります。
　実際、( " 消去) と (A2-12a) を仮定すると、"xP が成り立てば、P に現れない自由変数 z に対し、( " 消去) により (z | x)P が成り立ちます。ゆえに (A2-12a) により R が得られ、これは (A2-12b) が得られたことを意味します。
　逆に (A2-12a) Þ (A2-12b) が成り立つような推論体系では、P に現れない自由変数 z に対して (z | x)P が成り立てば、推論規則 ( 代入 ) を変数 z と任意に選んだ項 T に対して適用して (T | z)(z | x)P すなわち (T | x)P が得られますが、これは R に (T | x)P を代入した (A2-12a) が成り立つことを意味し、従って仮定により、R に (T | x)P を代入したときの (A2-12b) が成り立ちますが、これは ( " 消去) が導出できたことを意味します。

　次に、ある公理系のもとで、命題 P に対して、変数 x をある項 T に置き換えた命題 (T | x)P が成り立ったとします。しかもその項 T が具体的に何であるかには関心がなく、とにかくそのような項が存在するという事実だけに注目するとき、この状態のことを、P を満たす x が存在する、あるいは $xP と表現することにし、これを形式化します。
　すなわち命題型量化記号 $ と、「変数 x をある項 T に置き換えた命題が成り立っているとき命題 R が成り立つ」ということを意味する

(A2-13a) どんな項 T に対しても (T | x)P
————
R が成り立つ。

(A2-13b) $xP
———
R が成り立つ。

という２つの条件が普遍的に同等になるような推論規則を追加することにします。

　このとき、本文第１節で与えた ( $ 導入) という推論規則が $ の導入規則になります。
　実際、( $ 導入) と (A2-13b) を仮定すると、(A2-13a) の上段から ( $ 導入) により $xP が導かれ、更に (A2-13b) により R が導かれるので、確かに (A2-13a) が導出されることがわかります。
　逆に (A2-13b) Þ (A2-13a) が成り立つような推論体系では、R に $xP を代入すれば (A2-13b) は自明に成り立つので、仮定により R に $xP を代入した (A2-13a) が成り立ち、これは推論規則 ( $ 導入) が成り立つということに他なりません。

　また、本文第１節で与えた ( $ 消去) という推論規則が $ の消去規則になります。
　実際、( $ 消去) と (A2-13a) を仮定すると、$xP が成り立てば、P にも R にも現れない自由変数 z を任意に選んで P' :º (z | x)P と置くと、$xP は $zP' とも書けるので、$zP' が成り立ちます。次に P' を公理に追加した公理系では、P' の定義により (z | x)P が成り立ちますが、ここで (A2-13a) を T に変数 z を代入して適用すると R が得られますが、これはもとの公理系で P'├ R が成り立つことを意味します。ゆえに ( $ 消去) により R が得られ、これは (A2-13b) が得られたことを意味します。
　逆に (A2-13a) Þ (A2-13b) が成り立つような推論体系で、R に現れない自由変数 x に対して $xP と P├ R が成り立っているとします。このとき変数 x と任意の項 T に対し、推論規則 ( 代入 ) を P├ R に対して適用すれば、x が公理にも R にも現れないことから (T | x)P├ R が得られるので、推論規則 ( 切断 ) により (T | x)P から R が得られます。すなわち (A2-13a) が成り立つので、仮定により (A2-13b) が成り立ちますが、その上段の $xP は仮定により成り立っているので R が得られ、これは ( $ 消去) が導出できたことを意味します。

　さて、以上の議論を一般的に論じてみましょう。(A2-XXa) と書いた方の推論図の上段全体を、一つのメタ変数 C で表わします。ただし Ú の場合を考えればわかるように、このような C 自体が複数個ある場合もあるので、これを一般に C_i ( i = 1 ,¼, n ) と書くことにします。既に導入した論理記号 Ù , Ú , Þ , " , $ について一覧表を作れば、次のようになります：

s Ù Ú Þ " $
C₁ P
Q
P
P├ Q (z | x)P (T | x)P
C₂
Q

　さて、上の議論では、C₁ ,¼ C_n の中に登場する、命題を表わすすべてのメタ変数を P₁ ,¼, P_k とするとき、C₁ ,¼ C_n のうちのいずれかが成り立っている 、という状態のことを sP₁¼ P_k と表現し、これを形式化してきました。
　すなわち、新たな k 変項論理記号 s と、「C₁ ,¼ C_n のうちのどれかが成り立っているとき命題 R が成り立つ」ということを意味する

(A2-14a) C₁
——
R と C₂
——
R と … と C_n
——
R がすべて成り立つ。

(A2-14b) sP₁¼ P_k
————–
R が成り立つ。

という２つの条件が普遍的に同等になるような推論規則を追加するのでした。

　そして、各 i に対し、C_i を上段に持ち sP₁¼ P_k を下段に持つような推論規則を (s 導入_i) と名付ける、すなわち

(s 導入_i)
C_i
————
sP₁¼ P_k

と置けば、これら n 個の推論規則が、論理記号 s の導入規則になっています。
　実際、(s 導入_i) と (A2-14b) を仮定すると、(A2-14a) の上段 C_i から (s 導入_i) により sP₁¼ P_k が得られ、更に (A2-14b) により R が得られるので、確かに (A2-14a) 導出されることがわかります。
　逆に (A2-14b) Þ (A2-14a) が成り立つような推論体系では、R に sP₁¼ P_k を代入すれば (A2-14b) は自明に成り立つので、仮定により R に sP₁¼ P_k を代入した (A2-14a) が成り立ち、これは推論規則 (s 導入_i) が成り立つということに他なりません。

　それでは、この一般論で、C_i そのものを全く与えない、すなわち n がゼロ個の場合を考えたらどうなるでしょうか。これは、「C₁ ,¼ C_n のうちのいずれかが成り立っている状態」において、その C₁ ,¼ C_n 自体が無いのですから、「どんな状態でもない」ということであり、そんな状態はありえないですから、これは要するに「ありえない状態」という意味になります。
　そこで、この「ありえない状態」のことを、矛盾、あるいは ^ と書いて、この概念を形式化します。
　すなわち、この場合、C₁ ,¼ C_n 自体が一つも無いのですから、k も 0 であり、従って ^ という 0変項論理記号を追加し、また条件 (A2-14a) は空な条件、すなわちどんな場合にも常に成り立っている条件になるので、これと (A2-14b) の条件、すなわち

(A2-15) ^
——
R が成り立つ。

が普遍的に同等になるような推論規則を追加します。
　これは、要するに (A2-15) が常に成り立つような推論規則、言い換えると (A2-15) それ自体（すなわち本文第１節で与えた ( ^ 消去) ）を推論規則に追加する、ということに他なりません。
　ちなみに C₁ ,¼ C_n 自体が一つも無いことから、^ は導入規則を持たないことがわかります。

　さて、上で見てきたように、各論理記号 s とその推論規則を、証明文のある状態を形式化するという方法で“導出”してきましたが、このような議論は本文第２節のメタ定理５及びメタ定理６と実は密接な関係があるのです。以下、このことを一般論として解説しましょう。

　まず、(A2-14a) Þ (A2-14b) という条件は、

(A2-16) 　ある命題 R が、どの i に対しても、C_i が成り立っているときに導けるならば、R は sP₁¼ P_k が成り立っているときにも導ける。

と表現することができることに注意します。

　ところで各論理記号 s の推論規則は、(A3-14a) に出てくる推論図の上段にある C₁ ,¼ C_n によって規定されるわけですが、これらは論理記号 s の各導入規則の上段のことに他なりません。
　すなわち、各論理記号の推論規則を導出するという問題は、任意に与えられた導入規則に対する消去規則を如何にして求めるかという形に言い換えることができます。

　そこで、与えられた s の導入規則群 (s 導入_i) に対し、C_i と同様な、P_i あるいは P_j├ P_i の形のもの（場合によっては、更に何らかの項を変数に代入したもの）を何個か縦に並べた D によって

(e)
sP₁¼ P_k
D
—————
R

という形に書ける推論図を考え、このような推論図を一般に論理記号 s の消去図式とよぶことにしましょう。
　そして、複数個の消去図式群：

(s 消去_j)
sP₁¼ P_k
D_j
—————
R_j

をうまく選び、これらを推論規則に採用することによって条件 (A2-16) が成り立つようにするにはどうしたらよいかを考えてみましょう。

　一般に、消去図式 (e) の最上段の sP₁¼ P_k を、(s 導入_i) の上段である C_i で置き換えて得られる図式：

(s_i-e)
C_i
D
———
R

が構造に関する推論規則だけを使って導出可能なとき、消去図式 (e) は s の導入規則に対して局所整合（locally consistent）であるといいます。

　また、論理記号 s の導入規則 (s 導入_i) の下段の sP₁¼ P_k の頭の論理記号 s を別の新しい記号 s' に置き換えて得られる図式を (s' 導入_i) と書く、すなわち

(s' 導入_i)
C_i
————
s'P₁¼ P_k

と置きます。ここで、sP₁¼ P_k が成り立つとき、構造に関する推論規則と推論規則群 (s 消去_j) と推論規則群 (s' 導入_i) のみを使って s'P₁¼ P_k が導出できるとき、推論規則群 (s 消去_j) は s の導入規則に対して局所完全（locally complete）であるといいます。

　本文第２節のメタ定理５は、特に P' と Q' がそれぞれ P と Q の場合を考えると、論理記号 Ù , Ú , Þ , " , $ , ^ の各消去規則は導入規則について局所完全であることを示しています。
　また、メタ定理６は、論理記号 Ù , Ú , Þ , " , $ , ^ の各消去規則は導入規則について局所整合であることを示しています。

　そこで次に、推論規則群に関する局所整合性とか局所完全性という概念が、形式上どういう意味を持つのかということについて考察しましょう。

　最初は局所完全性の特徴付けです：

(A2-17) 推論規則群 (s 消去_j) が局所完全ならば、性質 (A2-16) が成り立つ。

　実際、(A2-16) の前提、すなわちある命題 R が、どの i に対しても、その上段 C_i から導出できると仮定します。これは、C_i を上段に持ち R を下段に持つ推論図が導出可能であることを意味します。
　ゆえに R のことを、新しい記号 s' を用いた“省略記法”で s'P₁¼ P_k 表すと、これは推論規則 (s' 導入_i) が成り立つことを意味しています。ゆえに (s 消去_j) が局所完全であるという仮定により、sP₁¼ P_k が成り立っていれば、s'P₁¼ P_k すなわち R が導けることがわかりますが、これは (A2-16) が成り立っていることを意味しています。

　次は局所整合性の特徴付けです：

(A2-18) 論理記号 s に対して (A2-16) が成り立つような論理的な理論では、局所整合な消去図式は導出可能である。

　実際、(A2-16) が成り立っているものとし、(e) を局所整合な消去図式とします。
　このとき、“局所整合な消去図式”の定義により、(e) の最上段にある sP₁¼ P_k を (s 導入_i) の上段で置き換えて得られる図式 (s_i-e) は導出可能です。
　ここで (e) の上段、すなわち sP₁¼ P_k と D がすべて成り立っていると仮定します。
　すると、この状態で更に (s 導入_i) の上段である C_i が成り立っていれば、(s_i-e) の上段である C_i と D がすべて成り立つので、(s_i-e) が導出可能であることから、その下段である R が導出できますが、これは (A2-16) の前提部分、すなわち「R が、どの i に対しても、C_i が成り立っているときに導ける」が成立していることを意味します。
　ところが仮定により (e) の上段がすべて成り立っているので、特に sP₁¼ P_k が成り立っています。ゆえに、(A2-16) の結論部分、すなわち「R は sP₁¼ P_k が成り立っているときにも導ける」により、R が成り立つことがわかり、これは (e) が導出可能であることを意味しています。

　以上の議論をまとめると、与えられた導入規則群 (s 導入_i) に対して局所完全な推論規則群 (s 消去_j) を推論規則に追加すれば (A2-16) の性質が成り立ち、逆に (A2-16) の性質が成り立てば、(s 導入_i) に対して局所整合な推論規則群 (s 消去_j) は導出可能です。
　従って特に、局所完全な推論規則から局所整合な推論図は導出可能であることがわかります。
　ゆえに、局所整合かつ局所完全な推論規則が２種類存在すれば、一方から他方が導出可能なので、両者は同等な推論規則であるといえます。すなわち局所整合かつ局所完全な推論規則は本質的に一組しか存在しないことがわかり、こうして一意に定まる推論規則群を、もとの導入規則に対して共役な推論規則群とよぶことにしましょう。
　論理記号 Ù , Ú , Þ , " , ^ の場合に求めたような、(A2-16) の成立を保証する推論規則群 (s 消去_j) は、局所整合かつ局所完全、すなわち共役な消去規則です。

　ところで、論理記号だけでなく、述語記号である等号 º についても論理記号と同様な考察が可能です。
　すなわち、T が S と同一の項であるという状態のことを、S と T は等しい、あるいは S º T と表現することにし、この概念を形式化します。すなわち２変項述語記号 º と、「T が S と同一の項であるとき命題 R が成り立つ」ということを意味する

(A2-19a) T が S と同一の項
————————–
R が成り立つ。

(A2-19b) S º T
———
R が成り立つ。

という２つの条件が普遍的に同等になるような推論規則を追加することにします。

　このとき、本文第４節で与えた ( º 導入) という推論規則が º の導入規則になります。
　実際、( º 導入) と (A2-19b) を仮定すると、(A2-19a) の上段から ( º 導入) により S º T が導かれ、更に (A2-19b) により R が導かれるので、確かに (A2-19a) が導出されることがわかります。
　逆に (A2-19b) Þ (A2-19a) が成り立つような推論体系では、R に S º T を代入すれば (A2-19b) は自明に成り立つので、仮定により R に S º T を代入した (A2-19a) が成り立ち、これは推論規則 ( º 導入) が成り立つということに他なりません。

　また、本文第１節で与えた ( º 消去) という推論規則が º の消去規則になります。
　実際、( º 消去) と (A2-19a) を仮定すると、R の中に現れる項 T のところを R に現れない自由変数 x に置き換えて得られる命題を R' と書くと、R は (T | x)R' と書くことができます。ところで (A2-19a) により、T が S と同一の項なら R が成り立ちますが、これは R の T を S に置き換えた命題、すなわち (S | x)R' が成り立つことを意味します。ゆえに、S º T が成り立つ場合は、これと (S | x)R' に ( º 消去) を適用すれば、(T | x)R' すなわち R が得られ、これは (A2-19b) が成り立っていることを意味します。
　逆に (A2-19a) Þ (A2-19b) が成り立つような推論体系では、S º T と (S | x)P が成り立てば、R :º (T | x)P という命題は、もし T が S と同一の項であれば (S | x)P に一致するので、仮定により定理です。これは (A2-19a) が成り立つことを意味しているので、仮定により (A2-19b) が成り立ちますが、その上段 S º T は仮定により成り立っているので、下段の R すなわち (T | x)P が得られ、これは推論規則 ( º 消去) が導出できたことを意味します。

　また、第４節のメタ定理41により、論理記号の場合のメタ定理５、メタ定理６と同様な性質が成り立ち、この場合も消去規則が導入規則に共役な推論規則であることがわかります。

　さて、以上解説してきたことをまとめると、直観主議論理とは、すべての論理記号とその推論規則を、どういう命題がどのように証明されているかという超数学的な状態の中から有用なものを選んでこれを形式化することによって次々に理論を拡大していって得られた論理であるとみなすことができます。
　すなわち、直観主義論理の論理記号の消去規則というのは、勝手に定めたものではなく、与えられた導入規則に共役な推論規則として（本質的に）一意に定まる推論規則でなければならない、という条件が付いているわけです。
　もともと、消去規則は一般に導入規則より複雑な形をしていることや、消去規則には「場合分けの方法」「三段論法」「補助定数の方法」のように、まるで“法則”であるかのような名前が付けられているものがあることや、「矛盾からは何でも導くことができる」という推論規則を証明なしに認めることには違和感を感じることなど、消去規則には、より上位に何らかの指導原理があって、そこから導出されるものなのではないかという期待があったのですが、上記の議論は、まさにそのとおりであったことを示しています。

　ところで、上述のような“消去規則群が導入規則群に共役である”という性質は、直観主義論理に特徴的な性質で、古典論理にはないものです。実際、古典論理では、否定記号 Ø の導入規則と消去規則がこのような共役な関係になく、そのために、消去規則が論理記号の定義という役目を超えて“余計な命題”まで証明してしまうことがあることは、第３節の最後でコメントしたように、同節メタ定理39 (h),(i),(k) 、メタ定理40 (c) の例が示すとおりです。

　なお、直観主義論理のように、構文論的なある状態に注目し、その概念が満たす構文論的な性質をいくつか挙げ、その概念と性質を理論内部の概念として「形式化」するという理論拡大の方法は、第４節で導入した等号やε量化記号や第５節で導入した冪理論や再帰的集合論においても採用されている方法です。
　すなわち構成主義数学というのは、論理記号だけでなく、数学において導入すべき記号や推論規則や公理も、構文論的な概念とその概念が持つ性質を形式化するいう方法のみによって導入していく立場であるということができます。

　さて、以上の解説は、直観主義論理を純粋に構文論的な手法のみによって正当化する方法を述べたものですが、それでは数学のデファクト・スタンダードである古典論理を構文論的に正当化するにはどうしたらよいでしょうか。

　述語記号 p 、論理接続詞 s 、命題型量化記号 π に対し、p˜ 、s˜ 、π˜ をそれぞれ

(A2-20a) p˜T₁¼ T_k ~~:º ØØ~~ pT₁¼ T_k

(A2-20b) s˜P₁¼ P_k ~~:º ØØ~~ sP₁¼ P_k

(A2-20c) π˜xS ~~:º ØØ~~ πxS

で定義し、論理式 S の中の述語記号 p 、論理接続詞 s 、命題型量化記号 π をすべて p˜ 、s˜ 、π˜ に置き換えて得られる文字列を S˜ と書くことにすると、明らかに次が成り立ちます：

(A2-21a) x˜ は x である。

(A2-21b) 関数記号 f に対し、( f T₁¼ T_k)˜ は f T₁˜¼ T_k˜ である。

(A2-21c) 述語記号 p に対し、( pT₁¼ T_k)˜ は p˜T₁˜¼ T_k˜ である。

(A2-21d) 論理接続詞 s に対し、(sP₁¼ P_k)˜ は s˜P₁˜¼ P_k˜ である。

(A2-21e) 命題型量化記号 π に対し、(πxS)˜ は π˜xS˜ である。

(A2-21f) 項型量化記号 τ に対し、(τxS)˜ は τxS˜ である。

(A2-21g) 項 T に対し、((T | x)S)˜ は (T ˜ | x)S˜ である。

　この (A2-21c),(A2-21d),(A2-21e) と (A2-20) により、命題 P に対する P˜ は、ある命題の二重否定の形になっていますから、メタ定理20により

(A2-22) 命題 P に対し、P˜ とその二重否定 ØØP˜ は同値である。

ということがわかります。

　さて、Ù , Ú , Þ , " , $ , ^ のいずれかを s と表わし、上に掲げた s の導入規則 (s 導入_i) に対して

(s˜ 導入_i)
C_i˜
—————
(sP₁¼ P_k)˜

という図式は導出可能です。ただし C_i˜ は、C_i 及び公理 Γ を構成する各命題 P をすべて P˜ に置き換えたものを表し、下段においても公理 Γ を構成する命題については同様の書き換えを行った Γ˜ に置き換えることにします。
　実際、(s 導入_i) を Γ˜ , P₁˜ ,¼, P_k˜ に対して適用することにより、(s˜ 導入_i) の上段から Γ˜ ® sP₁˜¼ P_k˜ が得られ、更に第３節メタ定理19により、結論を二重否定した Γ˜ ® s˜P₁˜¼ P_k˜ すなわち Γ˜ ® (sP₁¼ P_k)˜ が得られます。
　また、上に掲げた s の消去規則 (s 消去_j) に対して

(s˜ 消去_j)
(sP₁¼ P_k)˜
D˜
—————–
R_j˜

という図式は導出可能です。ただしこの場合も公理 Γ は Γ˜ に置き換えるものとします。
　実際、(s 消去_j) を Γ˜ , P₁˜ ,¼, P_k˜ に対して適用することにより、Γ˜ ® sP₁˜¼ P_k˜ と (s˜ 消去) 上段の２段目以降のsequentが定理なら、Γ˜ ® R_j˜ も定理であることがわかります。
　ゆえに、(s˜ 消去_j) 上段の２段目以降のsequentが定理なら、対偶に関するメタ定理17を２回適用して、Γ˜ ~~® ØØ~~ sP₁˜¼ P_k˜ から Γ˜ ~~® ØØ~~ R_j˜ が得られます。ところが ØØ sP₁˜¼ P_k˜ は (sP₁¼ P_k)˜ であり、ØØ R_j˜ は (A2-22) により R_j˜ と同値ですから、これは (s˜ 消去_j) が導出されたことを意味します。

　さらに、(A2-21g) に注意すれば、第４節の等号 º を º˜ に置き換え、第５節の Î を Î˜ に置き換えても、全く同じ推論規則が成り立つことは明らかです。

　さて、P Þ˜ ^˜ を Ø˜P と略記すれば、^˜ すなわち ~~ØØ^~~ は、メタ定理11により ^ と同値ですから、メタ定理５、20により Ø˜P は ØØ(P ~~Þ ^~~) すなわち ~~ØØØ~~P すなわち ØP と同値です。ゆえにメタ定理32により、直観主義論理のもとで

(A2-23) Γ˜ ® P˜ Ú˜ Ø˜P˜

が成り立ちます。

　一般に、命題 P を P˜ に置き換える操作を、（直観主義世界における）P の古典論理的解釈とよぶことにします。すると、上で示したことは、古典論理の証明文を構成するsequentに現れる命題を一斉に古典論理的に解釈すると、これは直観主義論理の証明文になる、ということです。すなわち次の結果が得られました：

(A2-24) 古典論理で Γ ® R が証明可能なら、直観主義論理で Γ˜ ® R˜ は証明可能である。

　ちなみに R と R˜ は古典論理では同値ですから、(A2-24) の逆は明らかです。

　ところで (A2-22) とメタ定理38により、s が Ù , Þ , " のとき、sP₁˜¼ P_k˜ はある命題の否定命題の形に表わされます。よってメタ定理20により、これらは二重否定を取ったもの s˜P₁˜¼ P_k˜ と同値になります。以上のことは、メタ定理11により s が ^ の場合にも成り立っています。すなわち

(A2-25) s が Ù , Þ , " , ^ のいずれかのときは、sP₁˜¼ P_k˜ と s˜P₁˜¼ P_k˜ は直観主義論理で同値である。

ということがわかります。s˜ というのは s を古典論理的に解釈したものですから、論理記号が Ù , Þ , " , ^ のときにそれと s が（直観主義論理で）同値だということは、これらの論理記号について“古典論理と直観主義論理で意味が同じである”ということを意味します。

　それでは論理記号 Ù , Þ , " , ^ と、それ以外の論理記号 Ú , $ には形式上どういう違いがあるのでしょうか。
　直観主義論理では、消去規則は導入規則の共役な推論規則として一意的に定まるものでしたから、論理記号の性質は導入規則によって決定されるはずです。
　そこで、各論理記号の導入規則を眺めると、論理記号が Ù , Þ , " , ^ である場合、その場合に限って導入規則の下段が与えられれば上段が復元できる、すなわち「証明文の中で、sequent Γ ® sP₁¼ P_k が論理記号 s に関する導入規則を適用して得られた」という情報だけで、その推論に使った推論規則の上段が一意的に定まることがわかります。
　例えば Ù の場合、Ù の導入規則は一つしかなく、下段のsequentを Γ ~~® P Ù~~ Q とすると、P Ù Q という論理式の中に P と Q が含まれているので、( Ù 導入) の上段は実は Γ ® P と Γ ® Q であったということが復元できます。Þ についても同じです。また " についても、自由変数の違いを除けば上段が一意に決まります。
　これに対し、Ú の場合、導入規則により Γ ~~® P Ú~~ Q というsequentが得られたとしても、Ú に関する導入規則は２つあるので、下段の情報だけではどちらの導入規則を用いたのかがわからず、従って上段を一意的に復元することができません。$ の場合も、上段に現れる項 T が下段では失われているので、やはり下段の情報だけで上段を復元することはできません。
　そこで、導入規則の下段の情報だけから上段が復元できるような論理記号を復元可能であるということにすれば、上記の事実は

(A2-26) 直観主義論理においては Ù , Þ , " , ^ は復元可能であり、Ú , $ は復元可能でない。

と表現することができ、(A2-25) は“復元可能な論理記号は古典論理でも直観主義論理でも意味が同じ”であることを示しています（付録９で、(A2-25) の逆も成り立つことを確かめます）。
　さて、復元可能な論理記号については、次のメタ定理が成り立ちます。

(A2-27) 　s は復元可能な論理記号で、局所完全な消去規則を持つものとする。このとき、導入規則の下段のsequentが定理ならば、上段のsequentもすべて定理である。

　実際、s が復元可能ならば、Γ ® sP₁¼P_k を下段に持つ上段 C は一意的に決まるので、C を構成する各sequent S は、一意的に定まる (s 導入) の上段である C が成り立つときは明らかに証明可能です。ゆえに、消去規則が局所完全であるという仮定により、S は下段のsequent Γ ® sP₁¼P_k が証明可能なら証明可能です。

　以上の準備のもとで、次のメタ定理が証明できます。

(A2-28) 　s は復元可能で、局所完全な消去規則を持つ k 変項論理記号とし、その導入規則の上段のsequentはすべて Γ, Δ_i ® P_{j_i} の形を持つものとする。このとき、P₁ ,¼, P_k がそれぞれ二重否定と自分自身が直観主義論理で同値ならば、sP₁¼ P_k も二重否定と自分自身は直観主義論理で同値である。従って特に sP₁˜¼ P_k˜ と s˜P₁˜¼ P_k˜ は同値である。

　実際、公理 Γ が sP₁¼ P_k のみからなる場合を考えると、明らかに Γ ® sP₁¼ P_k が成り立つので、(A2-27) により、Δ_i, sP₁¼ P_k ® P_{j_i} が成り立ちます。
　ゆえにメタ定理17を２度使えば Δ_i, ØØ sP₁¼ P_k ~~® ØØ~~ P_{j_i} が導けます。ところが P_{j_i} はその二重否定と同値ですから、Δ_i, ØØ sP₁¼ P_k ® P_{j_i} が成り立ちます。
　これは、公理 Γ が ØØ sP₁¼ P_k のみからなる場合に Γ, Δ_i ® P_{j_i} が成り立つことを意味しており、従って (s 導入) により、Γ ® sP₁¼ P_k すなわち ØØ sP₁¼ P_k ® sP₁¼ P_k が得られますが、これは (A2-28) が成り立つことを意味しています。
　この性質 (A2-28) こそが、(A2-25) が成り立つ形式上の理由だということができます。

	(s˜ 消去_j)
	(sP₁¼ P_k)˜ D˜ —————– R_j˜