ファイル置き場 Sendai Logic Homepage 101105ishida

(1)

Gentzen Consistency Proof For Number Theory

ISHIDA Kazuhiro Tohoku university logic seminar

November,5,2010

(2)

abstract

Gentzen^は”Die Widerspruchsfreiheit der reinen

Zahlentheorie”(Nath.Ann.112(1936))^でPA^{の無矛盾性を発表し} た。その証明では_ǫ₀までの超限帰納法が用いられている。

Gentzenのオリジナルの証明はこの帰納法を使用してなかったの

だが、ブラウワーのファン定理を使っていると指摘され、このような手法に修正した。

PAUL BERNAYSは、そのオリジナルの証明を見て、

◮ 発表されたものより簡単である。

◮ 超限帰納法は必要ない。

と考えた。そして、オリジナルのものに少し修正を加えて_PAの無矛盾性を証明した。今日の発表ではPAUL BERNAYS^の手法を紹介する。以下はPAUL BERNAYS^『ON THE ORIGINAL

GENTZEN CONSISTENCY PROOF FOR NUMBER THEORY^』を参考としている。

(3)

形式体系の構成

まず議論を行う形式体系を構成する。使用するlogical calculus^は Γ →Aという形のシークエントである。ここで、_Γは有限個の論理式の列挙をあらわしており、空でもよい。さらに、_Aと→_Aを同一視する。論理記号は∧_{, ¬, ∀}である。

(4)

✓定義 ✏ 項は次のように帰納的に定義される。

(i)^{変数は項である。}

(ii)t₀,^{· · ·},t_n−₁^を項、f^をn変数関数記号としたとき_f(t₀_,· · ·_,t_n₋₁₎ は項である。

(iii)^{定数は項である。}

✒ ✑

✓定義 ✏

原子論理式は_s=tの形をしている。ここで、_s,tは項である。

✒ ✑

✓定義 ✏

0,S0,SS0,^{· · ·}^をnumeral^という。S0=1,SS0=2,^{· · ·}^{と略記する。}

✒ ✑

(5)

◮ nonlogical symbol^{は後者関数}S,^定数関数Cⁿ_k,^射影関数 Pⁿ_k,Sub(g, ~h),Rec(g,h),^定数0であり、これらは任意の_x,y,z に対して次の条件を満たす。

•₀,_Sx

•_Sx=Sy→_x=y

•_Cⁿ

k⁽^x¹^{, · · · ,}^xⁿ⁾^=k

•_Pⁿ

k⁽^x¹^{, · · · ,}^xⁿ^{) =}^x^k

•_Sub₍_g_,_h₁_{, · · · ,}_h_m₎₍_x₁_{, · · · ,}_x_n_{) =} g(h₁(x₁, · · · ,x_n), · · · ,h_m(x₁, · · · ,x_n))

•_Rec₍_g_,_h₎₍₀_,_x₁_{, · · · ,}_x_n_{) =}_g₍_x₁_{, · · · ,}_x_n₎

•_Rec₍_g_,_h₎₍_Sy_,_x₁_{, · · · ,}_x_n_{) =}

h(y,Rec(g,h)(y,x₁, · · · ,x_n),x₁, · · · ,x_n)

(6)

◮ ^{始式は次の}3つの場合に分けられる。 Case1.

A^∧B ^→A A^∧B^→B A,B^→A^∧B A,^¬A^→1=2

¬¬_A→_A

∀_xF₍_x_{) →}_F₍_t₎

ここで、_tは項、_F₍_x₎は_xを自由変数としてもつ論理式である。

(7)

Case2. s=s s=t^→t=s s=t^∧t=u^→s=u

x₁ =y₁^{∧ · · · ∧}x_n =y_n ^→fx₁^{· · ·}x_n =fy₁^{· · ·}y_n Case3.

各nonlogical symbol^{が満たす７つの論理式}

(8)

◮ 推論規則は次の８個である。

1 Γ,A,B,∆ →C 2 Γ,A,∆ →B Γ,B,A,∆ →C Γ,A,C,∆ →B 3 Γ,A,A,B,∆ →C 4 Γ,^∀xF(x), ∆ →F(t)

Γ,A,B,∆ →C Γ,^∀yF(y), ∆ →F(t) 5 Γ →A A,∆ →B 6 Γ,A,∆ →1=2

Γ, ∆ →B Γ, ∆ → ¬A

7 Γ →F(a) 8 Γ →F(1) F(b), ∆ →F(Sb) Γ → ∀xF(x) Γ, ∆ →F(t)

ここで、_yは_F₍_x₎に出現しない変数であり、_aは_Γの中にあるすべての論理式と_F₍_x₎に出現しない任意の自由変数であり、_bは Γ, ∆の中にあるすべての論理式と_F₍₁₎_,F₍_t₎に出現しない任意の自由変数である。

(9)

無矛盾性証明の流れ

もしこの体系が矛盾していれば→_A,→ ¬_Aを導くことができるので次の証明図が成り立つ。

→_A _A,¬_A→₁₌₂

→ ¬_A ¬_A→₁₌₂

→₁₌₂

なので、この形式体系の無矛盾性を証明するためには→₁₌₂を導けないことを示せばよい。この証明で重要なテクニックは”reduction process”^{というものである。}

(10)

✓定義 ✏ reduction processは次の８個の操作をすることである。

step1 自由変数がシークエントの中にあれば任意に選ばれる

numeral^{に変える。}

step2関数記号があればその値を計算した値に変える。

step3結論の論理式の中にある∀_xF₍_x₎を_F₍_k₎に変える。ここで、_kは任意に選ばれる。

step4結論の論理式の中にある_A∧_Bを_Aもしくは_Bに変える。 step5Γ → ¬A ^をA,Γ →1=2^{に変える。}

✒ ✑

(11)

定義の続き

✓ ✏

step6^{結論が偽のとき、}仮定の論理式の中にある∀_xF₍_x₎を_F₍_k₎ に変える。

step7結論が偽のとき、仮定の論理式の中にある_A∧_Bを_Aもしくは_Bに変える。

step8結論が偽のとき、仮定の論理式の中に¬_Aがあれば、結

論を_Aに変えて仮定の¬_Aを消す。

✒ ✑

ただし、適用の順番は_step1が最優先で、次に_step2が優先される。

✓定義 ✏

シークエントがreduction process^をもつ :⇔ (i)結論が真となる等式になる。

または

(ii)ある仮定の論理式が偽となる等式になる。

✒ ✑

(12)

例

1.Sx=Sy^→x=y

step1

−−−−→_Sm=Sn→_m=n₍_m,nは任意の_numeralである。₎

step2

−−−−→_m^′_=n^′ →_m=n₍_m^′_,n^′は_Sm,Snの計算した値である。₎

•_n=mのとき、このシークエントはreduction process^をもつ。

•_n,_mのとき、仮定は偽となるのでこのシークエントは_reduction process^をもつ。

(13)

2.^∀xF(x) →F(t)

step1

−−−−→ ∀_xF^∗₍_x_{) →}_F^∗₍_k₎

step2,3,4

−−−−−−−→ ∀_xF^∗₍_x_{) →}_m=n

•_m=nが真のとき、このシークエントはreduction process^をもつ。

•_m=nが偽のとき

step6

−−−−→_F^∗₍_k_{) →}_m=n

step2,7,8

−−−−−−−→_m=n→_m=n

よって仮定が偽となるので、このシークエントは_reduction process^をもつ。

•−−−−−−−^step2,3,4→ ∀_xF^∗₍_x_{) → ¬}_Cのとき

step5,2,6,7

−−−−−−−−→ ¬_C_,_C →₁₌₂

step8

−−−−→_C→_C

よって_Cが真でも偽でもこのシークエントはreduction process をもつ。

(14)

例

3.A^∧B ^→A

step1,2,3,4

−−−−−−−−→_A^∗∧_B^∗→_m=n

step7

−−−−→_A^∗→_m=n

step2,6,8

−−−−−−−→_m=n→_m=n

•−−−−−−−^step2,3,4→_A^∗∧_B^∗→ ¬_Cのとき

step5

−−−−→_A^∗∧_B^∗_,_C →₁₌₂

step2,6,7,8

−−−−−−−−→_C→_C

(15)

4.A^∧B ^→B

step1,2,3,4

−−−−−−−−→_A^∗∧_B^∗→_m=n

step7

−−−−→_B^∗→_m=n

step2,6,8

−−−−−−−→_m=n→_m=n

•−−−−−−−^step2,3,4→_A^∗∧_B^∗→ ¬_Cのとき

step5

−−−−→_A^∗∧_B^∗_,_C →₁₌₂

step2,6,7,8

−−−−−−−−→_C→_C

(16)

証明の方針

この体系で導かれる任意のシークエントに対して_reduction

processが存在することを示せれば、この体系の無矛盾性が示せ

たことになる。そのために、始式がreduction process^{をもつのは} 明らかなので、各推論規則に対して仮定がreduction process^を持つならば結論もreduction processをもつことを示す。すると、最後のシークエントもreduction process^{をもつことになり、}

→₁₌₂はこの体系では導けないことになる。

(17)

無矛盾性証明

規則₁∼₄の仮定がreduction process^{をもつならば結論も}

reduction processをもつのは明らかである。ここからは_{Γ, ∆}には

すでに_step1が適用されていて、自由変数はないものとする。_F

∗

で_Fに_step1を適用させて得られる論理式とする。

(18)

✓主張 ✏ 規則₆の仮定_Γ_,A→₁₌₂がreduction process^{をもつとき、結} 論_{Γ → ¬}_Aもreduction process^をもつ。

✒ ✑

Proof

Γ → ¬A^がreduction processをもたないとして矛盾を導く。 step5^よりΓ,A^→1=2となる。仮定よりこれは_reduction process^{を持つので矛盾する。}

✓主張 ✏

規則₇の仮定_{Γ →}_F₍_a₎がreduction process^{をもつとき、結} 論_{Γ → ∀}_xF₍_x₎もreduction process^をもつ。

✒ ✑

Proof

上と同様にして成り立つ。

(19)

✓主張 ✏ 規則₈の仮定_{Γ →} _F₍₁₎ _F₍_b_{), ∆ →} _F₍_Sb₎がreduction process^{をもつとき、結論}Γ, ∆ → F(t)^もreduction process^をもつ。

✒ ✑

Proof

Γ, ∆ →F(t)^{−−−−−→}^step1,2 Γ, ∆ →F^∗(n)(n^は任意のnumeral)^が reduction processをもつことを示したい。

仮定より_{Γ →}_F₍₁₎_F₍_b_{), ∆ →}_F₍_Sb₎はreduction process^をもつ。₍_i_{)Γ →}_F₍₁₎

step1,2

−−−−−→_{Γ →}_F^∗₍₁₎であり、

(ii)F(b), ∆ →F(Sb)^{−−−−−→}^step1,2 F^∗(k), ∆ →F^∗(Sk)^となる。

◮ n=1^のとき

規則₂と₍_i₎より主張は成り立つ。

◮ n=Sm^のとき

規則₅の仮定がreduction process^{をもつとき、結論も} reduction processをもつという性質が成り立っていれば₍_i₎、 (ii)^、規則5^{より主張は成り立つ。}

(20)

✓主張 ✏ Γ →A A,∆ →B^がreduction process^{をもつとき、}Γ, ∆ →B^も reduction process^をもつ。

✒ ✑

Proof

除去する論理式が等式の形か論理記号を含むかで場合分けする。 Case1 A^{が等式のとき}

◮ A^{が真のとき}

仮定より_{∆ →}_Bがreduction process^{をもつ。これと規則}2 より、_{Γ, ∆ →}_Bもreduction process^をもつ。

◮ A^{が偽のとき}

Γ, ∆ →B^にstep3^∼5を適用させると、結論が真となる等式か、偽となる等式か、_B≡ ¬_Cのとき_C_,_{Γ, ∆ →}₁₌₂となるかである。

ここで、仮定と規則₂より_{Γ, ∆ →}_Aや_C_,_{Γ, ∆ →}_Aも reduction processをもつ。なので、偽となる等式、 C,Γ, ∆ →1=2^{となる場合も}reduction process^をもつ。

(21)

Case2 A^{が論理記号を含むとき}Aの複雑さに関する帰納法で示す。_A,_{∆ →}_Bのreduction processを考えるとき、除去する論理式 A^に対してstep^{をつかわなければ}Γ, ∆ →B^のreduction process と同じである。_step6∼₈を適用した場合_Aは∀_xF₍_x₎_,C∧_D,¬_Cのどれかである。

◮ A^{≡ ∀}xF(x)^のとき

A,∆ →B ⁻^step6⁻⁻⁻^→F(k), ∆ →Q (Q:^{偽となる等式})

step2

−−−−→_F₁₍_k_{), ∆ →}_Q 同様にして_F₁₍_k_{), ∆,}_C →₁₌₂を得る。

(22)

◮ F₁(k),∆ →Q^のとき

Γ →A^はreduction process^{をもつので}Γ →F₁^もreduction process^をもつ。A,∆ →B^はreduction process^{をもつので} F₁(k),∆ →Q^もreduction process^をもつ。F₁^{のなかにある} 論理記号は_Aより少なくなっているので、帰納法の仮定より Γ, ∆ →Q^はreduction process^{をもつ。よって}Γ, ∆ →B^も reduction process^をもつ。

◮ F₁(k), ∆,C ^→1=2^がreduction process^{をもつときは明らか} に_{Γ, ∆ →}_Bもreduction process^をもつ。

◮ A^≡B^∧Cのときも同様にして示せる。

(23)

◮ A^{≡ ¬}C^のとき

A,∆ →B ⁻^step8⁻⁻⁻^→∆ →C

同様にして_A,_{∆ → ¬}_Dを得る。

◮ _{∆ →C}のとき

Γ →A^はreduction processをもつのでC,_{Γ →}1=2も reduction processをもつ。よって帰納法の仮定より

∆, Γ →1=2^もreduction process^{をもつ。よって}∆, Γ →Q もreduction process^{をもつ。なので}Γ, ∆ →B^もreduction process^をもつ。

◮ _{A,∆ → ¬D}のとき

A,∆ → ¬D^はreduction process^{をもつので、}A,∆,D ^→1=2^も reduction process^{をもつ。なので、}∆,D ^→C^もreduction processをもつ。帰納法の仮定より_∆,D,_{Γ →1=2}も_reduction process^{をもつ。よって}Γ, ∆ →B^もreduction process^をもつ。

(24)

これで各推論規則に対して、仮定がreduction process^{をもつなら} ば結論もreduction processをもつことが言えたのでこの体系の無矛盾性が証明できた。この体系は_PAの定義による拡張になっている。つまり、_PAで示せることはこの体系で示せる。

(25)

✓参考文献 ✏ PAUL BERNAYS^『ON THE ORIGINAL GENTZEN

CONSISTENCY PROOF FOR NUMBER THEORY^』1970 Wolfram Pohlers^『Proof Theory^』2003

Samuel R.Buss^『An Introduction to Proof Theory^』1998

✒ ✑