このノートでは、以下に定式化するロビンソン算術 N_1 から、
次の論理式が証明不可能であることを
有限の立場で証明する：
∀x(k_n≦x∨x≦k_n)
ここに、k_n とは、超数学的自然数 n に対して、
N_1 の定数 0 の前に S を n 個並べたものである。
（k_n は n に対応する数項と呼ばれる。）
また、x≦y は ∃z(x+z=y) の略とする。
1.1
N_1 の土台となる論理体系は、等号述語論理で、
等号は x=y で表す。
N_1 の関数記号は 0変数関数記号(定数) 0,
1変数関数記号 S, 二変数関数記号 +, ・である。
N_1 の述語記号は二変数述語記号 = である。
1.2
N_1 の公理系：
N_1 は、等号述語論理の公理系のほかに、
次の明示的公理を持つものとする：
N(1) ∀x(Sx≠0)
N(2) ∀x∀y(Sx=Sy ⇒ x=y)
N(3) ∀x(x+0=x)
N(4) ∀x∀y(x+Sy=S(x+y))
N(5) ∀x(x・0=0)
N(6) ∀x∀y(x・Sy=(x・y)+x)
N(7) ∀x(x≠0⇒∃y(x=Sy))
よって、N_1 の明示的公理は確かに有限個である。
2.
証明のために、形式的体系 N_1 を拡張し、
次のような形式的体系 N_2 を考える:
2.1
N_2 における記号は, N_1 における記号に加えて、
定数記号 ω, λ と 1変数関数記号 B である。
2.2
N_2 の土台となる論理体系は等号述語論理で、
明示的公理は N(1)～N(6) に加え、次の N(8)
である:
N(8) ∀x(x≠0 ⇒ x=SBx)
等号述語論理のもの以外の N_2 の公理シェーマは、次の S1 である:
S1 n が超数学的自然数のとき、論理式
∀y ( (k_n +y≠ω) ∧ (ω+y≠k_n) )
は公理である。
3
明らかに、N_2 は N_1 よりも強い理論である。
3.1
そこで、N_2 が無矛盾であることを示す。
3.2
そのために、超限数とそれらの間の演算の概念を有限の立場で導入する。
3.3
3.3.1: 図形 0 は自然数である。
3.3.2: 図形 n が自然数ならば、図形 Sn は自然数である。
3.3.3: 以上によって定義されたもののみが、自然数である。
3.4
3.4.1: 自然数は超限数である。
3.4.2: 図形 ω、λは超限数である。
3.4.3: 以上によって定義されたもののみが、超限数である。
3.5
超限数の間の関係 x=y は、x と y が
同じ図形のときのみに正しいと定義する。
3.6
ω、λに対しては、Sω :=ω, Sλ:=λ
と定義する。
3.7
B0 := 0, Bk_{n+1} := k_n,
Bω:=ω, Bλ:=λ
と定義する。ここに、n は超数学的自然数。
3.8
+ の解釈：超数学的自然数 n, m に対し、
k_n + k_0 = k_n, k_n + (Sk_m) := S(k_n + k_m),
k_n +ω :=λ, k_n +λ:=λ,
ω + k_n := ω, λ + k_n := λ,
ω+ω:=ω, ω+λ:=ω, λ+ω:=λ, λ+λ:=λ
と定義する。
3.9
・の解釈：超数学的自然数 n, m に対し、
k_n・k_0 = k_0, k_n ・(Sk_m) := (k_n・k_m) + k_n,
k_n ・ω:=λ, k_n・λ:=λ,
ω・k_0 := k_0, ω・k_{n+1} := λ,
λ・k_0 := k_0, λ・k_{n+1} := λ,
ω・ω:=ω, ω・λ:=λ, λ・ω:=ω, λ・λ:=λ
と定義する。
3.10
N_2 の論理式で自由変数と∀と∃を含まないものについては、
上記 3.3～3.9の有限の立場の解釈の下で成り立つ命題のとき、
そのときに限り、真とする。
3.11
N_2 の公理で等号述語論理の公理でないものは全て正規で、
その完全分解公理については、3.10 の意味で全て真である。
(「正規」、「完全分解公理」と言う用語については、
竹内外史・八杉満里子「証明論入門」pp.52-58
を参照のこと。)
3.12
また、N_2 の公理で等号述語論理の公理であり
なおかつ述語論理の公理でないもので、
自由変数と∀と∃を含まないものについては、
3.10 の意味で全て真である。
3.13
従って、竹内外史・八杉満里子「証明論入門」
p.59, 4.18 より、N_2 は無矛盾である。
4
よって、もし、ある超数学的自然数 n に対して N_1 から論理式
∀z(k_n≦z∨z≦k_n)
が証明可能であれば、それは N_2 からも証明可能で、
したがって、N_2 からは論理式
k_n≦ω∨ω≦k_n
が証明可能となる。
従って、N_2 からは論理式
∃y(k_n +y=ω∨ω+y=k_n)
が証明可能で、公理シェーマ S1 と合わせて
N_2 が矛盾することになり、これは不合理である。
よって、任意の超数学的自然数 n に対し、N_1 からは論理式
∀z(k_n≦z∨z≦k_n)
は証明不可能である。
補足：上記解釈の下で、N_1 からは論理式
∀x(x+k_n = k_n +x),
∀x(0・x = x・0),
∀x(x≠Sx)
などは証明不可能であることがわかる。
従って、たとえば、倉田令二郎著「入門数学基礎論」p.145 に於いて、
論理式 ∀z(k_n≦z∨z≦k_n) が上記 N_1 から証明可能であるという
記述があるが、それは間違っている。
参考文献
文責: Dr. Kazuyoshi Katogi (加藤木 一好)
