数理科学と日本古代史のブログ

　今までに、“形式化の原理”、すなわち特定の記号列、あるいは記号列に関する特定の状態に名前を付け、それが持つ構文論的な性質を列挙し、しかる後にその名前を付けたモノを理論内部の記号として改めて追加すると共に、それが持っていた構文論的な性質を推論規則あるいは公理の形に翻訳する、という方法で理論拡大していく手法を具体的に説明してきました。
　独断的な名前ですが、こうして得られた理論を「根拠のある理論」と呼ぶことにしましょう（もちろん、これは“根拠がある”という概念に対する考え方の一つに過ぎず、それ以外の考え方は誤りだ！などと主張するものではありませんので念のため）。
　このとき、今までの議論により、以下の結果が得られたことになります。

(1) 自然推論や（右辺が１個からなる）sequent計算における、論理記号に無関係な推論規則 (増、減、換、カット、代入）は根拠がある。

(2) 論理記号 ∧ ∨ ⇒ ∀ ∃ ⊥ とそれらに対する直観主義論理の推論規則は根拠がある（排中律 R∨¬R は、推論規則としては根拠がない）。

(3) 派生的に定義される論理記号 ⇔ ¬ は根拠がある。

(4) 等号 ＝ やε量化記号と、それに対する推論規則は根拠がある（ただし、いわゆるε公理：∀x(P(x)⇔Q(x)) ⇒ εxP(x)＝εxQ(x) は根拠がない）。

(5) 理論 τ に根拠があれば、その冪理論 τ* は根拠がある。

(6) 理論 σ と理論 τ に根拠があれば、それらの和理論 σ∨τ も根拠がある。

(7) 理論 τ に根拠があれば、その再帰的集合論 τ' は根拠がある（特に、(a)τ項全体からなる集合の存在、(b)非順序対の公理、(c)和集合の公理、(d)冪集合の公理、(e)分出公理、更には (a) と (e) から得られる空集合の存在、ε量化記号を用いることによって導かれる選択公理は根拠がある。これに対して外延性公理 set(A)∧set(B)∧∀x(x∈A ⇔ x∈B) ⇒ A＝B は根拠がない）。

　以上ですが、実は一つだけ不足しているモノがあります。
　それは、以上の (1)〜(7) だけだと、スタート地点に当たる「根拠のある理論」について何も書いていないため、等号とε量化記号を持つ直観主義の述語論理という「一般論の枠組み」以外の理論、すなわち根拠のある理論の具体例が作れない、ということです。

　これでは困るのですが、さりとて「自然数論 N は根拠がある」などという主張を付け加えるのは感心しません。クロネッカーの時代ならいざ知らず、形式主義の浸透したこの現代に「自然数が天与のものだと思え」というのも無理な注文です。
　もっとも、証明論とか有限の立場で議論するときは、自然数の存在についてはアプリオリに認めてしまうのが普通ですが、それだって、便宜的な立場に過ぎず、「自然数という概念なら根拠がある」と先験的に考えるのは、やはり一種の“信仰”でしょう。

　そこで、「これなら“根拠がある”と言ってもよいだろう」と誰もが思えるようなモノとして、次の主張を加えることにします：

(0) 空な理論 σ （すなわち存在述語記号 σ を持つというだけで、σ に関する推論規則も公理も一切持たない）は根拠がある。

　つまり、記号 σ を導入するだけで、それに関して何が成り立つことも仮定しないのですから、これこそ“究極の”根拠がある理論ということになります（笑）。

　こんな理論を根拠があると認めたって、何の価値も無いじゃないかと思うかもしれませんが、この (0) と (7) を組み合わせると、なんと自然数論が展開できるのです。
　具体的には、空な理論 σ の再帰的集合論 τ ≡ σ' において、次のように定義します：

(8) 0 ≡ { x∈'[σ]' | ⊥ }'

(9) s(x) ≡ {x}' ≡ {x, x}'

　ただし、σ' における集合の帰属関係を ∈' で、σ項の全体からなる集合を [σ]' で、分出集合を {x∈'a|R(x)}' で、非順序対を {a,b}' で表わすことにしました。これは、τ≡σ' に対して再度、再帰的集合論を取りたいので、ダッシュ無しの記号は τ 上の再帰的集合論のために取っておきたいからです。
　そこで、τ の再帰的集合論 τ'≡σ'' において次のように定義します（見易さのため、τ' における集合に関する概念を意図している変数をラテン大文字で表わすことにします）：

(10) Ind(A) ≡ 0∈A ∧ ∀x[x∈A ⇒ s(x)∈A]

(11) N(x) ≡ ∀A [Ind(A) ⇒ x∈A]

　このとき、１変項述語記号 N は次の性質を満たします：

(12a) N(0)

(12b) ∀x [N(x) ⇒ N(s(x))]

(12c) ∀x [N(x) ⇒ s(x)≠0]

(12d) ∀x ∀y [N(x)∧N(y)∧s(x)＝s(y) ⇒ x＝y]

(12e) R(0)∧∀x[N(x)∧R(x) ⇒ R(s(x))] ⇒ ∀x[N(x) ⇒ R(x)]

　実際、(12a) と (12b) は Ind と N の定義から明らかです。
　また、(12c) 以下を示す前に、

(13) ∀x [N(x) ⇒ τ(x)]

を確かめておきましょう。
　実際、0 の定義 (8) により、σ'(0) ですから、0∈[σ']≡[τ] です。
　また、x∈[τ] すなわち τ(x) すなわち σ'(x) なら、(9) と再帰的集合論 σ' における非順序対の公理により s(x)≡{x}' は σ'元です。すなわち σ'(s(x)) すなわち τ(s(x)) すなわち s(x)∈[τ] です。
　以上と Ind の定義 (10) により、Ind([τ]) が成り立つことがわかりました。ゆえにこれと N の定義 (11) により、N(x) なら x∈[τ] すなわち τ(x) となるので、(13) が成り立ちます。

　この (13) を用いると、N(x) なら τ(x) すなわち σ'(x) なので、s(x) すなわち {x}' は再帰的集合論 σ' における空集合である 0 と等しくないことは明らかです。これはすなわち (12c) が成り立つことを意味しています。

　また、N(x) かつ N(y) かつ s(x)＝s(y) なら、やはり x と y は再帰的集合論 σ' のσ'項ですから、s(x)＝{x}' と s(y)＝{y}' が成り立ち、従って {x}'＝{y}' が成り立ちます。ところが z∈'{x}' ⇔ z＝x と z∈'{y}' ⇔ z＝y が成り立ちますから、x＝y が得られ、従って (12d) も成立します。

　最後に (12e) ですが、これは、命題 R(x) に対して

(14) A≡{ x∈[τ] | N(x) ∧ R(x) }

と置くと、まず明らかに 0∈A であり、また x∈A なら、(12e) の前提部分と (12b) により s(x)∈A ですから、Ind(A) が成り立ち、従って、N(x) なら x∈A が得られ、従って R(x) となって、(12e) の結論部分が得られます。

　以上により、理論 τ≡σ' は、ペアノの公理を満たす１変項述語記号 N を持つことがわかりました。そして、(13) によれば

(15) N(n) ⇔ n∈{ x∈[τ] | N(x) }

ですから、再帰的集合論 τ' は、自然数全体から成る集合 N≡{ x∈[τ] | N(x) } を持つことがわかりました。
　これは、再帰的集合論 τ'≡σ'' が、無限集合 N を持つことを意味し、集合論 τ' が事実上無限公理を満たすことを意味しています。

　以上の結論は、いわゆるフォン・ノイマン流の無限集合 ω の存在、すなわち「空集合を元に持ち、x を元に持てば x∪{x} を元に持つような集合が存在する」とは異なりますが、これは置換公理を前提にすれば単なる無限集合の存在と同値になります。我々は置換公理を持たないので両者の同値性までは言えませんが、順序数の一般論でも展開しない限り、通常の数学を展開するには我々の定義で十分です。

　以上の議論により、“形式化の原理”の立場において、無限公理にも“根拠がある”ことが確かめられました。