logicArth - 41semicolon/41semicolon.github.io GitHub Wiki

1. 算術の世界

1階述語論理の証明系を背景とした 構文的・形式的な世界を算術の世界と呼ぶ。

言語と理論: 算術の言語は {0,1,+,×,≦}。加法・乗法・順序に関する16の公理からなる理論 ロビンソン算術Q、それに数学的帰納法相当の公理(IS)を追加した IOpen,IΣ1,PA等を考える。違いは(IS)の適用範囲。以下Tとして Q⊆T とする。

算術的階層: 算術の論理式を量化子の現れ方で分類した階層。Δ0=Σ0=Π0 は量化子が現れない式(限定量化子はあってもよい)。それに∀が任意個数くっつけば Π1、∃が任意個くっつけば Σ1。同様に Π1 に∃を任意個くっつければ Σ2 になるし、Σ1に∀を任意個くっつければ Π2になる。以下同様に Σn, Πn を定義。さらに Σn と同値な式もまとめて Σnと呼ぶ(Πnに関しても同様)。Σn かつ Πn なのを Δn という。

2. 計算の世界

ペアノらによって提示された数学的構造 ℕ上での演算に関する世界が計算の世界。

計算可能性: 再帰関数・型無しラムダ計算・チューリング機械などは同じ強さの計算能力を持ち、この計算能力を計算可能性と呼ぶ（チャーチ・チューリングの提唱）。

再帰関数: 再帰関数＝原始再帰関数＋最小化。原始再帰関数は「射影関数・定数関数・後者関数」という基本部品に「合成・再帰法」という構造化の規則を持つプログラミング言語と捉えられる。add, mult, ge, ifelse 等を表現でき、これは{+,×,≦}の意図した解釈が原始再帰的に構成できることを示す。一方 最小化は whileを実現するために必要な規則と捉えられる。最小化の導入により全域性が失われるが、その代償として計算可能性に到達できる。

3. 算術と計算が出会う舞台

出会う舞台: 計算の世界には「数∈ℕ」があり、算術の世界には「数項∈Num」がある。（集合論を背景として）関数・関係を捉える時、計算の世界ではA ⊆ N^nを 算術ではA' ⊆ Num^nを使う。N^n と Num^n は異なる種類の存在物であるが、意図した解釈を背景として 同一視する。つまり {2,3} と {1+1, 1+1+1} を同一視する。また 例えば{(1,1),(2,4)}と{(1,1),(1+1,1+1+1+1)}を同一視する。この舞台（すなわち N^nとNum^nを同一視した世界）において 計算論の諸概念と算術の諸概念とは 同じ種類の存在物するのでそれらの関係性を議論できる。

計算可能集合と枚挙可能集合: ある集合 A⊂ℕ^n に対して、その特性関数が再帰的関数である場合に計算可能集合と呼ぶ。一方、その外延を定めるのが（全域的な）再帰的関数の値である場合 枚挙可能な集合と呼ぶ。「計算可能⇒枚挙可能」は成立するけれど「枚挙可能⇒計算可能」は成立しないこともある。この二つの集合には多くの別名が存在し、(後述する）性質を反映する:

  • 計算可能集合 = 帰納的集合 = 再帰的集合 = 決定可能な集合
  • 枚挙可能集合 = r.e.な集合 = 帰納的可算な集合 = 半決定可能な集合 = 証明可能集合

定義可能性: A = {a | N ⊨ φ(a)} で集合が定まる時、集合は定義可能という。以下が成立:

  • 「集合Aが計算可能」⇔「集合Aに対応する 関数/関係 が Π1式で定義可能」
  • 「集合Aが枚挙可能」⇔「集合Aに対応する 関数/関係 が Σ1式で定義可能」

表現可能性: A = {a | T ⊢ φ(a)} で集合が定まる時、集合はAは弱表現可能であるといい、さらに 補集合がその否定を導出する時には表現可能という。以下が成立:

  • 「集合Aが計算可能」⇔「A は Σ1式で表現可能」⇔「Aは表現可能」
  • 「集合Aが枚挙可能」⇔「A は Σ1式で弱表現可能」⇔「A は弱表現可能」
    • 枚挙可能集合の別名「半決定可能な集合」はこの事実に起因しそう
    • 枚挙可能集合の別名「証明可能集合」はこの事実(と算術のΣ1完全性)に起因しそう

4. 完全性に関する諸性質

算術化の前に、押さえておきたい概念・事実を整理する。

完全性と健全性: 算術的階層を使って粒度の細かい完全性と健全性を定義。いくつかの定理:「Πn健全 ⇒ Σn+1 完全」「Πn 完全⇒ Σn+1 健全」「Σ1 健全⇒無矛盾 (つまり Σn 健全性は無矛盾性を強めた主張)」以下の性質が特に重要:

  • T は Σ1完全。つまり Σ1 文に対し N ⊨ φ ⇒ T ⊢ φ
  • T が無矛盾なら Π1 健全。つまり Π1文に対し T ⊢ φ ⇒ N ⊨ φ
  • 任意の Δ0文に関しては T ⊢ φ または T ⊢ ¬φ が成立 (部分的な完全性)

PAはℕをモデルに持つか？: PAという理論はℕをモデルに持つことを意図して作られてはいるが、ℕをモデルに持つ（≒無矛盾である）と言い切りづらい。PAの完全性・無矛盾性・ℕに相当する存在物の一意存在性はZFCにおいては示すことができるが、それが直ちにZFCとは別言語・別理論であるPAにおいて言えるとは言い難い。このあたりの歯切れの悪さが完全性の定義等に反映されている。例えば Σ1完全の定義は「Σ1文に対し N ⊨ φ ⇒ PA ⊢ φ」であって「Σ1文に対し PA ⊨ φ ⇒ PA ⊢ φ」でない。

「+」は「add」なのか？:

5. 算術化

初等関数記号の導入: 関数記号の解釈である 関数は全域的である。一方 意図した解釈の世界ℕには部分関数が存在する。よって関数をグラフと同一視すると「集合 A⊆ℕ^n に名前を付ける（関数記号を導入する）ことができるか？」という概念、つまり「可証再帰性」に到達する。原始再帰的な関数はすべて可証再帰的であるので、べきの関数記号Powや素数判定述語記号Primeなどを言語に導入できる。

ゲーデル数化: 算術化の対象としたいのは 論理式（＝記号列）であり、証明（＝論理式列）である。これらを一意に「数」に符号化（及び復号）する原始再帰的な関数が存在する。この符号化方式をゲーデル数化という。上述の舞台では「数」と「数項」を同一視するので、任意の論理式や証明は数項へと形式化できる。

公理化: 理論Tによって定められる集合 S = { ⌜φ⌝ | φ ∈ T } に対する性質（原始再帰的・計算可能・枚挙可能）に応じて、理論の公理化可能性という概念を導入する。例えば S が枚挙可能な集合の場合、理論Tは「枚挙可能に公理化可能な理論」と呼んだり、単純に「枚挙可能な理論」と呼んだりする。不完全性定理の文脈で重要な事実は以下で、次節ですぐ使う:「PAは計算可能な算術の理論である」。

証明の算術化と可証性述語の本質: (PAに代表されるように) 理論Tが計算可能ならば、「Tでの証明のゲーデル数全体からなる集合 = Prf = { (⌜φ⌝ ,⌜Φ⌝ ) | Φはφの証明}」が計算可能集合になる。よって Prf はΔ1式で定義できるので、対応する 2つの自由変数を含むΣ1式に Pf(x,y) という名前を付ける。そして ∃yPf(x,y) に Pr(x) という名前を付ける。一方「Tの定理のゲーデル数全体からなる集合 = Prv = { ⌜φ⌝ | T ⊢ φ}」は枚挙可能集合となり「n ∈ Prv」⇔「ℕ ⊨ Pr(n)」なる関係が成立するが、これは証明の算術化の一つの到達点といえる。さて、Prにおける超重要な3つの性質がある。これらは第一不完全性定理において使われ、逆にこの3つの性質しか使わない（Prの定義の仕方は本質ではない）:

  • 「T ⊢ φ」⇔「ℕ ⊨ Pr(⌜φ⌝)」
  • 「T ⊢ φ」⇒「T ⊢ Pr(⌜φ⌝)」
  • TがΣ1健全である時、「T ⊢ Pr(⌜φ⌝)」⇒ 「T ⊢ φ」

対角化定理: Φ(x)をxのみ自由変数とする任意の論理式とすると、T ⊢ δ↔Φ(⌜δ⌝) となる 文δが存在するという言明。「文φを入力して文Φ(⌜φ⌝)を出力する」という関数 f の不動点になっている