数理論理学(鹿島亮)6
自然数論は数学の最も基本的な分野
自然数論において、公理をどのように設定しても避けることのできない本質限界がある
定義
Nは自然数全体の集合
N = {0,1,2,3,……}
定義6.1.1 計算可能関数
N上のk変数関数fが計算可能であることの定義
これを計算するアルゴリズムが存在すること
どんな自然数が与えられてもそれに従って計算すれば、f(n1,n2,…nk)の値を正しく有限時間内に求められる計算手順が存在すること
Nの部分集合Sが計算可能であることの定義
Sに属する否かを判定するアルゴリズムが存在すること
どんな自然数が与えられてもそれに従って計算すれば、n∈Sかn∉Sかを正しく有限時間内に答えられる計算手順が存在すること
アルゴリズムが存在するの厳密な定義は省略
計算可能関数、計算可能集合の例1
計算可能関数
足し算
掛け算
計算可能集合
素数
計算可能関数、計算可能集合の例2
pair(x,y) := (x+y)(x+y+1)+2x
この関数は、自然数のすべてのペアを偶数と1対1に対応させる関数
pairの逆関数を次のように定める(適切な値がないときは0を返す)
left(z)
= x if zが偶数で、あるyについて、pair(x,y) = z のとき
このyが一意であるから、xがただ一つ決まる感じかなik.icon
= 0 if zが奇数のとき
right(z)
= y if zが偶数で、あるxについて、pair(x,y) = z のとき
= 0 if zが奇数のとき
上記はすべて計算可能である
pair
足し算と掛け算の有限回の組み合わせ
left(n)
nが奇数なら0 を返す
nが偶数なら
0 ≤ x ≤ n/2 かつ 0≤ y ≤ n/2 となるすべてのx,yの組み合わせ(有限個になる)についてpair計算してみて、その値がnに等しくなったときのxをleft(n)の答えとする
rightも同様
表現定理
論理式に関する表記方法
(φ→ψ)∧(ψ→φ) のことを φ⇄ψと略記する
論理式φのことをφ(x1,x2,…,xk)などと表記することがある
x1,x2,…,xkは互いに異なる変数
φ中のx1,x2,…,xkをそれぞれ代入可能な項t1,t2,…,tkですべて置き換えて得られる論理式をφ(t1,t2,…,tk)と表記する
不完全性定理は自然数論に関するもの
変数記号は自然数を指している
zeroを0
sucを後者関数
⨁を足し算
⨂を掛け算
⧀を不等号と読む
このような読み方を標準ストラクチャーと呼ぶ
以下のように規定されるストラクチャーNのことを標準ストラクチャーとよぶ
zero^N = 0
suc^N(x) = x+1
x⨁^N y = x+y
x⨂^N y = x×y
自然数論の公理を記述した9つの閉論理式
∀x¬(suc(x) = zero)
∀x∀y(suc(x) = suc(y) → x = y)
∀x(x⨁zero = x)
∀x∀y(x⨁suc(y) = suc(x⨁y))
∀x(x⨂zero = zero)
∀x∀y(x⨂suc(y) = (x⨂y)⨁x)
∀x¬(x⧀zero)
∀x∀y(x⧀suc(y) → (x⧀y)∨(x=y))
∀x∀y((x⧀y)∨(x=y)∨(y⧀x))
この9個の閉論理式からなる集合をBasicと呼ぶ
Basicを公理としてどんな論理式が導出できるか
ということを論じていく
自然数nに対して
suc(suc(……suc(zero)……))
sucをn回合成
という項(すなわち自然数nを意図する項)を$ \overline{n}と表記して、nの数値項(numeral)と呼ぶ
例
$ \overline{0}はzeroのこと
$ \overline{1}はsuc(zero)のこと
$ \overline{2}はsuc(suc(zero))のこと
https://scrapbox.io/files/688077557f27389297a6af7d.jpeg
https://scrapbox.io/files/688077584b2ed3aa35930df5.jpeg
上記のような簡単な命題でもBasicから導出するのは案外大変
Basicはある意味十分んな能力を持っているということを示すのが、表現定理
定義6.2.3
記号(1)
fはN上のk変数関数
x1,x2,……,x,yは相異なる変数記号
φ(x1,x2,……,xk,y)はx1,x2,……,x,y以外の変数記号が自由出現しない論理式
定義(1)
任意の自然数n1,n2,……,nkに対して、以下が成り立つことを「φ(x1,x2,……,xk,y) は Basic上で関数fを表現する」という
Basic ⊢ ∀y((y = $ \overline{f(n1,n2,…,nk)}) ⇄ φ($ \overline{n1},\overline{n2},…,\overline{nk},y)) (6.1)
また、このような論理式φ(x1,x2,……,xk,y)が存在することを「関数fはBasic上で表現可能である」という
記号(2)
XはNの部分集合
φ(x)はx以外の変数記号が自由出現しない論理式
定義(2)
任意の自然数nに対して、以下の2条件が成り立つことを「φ(x) は Basic上で集合Xを表現する」という
n ∈ X ならば Basic ⊢ φ($ \overline{n}) (6.2)
n ∉ X ならば Basic ⊢ ¬φ($ \overline{n}) (6.3)
また、このような論理式φ(x)が存在することを「集合XはBasic上で表現可能である」という
Basic上で表現可能な関数の例
自然上の引き算
関数
minus(x1,x2)
x1 - x2 if x1 ≥ x2 のとき
0 if x1 < x2 のとき
論理式
(y⊕x2 = x1)∨( (x1⧀x2)∧y=$ \overline{0})
条件6.1をどう満たしているかの例
n1=5, n2=2に対しては
Basic ⊢ ∀y((y=$ \overline{3}) ⇄ ((y⊕$ \overline{2} = $ \overline{5})∨( ($ \overline{5}⧀$ \overline{2})∧y=$ \overline{0}))
主張
自然数上の計算可能関数および計算可能集合はすべてBasic上で表現可能である
また逆に、Basic上で表現可能な関数と集合はすべて計算可能である
証明
証明は非常に長いので、教科書では省略
6.3ゲーデル数
αが項や論理式や導出図のときにαに割り当てられる自然数をゲーデル数と呼ぶ ⎾α⏋と表記する
pair関数を用いて、ゲーデル数を具体的に定義する
変数記号は可算無限個あるので
v1,v2,v3,……
とよぶことにする
定数記号と変数記号のゲーデル数
⎾zero⏋ = 3
⎾v1⏋ = 5
⎾v2⏋ = 7
⎾v3⏋ = 9
……
と3以上の奇数に順に割り当てる
関数を含む項のゲーデル数
再帰的に定義する
⎾suc(t)⏋ = pair(0,⎾t⏋)
⎾s⊕t⏋ = pair(1, pair(⎾s⏋,⎾t⏋))
⎾s⊗t⏋ = pair(2, pair(⎾s⏋,⎾t⏋))
論理式のゲーデル数
再帰的に定義する
⎾s=t⏋= pair(3,pair(⎾s⏋,⎾t⏋))
⎾s⧀t⏋= pair(4,pair(⎾s⏋,⎾t⏋))
⎾⊥⏋= 1
⎾¬φ⏋= pair(5,⎾φ⏋)
⎾φ∧ψ⏋= pair(6,pair(⎾φ⏋,⎾ψ⏋))
⎾φ∨ψ⏋= pair(7,pair(⎾φ⏋,⎾ψ⏋))
⎾φ→ψ⏋= pair(8,pair(⎾φ⏋,⎾ψ⏋))
⎾∀xφ⏋= pair(9,pair(⎾x⏋,⎾φ⏋))
⎾∃xφ⏋= pair(10,pair(⎾x⏋,⎾φ⏋))
導出図のゲーデル数
導出図は以下のどれかの形をしている
1. 自然演繹の導出図は単独の論理式
2.
𝓐
-----
φ
3.
𝓐 𝓑
----------
φ
3.
𝓐 𝓑 𝓒
-------------
φ
1の場合
その論理式のゲーデル数をそのまま導出図のゲーデル数とする
2の場合
pair(11,pair(⎾φ⏋,⎾𝓐⏋))
3の場合
pair(12,pair(⎾φ⏋,pair(⎾𝓐⏋,⎾𝓑⏋)))
4の場合
pair(13,pair(⎾φ⏋,pair(⎾𝓐⏋,pair(⎾𝓑⏋,⎾𝓒⏋))))
ゲーデル数の例
¬(zero ⧀ zero)
⎾¬(zero ⧀ zero)⏋ = pair(5,⎾zero ⧀ zero⏋) = pair(5, pair(4,pair(⎾zero⏋,⎾zero⏋))) = pair(5, pair(4,pair(⎾3⏋,⎾3⏋)))
= 7670140
ゲーデル数の定義について
定義自体は別の方法でも良い
重要な点は、項・論理式・導出図に一意に自然数が割り当てられること
そして、項・論理式・導出図に対する操作などがゲーデル数を介して自然数上の計算可能関数・計算可能集合として表せるということ
例
論理式φ
変数記号x
項t
が与えられたときに、φ[t/x]を作るという操作はN上の3変数関数として表すことができる
f(a,b,c)
⎾φ[t/x]⏋
if
aが論理式φのゲーデル数
bが変数記号xのゲーデル数
cが項tのゲーデル数
φ中のxにtが代入可能
0
それ以外のとき
ゲーデル数が適切に定義されていることで、この関数が計算可能になる
{⎾A⏋ | A は自然演繹の導出図である} (6.4)
すべての導出図のゲーデル数の集合が計算可能
つまり、任意に与えられ他自然数に対してそれが自然演繹の文法に正しく従った導出図のゲーデル数になっているか否かを判定するアルゴリズムが存在する
論理式は標準ストラクチャーの読み方によって「自然数についての命題」を意図している
しかし、ゲーデル数を介することで「項や論理式や導出図についての命題」と解釈することができるようになる
6.4 対角化定理
自己言及的な意味を持つ論理式を構成するための有用な定理を示す
記号
φ(x)はx以外の変数記号の自由出現を持たない任意の論理式
主張
次の条件を満たす閉論理式ψが存在する
Basic ⊢ ψ ⇄ φ(⎾ψ⏋)
証明
x以外の変数記号の自由出現を持たない論理式すべてを、そのゲーデル数の小さい順に並べる
p0(x), p1(x), p2(x),… 列(6.6)
自然数上の関数fを以下のように定義する
f(n) = ⎾pn($ \overline{n})⏋
ゲーデル数の定義からfは計算可能関数になる
表現定理によって、fはBasic上で表現可能
fを表現する論理式の変数記号を必要に応じて書き換えることで、次の条件を満たすθ(x,y)の存在がいえる
yはxと異なる変数記号。φ中に現れない
θ(x,y)はx,y以外の変数記号の自由出現を持たない
θ(x,y)はBasic上で関数fを表現する
すなわち任意の自然数nに対して以下が成り立つ
Basic ⊢ ∀y( (y = $ \overline{f(n)}) ⇄ θ($ \bar{n}, y )) (6.7)
ここで、論理式 ∃y(θ(x, y)∧φ(y)) (6.8)を考える
この論理式はφ(f(x))を意図している
メモ
φ($ \overline{f(0)}) , φ($ \overline{f(1)}) , φ($ \overline{f(2)}) などで良いじゃんと思ってしまうがこれは閉論理式になってしまい、xを変数と持つような形にうまくできない(はず)
φ($ \overline{f(x)})というものは作れない
これはx以外の変数記号を持たないので、列(6.6)に現れる
つまり、あるkが存在して、pk(x)が論理式(6.8)に等しくなっている
このkを数値項にして(6.8)のxに代入して得られる閉論理式
∃y(θ($ \overline{k}, y)∧φ(y)) をψとする
この論理式はφ(f(k))を意図している
これが求めるψになっていることを示すために次の2つを示す
Basic ⊢ φ($ \overline{⎾ψ⏋}) → ψ
Basic ⊢ ¬φ($ \overline{⎾ψ⏋}) → ¬ψ
Basic ⊢ φ($ \overline{⎾ψ⏋}) → ψ を示す
任意のnに対して、Basic ⊢ ∀y( (y = $ \overline{f(n)}) ⇄ θ($ \bar{n}, y )) が成り立つ
Basic ⊢ ∀y( (y = $ \overline{f(k)}) ⇄ θ($ \bar{k}, y )) が成り立つ
n = kとする
Basic ⊢ ( ($ \overline{⎾ψ⏋} = $ \overline{f(k)}) ⇄ θ($ \bar{k}, $ \overline{⎾ψ⏋} ))
∀除去して、yに$ \overline{⎾ψ⏋}を代入
Basic ⊢ θ($ \bar{k}, $ \overline{⎾ψ⏋} )
($ \overline{⎾ψ⏋} = $ \overline{f(k)})は以下より成り立つ
f(k) = ⎾ρk($ \bar{k})⏋ = ⎾∃y(θ($ \bar{k},y) ∧ φ(y) )⏋ = ⎾ψ⏋
Basic ⊢ φ($ \overline{⎾ψ⏋}) →(θ($ \bar{k}, $ \overline{⎾ψ⏋} ) ∧ φ($ \overline{⎾ψ⏋}))
θ($ \bar{k}, $ \overline{⎾ψ⏋} )に対して、φ($ \overline{⎾ψ⏋})を仮定して、∧導入して、→導入して仮定を落とせば良い。
Basic ⊢ φ($ \overline{⎾ψ⏋}) →∃y(θ($ \bar{k}, y ) ∧ φ(y))
φ($ \overline{⎾ψ⏋}) →(θ($ \bar{k}, $ \overline{⎾ψ⏋} ) ∧ φ($ \overline{⎾ψ⏋}))に対して、φ($ \overline{⎾ψ⏋})を仮定して、∃導入して、→導入する
Basic ⊢ ¬φ($ \overline{⎾ψ⏋}) → ¬ψを示す
¬ψは∀y(θ($ \bar{k},y )→¬φ)と同値
Basic ⊢ ¬φ($ \overline{⎾ψ⏋}) → ∀y(θ($ \bar{k},y )→¬φ)を示せば良い
Basic ⊢ ¬φ($ \overline{⎾ψ⏋}) → ∀y((y=$ \overline{⎾ψ⏋})→¬φ(y))
等号に関する推論より
もう少し詳細に説明すると
¬φ($ \overline{⎾ψ⏋}) を仮定する
(y=$ \overline{⎾ψ⏋})を仮定する
等号規則より ¬φ(y)
→導入で、(y=$ \overline{⎾ψ⏋})→¬φ(y)
∀導入で、∀y((y=$ \overline{⎾ψ⏋})→¬φ(y))
→導入で、¬φ($ \overline{⎾ψ⏋}) → ∀y((y=$ \overline{⎾ψ⏋})→¬φ(y))
Basic ⊢ ¬φ($ \overline{⎾ψ⏋}) → ∀y((y=$ \overline{f(k)})→¬φ(y))
f(k)=⎾ψ⏋であるから、$ \overline{f(k)}=$ \overline{⎾ψ⏋} であるので等号規則を適用して得られる
Basic ⊢ ¬φ($ \overline{⎾ψ⏋}) → ∀y(θ($ \overline{k},y)→¬φ(y))
¬φ($ \overline{⎾ψ⏋}) → ∀y((y=$ \overline{f(k)})→¬φ(y))に対して
¬φ($ \overline{⎾ψ⏋}) を仮定して、→除去
∀除去をして、(y=$ \overline{f(k)})→¬φ(y)を得る
θ($ \overline{k},y)を仮定する
(6.7)より、Basic ⊢ θ($ \bar{k}, y )→(y = $ \overline{f(k)})
¬φ(y)を得る
→導入でθ($ \overline{k},y)→¬φ(y)
∀導入で、∀y(θ($ \overline{k},y)→¬φ(y))
→導入で、¬φ($ \overline{⎾ψ⏋}) → ∀y(θ($ \overline{k},y)→¬φ(y))
両方示せたので、ψは求める論理式となっている
メモ
一般に y = f(x) なら、 Basic ⊢ $ \overline{y}=$ \overline{f(x)}かな？
6.5
ゲーデルの不完全定理には第一定理と第二定理がある
第一定理はロッサーによって、改良が加えられた形がよく知られている
ω無矛盾って概念を聞いたことがある
定理6.5.1 Basicの無矛盾拡大からの導出可能性判定の計算不可能性
主張
以下の三条件を同時に満たす閉論理式集合Γは存在しない
1. Basic ⊆ Γ
2. Γは無矛盾である
3. Γから導出できる閉論理式全体のゲーデル数の集合{⎾φ⏋ | φ は閉論理式 Γ ⊢ φ} が計算可能である
言い換えると、任意に与えられた閉論理式がΓから導出できるか否かを判定するアルゴリズムがある
証明
方針
条件1,3を仮定して、Γが矛盾することを導く
条件3と表現定理6.2.4によって、論理式ρ(x) (ただしx以外の変数記号の自由出現を持たない) が存在し、以下の条件が任意の閉論理式φに対して成り立つ
Γ ⊢ φ ならば Basic ⊢ ρ($ \overline{⎾φ⏋}) (6.9)
Γ ⊬ φ ならば Basic ⊢ ¬ρ($ \overline{⎾φ⏋}) (6.10)
ρ(x)は「ゲーデル数xの閉論理式はΓから導出できる」ということを表現した論理式である
¬ρ(x)に対して対角化定理を適用して、次のような閉論理式ψを作る
Basic ⊢ ψ ⇄ ¬ρ($ \overline{⎾ψ⏋}) (6.11)
ψは「自分自身はΓから導出できない」という自己言及的な意味を持つ論理式
ψはΓから導出できる
もしもΓ ⊬ ψ (6.12) であるとすると
6.10 から Basic ⊢ ¬ρ($ \overline{⎾φ⏋})
6.11 から Basic ⊢ ψ
条件1より、Γ ⊢ ψ
これは 6.12 に反する
したがって、Γ ⊢ ψ
Γ ⊢ ψ (6.13) であるが……
6.9 よりBasic ⊢ ρ($ \overline{⎾φ⏋})
6.11 より Basic ⊢ ¬ψ
条件1より、Γ ⊢ ¬ψ
これは 6.13 に反する
したがって、Γ ⊢ ¬ψ
6.12, 6.13を合わせて、Γが矛盾することになる
定理6.5.2 第一不完全定理
主張
以下の四条件を同時に満たす閉論理式集合Γは存在しない
1. Basic ⊆ Γ
2. Γは無矛盾である
3. Γのゲーデル数の集合 {⎾φ⏋| φ ∈ Γ} が計算可能である
4. どんな閉論理式φについても、φと¬φのどちらかはΓから導出できる
証明
Γが4つの条件すべてを満たしていると仮定する
これが定理6.5.1に反することを示す
任意に与えられた閉論理式φがΓから導出できるか否かは、次のアルゴリズムで判定することができる
【Γ⊢φ ならばYES, Γ⊬φ ならばNO と答えるアルゴリズム】
nを初期値とする
(†)
nが導出図のゲーデル数であり
その結論がφ、解消されていない仮定がすべてΓの要素になっているならば
YESと答えてアルゴリズムは終了する
(‡)
nが導出図のゲーデル数であり
その結論が¬φ、解消されていない仮定がすべてΓの要素になっているならば
NOと答えてアルゴリズムは終了する
いずれも成り立たないときは、nの値を1増やして同様に繰り返す
(†)、(‡)の判定は可能
導出図のゲーデル数の集合(6.4) は計算可能
定理の条件3 Γのゲーデル数の集合 {⎾φ⏋| φ ∈ Γ} が計算可能である
ことなどからいえる
このアルゴリズムの停止性(有限ステップで必ず答を出すこと)は条件4からいえる
このアルゴリズムが有限ステップで停止しないのは、Γ⊢φでもΓ⊢¬φでもないとき
Γ⊢φ か Γ⊬φ のどちらかが成り立つことは条件4から保証される
このアルゴリズムの正当性(出した答が必ず正しいこと)は条件2からいえる
Γ⊢φであるとき
出した答が誤っている(NOと答える)ことは、アルゴリズムの定義からΓ⊢¬φであるので、
Γ⊢φ かつ Γ⊢¬φ ということになり、条件2に反する
Γ⊢¬φであるとき
出した答が誤っている(YESと答える)ことは、アルゴリズムの定義からΓ⊢φであるので、
Γ⊢φ かつ Γ⊢¬φ ということになり、条件2に反する
このようなアルゴリズムが存在するので、定理6.5.1の条件3が成り立つ
条件1,2は定理6.5.1と定理6.5.2で共通
よって、これは定理6.5.1に反する
第一不完全性定理の内容
Basicは自然数に関する基本的な公理集合
ただこれだけでは、足りないのでさらに必要な閉論理式を加えて公理集合Γを得ることを考える
条件1を満たす
条件2,3は数学の公理が満たすべき条件
矛盾する公理集合からはなんでも証明できる
ので無意味
数学の理論を展開する際に公理は自明な出発点
「何がその理論の公理で何が公理でないのか」すなわちφ∈Γ ? の判定が計算可能であることは必須
Γが有限集合ならば、この判定は明らかに計算可能
無限集合であっても、「あるパターンにあてはまる論理式全体」という場合は計算可能
条件4 (完全性)
Γが完全であるとはどんな閉論理式もΓから証明または反証ができるということ
すなわち現在未解決な問題を含めて論理式で記述可能などんな性質の成否もこの公理集合によって解明できるということ
自然数に関するすべての問題の成否を決着付けられる数学理論は存在しない
第一不完全性定理の応用
記号
Nは標準ストラクチャー
主張
次の条件を任意の閉論理式φに対して、成り立たせるような論理式τ(x) (x以外の変数記号の自由出現を持たない) は存在しない
N(φ) = 真 ⇔ N(τ($ \overline{⎾φ⏋})) = 真 (6.14)
証明
このようなτ(x)があると仮定する
¬τ(x)に対角化定理を適用して、以下を満たす閉論理式ψを得る
Basic ⊢ ψ ⇄ ¬τ($ \overline{⎾ψ⏋})
これから、 N(ψ ⇄ ¬τ($ \overline{⎾ψ⏋})) = 真 (6.15) となる
健全性定理より
しかし、N(ψ)が真であっても、偽であっても、(6.14)のφをψにした条件と(6.15)とは両立できない
N(ψ)=真 であるとする
(6.14)より
N(ψ) = 真 ⇔ N(τ($ \overline{⎾ψ⏋})) = 真
N(τ($ \overline{⎾ψ⏋})) = 真
(6.15)より
N(ψ ⇄ ¬τ($ \overline{⎾ψ⏋})) = 真
⇔ N((ψ → ¬τ($ \overline{⎾ψ⏋})) ∧ ((¬τ($ \overline{⎾ψ⏋}) → ψ)) = 真
⇔ N(ψ → ¬τ($ \overline{⎾ψ⏋})) = 真 かつ N(¬τ($ \overline{⎾ψ⏋}) → ψ) = 真
⇔ (N(ψ) = 偽 または N(¬τ($ \overline{⎾ψ⏋})) = 真 ) かつ (N(¬τ($ \overline{⎾ψ⏋})) = 偽 または N(ψ) = 真)
この二つの条件は両立できない
N(ψ)=偽 であるとする
同様にいえる
τ(x)は、任意の閉論理式の真理値をゲーデル数を介して定義する論理式といえる
この定理は「標準ストラクチャー上での真理値は論理式では定義できない」ということを示している
定理6.6.2 自然数上の真理決定不可能性定理
記号
Nは標準ストラクチャー
主張
Nで真になる閉論理式全体のゲーデル数の集合 {⎾φ⏋ | φは閉論理式でN(φ) = 真} は計算不可能である
任意に与えられた閉論理式が自然数上の通常の意味での
証明
Γ = {φ | φは閉論理式でN(φ) = 真} とすると、これは第一不完全性定理の条件1,2,4 を満たす(演習問題)
したがって、第一不完全性定理によって、条件3が否定される
定理6.6.3 恒真性の決定不可能性定理
任意に与えられた閉論理式が恒真である否かを判定するアルゴリズムは存在しない
証明
Basicの9個の閉論理式をβ1,β2,β3,…,β9と呼ぶ
任意の論理式φに対して次が成り立つ
Basic ⊢ φ
⇔ ⊢β1→(β2→(…(β9→φ)…))
2章演習問題2.8 より
⇔ β1→(β2→(…(β9→φ)…)) は恒真 ( ⊨ β1→(β2→(…(β9→φ)…)) とも書ける)
健全性定理・完全性定理より
題意のアルゴリズムが存在するならば上記の論理式が真か否かの判定ができる
これによって、Basic ⊢ φ かどうか。すなわちφがBasicから導出できるか否かの判定ができることになる
定理6.5.1 で Γ=Basicとした結果に反する
第一不完全定理の発展
この節では第二不完全性定理の概要を説明する
超準モデルというものをごく簡単に紹介する
第二不完全性定理のための準備1
閉論理式の集合Γがあり、その要素のゲーデル数の集合{ φ | φ ∈ Γ} が計算可能だとする
ここで自然数nに対する述語P(n)を次のように定める
メタ言語の述語か(対象言語の述語は=,⧀だけなので)
P(n)
nは導出図のゲーデル数
その結論は⊥
解消されていない仮定はすべてΓの要素
すなわち、nはΓから⊥を導く導出図のゲーデル数
任意に与えられた自然数nに対してP(n)が成り立つか否かを判定するアルゴリズムが存在する
P(x)という内容を記述した論理式π(x)を適切に作る
ただしx以外の変数記号の自由出現を持たない
π(x) ⇔ xはΓから⊥を導く導出図のゲーデル数である
という意味を表すことになる
集合{n ∈ N | P(n)}を定義6.2.3(2) の意味で表現する論理式
このπ(x)を使って作られる閉論理式 ∀x¬π(x) のことをConΓ と呼ぶ
ConΓは「どんな自然数もΓから⊥を導く導出図のゲーデル数ではない」
Γの無矛盾性を記述した閉論理式
第二不完全性定理のための準備2
ψの閉包
論理式ψ中に自由出現する変数記号がx1,x2,…,xnのとき、それらをすべて∀で束縛した閉論理式
∀x1,∀x2,…,∀xnψのことをψの閉包とよぶ
論理式φ(x) に対して次の形をした論理式を考える
(φ(zero) ∧ ∀x(φ(x) → φ(suc(x))))→∀xφ(x) (6.16)
これが意図しているのは次のような数学的帰納法
φ(0)が成り立ち、「φ(k)が成り立つならばφ(k+1)も成り立つ」が任意のkについていえれば、どんなxについてもφ(x)が成り立つ
論理式φ(x)の取り方は任意なので帰納法の公理は無限個ある
PA
Basicに帰納法の公理をすべて追加した無限集合をPAとよぶ
PAの要素はすべて標準ストラクチャーで真である
これそうなんだ？って感じになるik.icon 標準ストラクチャーって何者なんだって気持ち
したがって健全性定理よってPAは無矛盾である
閉論理式集合Γが次の三条件を満たすならば、Γ⊬ConΓ である
条件
1. PA ⊆ Γ
2. Γは無矛盾である
3. Γのゲーデル数の集合が計算可能である
このようなΓは自分自身の無矛盾性を記述した閉論理式ConΓを導出できない
第一不完全性定理と第二不完全性定理の比較
第一不完全性定理
「標準ストラクチャーで真であるがΓから導出することができない閉論理式」の存在が主張されている
第二不完全性定理
Γの無矛盾性を記述した自然な論理式ConΓを具体例として示している
第二不完全性定理
「数学が無矛盾ならば無矛盾性を示そうと思ってもそれは不可能である」という普遍的な否定解を与えているとも解釈できる
意義は否定的なものだけではない
無矛盾性が理論の強さを分類する指標になる
例 Γ1 ⊊ Γ2となる公理集合で、 Γ1が第二不完全性定理の条件を満たしている
Γ1とΓ2は集合として異なるが、それぞれから導出できる論理式に差があるかどうかは明らかではない
ここで、Γ2⊢ConΓ1が示されれば、Γ2はΓ1より真に強いことが示される
算術のさまざまな理論に対してその無矛盾性を証明するためにどんな公理が必要か？
数理論理学の研究テーマのひとつになっている
例
PAの無矛盾性は「ε0までの超限帰納法」という公理によって証明できることがわかっている
これを示すには緻密な議論が必要
第二不完全性定理をΓ=PAで適用すると次が得られる
PA ⊬ ConPA
完全性定理(の対偶)によって、次のようなストラクチャーMが存在する
PA ⊬ ConPA ならば PA ⊭ ConPA
PA ⊭ ConPAはあるストラクチャーが存在して、PAを真にConPAを偽にする
Mは標準ストラクチャーとは異なるはずである
標準ストラクチャーでConPAは真
PAのモデルであって、標準ストラクチャーとは異なるストラクチャーのことをPAの超準モデルとよぶ 標準ストラクチャーのことをPAの標準モデルともよぶ
同型
ストラクチャーMが次の条件を満たす場合、Mと標準ストラクチャーとは同型であるという
Mの対象領域と自然数全体の間に一対一対応(全単射)がある
Mにおける定数・関数・述語記号の解釈がその対応を通して標準ストラクチャーにおける解釈と一致する
例
次のストラクチャーMは標準ストラクチャーと同型
対象領域
偶数全体の集合
定数項と関数の定義
zero^M = 0
suc^M(x) = x+2
x⨁^M y = x+y
x⨂^M y = xy/2
x⧀^M y ⇔ x < y
この場合Mの対象領域の各要素を「2で割った自然数」に対応させれば上記の条件を満たすので、Mは標準ストラクチャーと同型である
自然数の公理集合(特にPA)の超準モデルの性質は詳しく研究されている
2025/7/23 16:00
Basicの超準モデルの例
自然数とは異なる「モノ」を何でもよいからひとつ持ってきて、ωと名付ける
そして標準ストラクチャーの対象領域にωを付け加えた次のストラクチャーをN'とよぶ
対象領域
N∪{ω}
各記号の解釈
zero^N' = 0
suc^N'(x)
= x+1 if x∈N
= ω elseif x=ω
x⨁^N' y
= x+y if x∈N かつ y∈N
= ω else
x⨂^N' y
= xy if x∈N かつ y∈N
= 0 elseif x=ω かつ y=0のとき
= ω else
x⧀^N' y = 真
⇔ (x∈N かつy∈N かつ x<y) または y=ω
N'はBasicのモデルである(演習問題)
N'は超準モデル
N'と標準モデルの間に同型を示す対応を付けようとしてもωに対応する自然数が存在しない
この超準モデルN'において、たとえば論理式
∀x¬(x = suc(x)) は偽である
反例
ω = suc(ω) が真であるため
したがって健全性定理4.2.2によって
Basic ⊬ ∀x¬(x = suc(x))
であることがわかる
健全性定理の対偶はΓ⊭φ ならば Γ⊬φ
他にも超準モデルを考えることで、いくつかの論理式についてはそれがBasicから導出不可能であることが簡単に示される
N'はPAのモデルではない
PA ⊢ ∀x¬(x = suc(x))
であるため。(PAからこの論理式を導出する際には帰納法の公理が使われる)
言いたいことはわかるけれど、N'はPAのモデルではないって具体的にどう示すんだろう？
定義3.3.2 モデル、充足可能性
閉論理式の集合Γ
有限でも無限でも可能
ストラクチャーM
Γのすべての要素φに対してM(φ)=真となるとき、Mのことを「Γのモデル」あるいは「Γを充足するストラクチャー」という
Γのモデルが存在することを「Γはモデルを持つ」あるいは「Γは充足可能である」という
( φ(zero) ∧ ∀x(φ(x)→φ(suc(x))) ) → ∀xφ(x) ∈ PA
φ(x)をとする
N'ではこれが偽になりそう
¬(zero = suc(zero)) ∧ ∀x( ¬(x = suc(x)) → ¬(suc(x) = suc(suc(x))) ) → ∀x¬(x = suc(x))
¬(zero = suc(zero)) は真
∀x( ¬(x = suc(x)) → ¬(suc(x) = suc(suc(x))) ) は真
xが自然数のときには、明らかに成り立つ
¬(ω = suc(ω)) は偽になるので、∀x¬(x = suc(x))は偽
全体は真
∀x¬(x = suc(x)) は偽
全体は偽
になる
こういうことはいえる？
「Γ ⊢ φ のとき、M(φ)=偽 なら、MはΓのモデルではない。」
証明
健全性定理から、Γ ⊢ φ のとき、Γ ⊨ φ となる
Γ ⊨ φは (すべてのγ∈Γに対してM(γ)=真) ならば M(φ)=真 という意味
この対偶を考えると、M(φ)=偽ならば (すべてのγ∈Γに対してM(γ)=真) ではない
すなわち、M(φ)=偽 ならば MはΓのモデル ではない
よって、 MはΓのモデル ではない
標準ストラクチャーで真な閉論理式集合に対する超準モデル
Nを標準ストラクチャーとして、閉論理式の集合Tを次で定義する
T = {φ | φは表6.2の記号のみで構成される閉論理式で、N(φ) = 真}
Tは自然数上の通常の意味で真である閉論理式の集合である
これは定理6.2.2によって、このゲーデル数の集合は計算不可能である
このTにも超準モデルがある
定理6.7.2 Tの超準モデルが存在する
証明
表6.2 に入っていない定数記号omegaを使って、Tに($ \overline{n}⧀omega) という形の無限個の論理式を加えた集合をT'とする
この集合T'の任意の有限集合はモデルを持つ(演習問題)
したがってコンパクト性定理5.5.1によって、T'もモデル(Mとする)を持つ
するとMは超準モデルである
なぜならこのMと標準モデルの間に同型を示す対応をつけてもomega^Mに対応する自然数が存在しない
MがTの超準モデルであるということは、表6.2の記号のみで構成される任意の閉論理式φに対して
M(φ) = 真 ⇔ 標準ストラクチャーNでφは真
であるにも関わらず、MはNと同型でないということ
つまりMとNは成り立つ論理式の違いだけでは区別ができない
自然数という構造を表6.2の記号のみで構成される論理式によって、特徴づけることは不可能
どうやったら自然数を特徴づけられるのだろうか？気になるik.icon
演習問題
6.1 定理6.6.2の証明中のΓが定理6.5.2の条件1,2,4を満たすことを示せ
Γ = {φ | φは閉論理式でN(φ) = 真} である
Basicの論理式は標準ストラクチャーNで真である
よってΓの定義から、Basic ⊆ Γ となるので条件1を満たす
Γが矛盾していると仮定する
すなわち Γ ⊢ ⊥ であると仮定する
健全性定理から、N(⊥) = 真となる
これは⊥の真理値の定義に反する
よってΓが矛盾していない。条件2を満たす。
条件4(Γ⊢φ または Γ⊢¬φ)を満たすことの証明ってことんな感じか？
φ ∈ Γ ⇔ Γ⊢φ ってなっている気がすることが言えればいいのかな
φ ∈ Γ であるとき、Γ⊢φが成り立つ
¬φ ∈ Γ であるとき、Γ⊢¬φが成り立つ
φ ∈ Γまたは¬φ ∈ Γかが成り立つので、Γ⊢φまたはΓ⊢¬φが成り立つ
「φ ∈ Γまたは¬φ ∈ Γか」これが怪しいな
任意の閉論理式φについてN(φ) = 真であるか、N(φ) = 偽である
N(φ) = 真であるならφ ∈ Γが成り立つ
N(φ) = 偽であるなら¬φ ∈ Γが成り立つ
6.2
ストラクチャーN'がBaiscのモデルであることを示す
モデルの定義
Γのすべての要素φに対してM(φ)=真となるとき、Mのことを「Γのモデル」という
N'(∀x¬(suc(x) = zero)) = 真
⇔ N'の任意の要素の任意の名前aに対して、N'(¬(suc(a) = zero))=真
⇔ N'の任意の要素の任意の名前aに対して、N'(suc(a) = zero)=偽
⇔ N'の任意の要素の任意の名前aに対して、N'(suc(a)) ≠ N'(zero)
aが自然数のとき
(N'(suc(a)) = a+1 ≠ 0) なのでN'(suc(a)) ≠ N'(zero)
aがωのとき
(N'(suc(a)) = ω ≠ 0)なので、、N'(suc(a)) ≠ N'(zero)
証明完了ik.icon
N'(∀x∀y(suc(x) = suc(y) → x = y)) = 真
⇔ N'の任意の要素の任意の名前aに対して、N'(∀y(suc(a) = suc(y) → a = y))=真
⇔ N'の任意の要素の任意の名前a,bに対して、N'(suc(a) = suc(b) → a = b))=真
⇔ N'の任意の要素の任意の名前a,bに対して、(N'((suc(a) = suc(b) ) = 偽 または N'(a = b) = 真)
a,bが自然数の場合
成り立つ
aが自然数、bがωの場合
N'(suc(a) = suc(b) ) = 偽 が常に成り立つ
aがω、bが自然数の場合
N'(suc(a) = suc(b) ) = 偽 が常に成り立つ
aがω、bがωの場合
M(a = b) = 真 が常に成り立つ
証明完了ik.icon
N'(∀x(x⨁zero = x)) = 真
⇔ N'の任意の要素の任意の名前aに対して、N'(a⨁zero = a)=真
aが自然数の場合
成り立つ
aがωである
a⨁zero = ω となるので、N'(a⨁zero = a)=真が成り立つ
証明完了ik.icon
N'(∀x∀y(x⨁suc(y) = suc(x⨁y))) = 真
⇔ N'の任意の要素の任意の名前a,bに対して、N'(a⨁suc(b) = suc(a⨁b))=真
a,bが両方自然数の場合
成り立つ
aが自然数、bがωの場合
a⨁suc(b) = a⨁ω = ω = suc(ω) = suc(a⨁ω) = suc(a⨁b)なので、成り立つ
aがω、bが自然数の場合
a⨁suc(b) = ω⨁suc(b) = ω = suc(ω) = suc(ω⨁b) = suc(a⨁b)なので、成り立つ
aがω、bがωの場合
a⨁suc(b) = ω⨁suc(ω) = ω = suc(ω) = suc(ω⨁ω) = suc(a⨁b)なので、成り立つ
証明完了ik.icon
N'(∀x(x⨂zero = zero)) = 真
⇔ N'の任意の要素の任意の名前aに対して、N'(a⨂zero = zero)=真
aが自然数のとき
成り立つ
aがωのとき
a⨂zero = ω⨂zero = 0 = zeroなので、成り立つ
証明完了ik.icon
N'(∀x∀y(x⨂suc(y) = (x⨂y)⨁x)) = 真
⇔ N'の任意の要素の名前a,bに対して、N'(a⨂suc(b) = (a⨂b)⨁a)=真
a,bが両方自然数の場合
成り立つ
aが自然数、bがωの場合
a⨂suc(b) = a⨂ω = ω = ω⨁a = (a⨂ω)⨁a = (a⨂b)⨁a)なので、成り立つ
aがω、bが自然数の場合
a⨂suc(b) = ω⨂suc(b) = ω = ω⨁ω = (ω⨂b)⨁ω = (a⨂b)⨁a)なので、成り立つ
メモ：suc(b)は1以上の自然数なのでω⨂suc(b) = ωなんですよねik.icon
aがω、bがωの場合
a⨂suc(b) = ω⨂suc(ω) = ω = (a⨂b)⨁a)なので、成り立つ
証明完了ik.icon
N'(∀x¬(x⧀zero)) = 真
⇔ N'の任意の要素の名前aに対して、N'(¬(a⧀zero))=真
aが自然数のとき
成り立つ
aがωのとき
(ω⧀zero)=偽 となるから成り立つ
証明完了ik.icon
N'(∀x∀y(x⧀suc(y) → (x⧀y)∨(x=y))) = 真
⇔ N'の任意の要素の名前a,bに対して、N'(a⧀suc(b) → (a⧀b)∨(a=b))=真
⇔ N'の任意の要素の名前a,bに対して、N'(a⧀suc(b))=偽 または N'((a⧀b)∨(a=b))=真
⇔ N'の任意の要素の名前a,bに対して、N'(a⧀suc(b))=偽 または N'(a⧀b)=真 または N'(a=b)=真
a,bが両方自然数の場合
成り立つ
aが自然数、bがωの場合
(a⧀b) = (a⧀ω) が成り立つ
aがω、bが自然数の場合
a⧀suc(b) = ω⧀suc(b) は成り立たない。よって、M(a⧀suc(b))=偽
メモ：suc(b)が自然数なため。ik.icon
aがω、bがωの場合
a⧀suc(b) = ω⧀suc(ω) = ω⧀ω は成り立つ
証明完了ik.icon
N'(∀x∀y((x⧀y)∨(x=y)∨(y⧀x)))
⇔ N'の任意の要素の名前a,bに対して、N'((a⧀b)∨(a=b)∨(b⧀a))=真
⇔ N'の任意の要素の名前a,bに対して、N'(a⧀b)=真 または N'(a=b)=真 または N'(b⧀a)=真
a,bが両方自然数の場合
成り立つ
aが自然数、bがωの場合
N'(a⧀b) = N'(a⧀ω)=真なので、成り立つ
aがω、bが自然数の場合
N'(b⧀a)= N'(b⧀ω) =真なので、成り立つ
aがω、bがωの場合
N'(ω=ω)=真なので、成り立つ
メモ：N'(a⧀b)=N'(ω⧀ω)=真 となる
演習問題6.3
表6.2 に入っていない定数記号omegaを使って、Tに($ \overline{n}⧀omega) という形の無限個の論理式を加えた集合をT'とする
この集合T'の任意の有限集合はモデルを持つことを証明する
証明1
次のストラクチャーN'を以下のように定義する。これがモデルになることを示す。
ik.iconBasicの超準モデルを持ってきただけです。これでうまくいかないような気がするけどどうなんだろう？
任意の有限部分集合のモデルでもあるんだけど、直接T'のモデルになっている気もする
ストラクチャーN'の定義
対象領域
N∪{ω}
各記号の解釈
zero^N' = 0
omega^N' = ω
suc^N'(x)
= x+1
x⨁^N' y
= x+y
x⨂^N' y
= xy
x⧀^N' y = 真
⇔ (x∈N かつy∈N かつ x<y) または y=ω
T'の任意の有限部分集合をΓとする
Γに($ \overline{n}⧀omega) という形の論理式が含まれていない場合
標準ストラクチャーで真になるので、N'でも真になる
ik.icon本当はN'が「Γを充足するストラクチャー」であるという言い回しの方が正しいかも
Γに($ \overline{n}⧀omega) という形の論理式が含まれる場合
($ \overline{n}) ⧀omega という形の論理式は真になる
($ \overline{n}) ⧀omega という形でない論理式は標準ストラクチャーで真になるのでN'でも真になる
証明完了ik.icon
証明2
ik.iconこっちの方がコンパクト性定理を後で利用する意味が生まれそうな証明になっている気がする。T'のモデルを作らない証明になっていると思うので
T'の任意の有限部分集合をΓとする
Γに($ \overline{n}⧀omega) という形式の論理式が含まれていない場合
これはTの有限部分集合である。
よって、Γは標準ストラクチャーで真となる
したがって、T'の任意の有限部分集合はモデルを持つ
Γに($ \overline{n}⧀omega) という形の論理式が含まれる場合
Γに含まれる($ \overline{n}⧀omega) という形の論理式は有限個である。
Γが有限集合なので
それを数値項が小さい順に以下のように列挙する
($ \overline{n_1}⧀omega), ($ \overline{n_2}⧀omega), … , ($ \overline{n_{last}}⧀omega)
このとき、次のようなストラクチャーN'を考える
標準ストラクチャーに、omega^N' = $ {n_{last}}+1 という解釈を加えたストラクチャー
ΓはN'で真となる
したがって、T'の任意の有限集合はモデルを持つ
証明完了ik.icon
証明前の残骸
アイディアの解説
ik.icon 任意のTの有限集合と($ \overline{n}⧀omega) という形の論理式の有限集合と和集合を取れば、T'の任意の有限集合が作れるじゃん。
($ \overline{n}⧀omega) という形の論理式の有限集合に自然数を割り当てられれば、
任意のTの有限集合に対して、任意の自然数に対応する($ \overline{n}⧀omega) という形の論理式の有限集合を持ってきて、和集合を取って真になることを確かめればいいよね。
任意の有限集合と自然数を対応させるには……要素を2進法の各桁と思えばいいじゃん！という発想だった。
わかりづらいし、その方法で証明になっているか知らないけど
メモ
帰納法で証明する
($ \overline{n}⧀omega) という形の論理式の有限集合と自然数を一対一に割り当てる。
($ \overline{n}⧀omega) という形の論理式の集合は可算無限。その集合の有限部分集合に自然数を割り当てていくわけだが、可算無限集合の有限部分集合全体は可算無限になる(と思う)
kを2進法で表記する。2^nの位が1のとき、集合に($ \overline{n}⧀omega) が含まれ、2^nの位が0のとき、集合に($ \overline{n}⧀omega) が含まれないとする
例：100101
{ $ \overline{0}⧀omega ,$ \overline{2}⧀omega ,$ \overline{5}⧀omega }