Gödelの第一不完全性定理｜証明可能性

「証明可能性の階層性」は、数理論理学や計算理論の核心的なテーマであり、Gödelの不完全性定理、Turingの計算可能性理論、証明論などを貫いて現れる階層構造です。以下に体系的に説明します。

🔷 1. 証明可能性の基礎的枠組み

◾ 証明可能性とは

形式体系（たとえばペアノ算術 PA や ZFC）において、ある命題 φ がその体系から論理的に導かれる（=証明できる）ことを言います。

◾ Gödelの第一不完全性定理

• 任意の無矛盾で十分に強い体系（PAなど）には、 その体系では証明できず、かつ偽でもない命題が存在する。
• つまり、体系の内部からは捉えきれない命題がある。

🔷 2. 証明可能性と計算理論（チューリング階層）

◾ チューリング機械と決定可能性

• 命題が「真であるか否か」をTuring machineが有限時間で判定できるとき、それは「決定可能（decidable）」。

◾ Turing Degree（チューリング次数）

• 計算不能な問題には、計算困難さの段階がある。
• 「Halting problem（停止性問題）」は最も基本的な計算不能問題であり、それを解くオラクルがあるとより難しい問題が解ける。
• 各問題は「Turing Degree（チューリング次数）」という帰納的不可解さの階層に分類される。

例：

• 0：計算可能な問題
• 0′：停止性問題（= Turing jump of 0）
• 0″：0′の停止性問題（より上位の階層）

🔷 3. 証明可能性と算術階層（Arithmetical Hierarchy）

これは命題の量化構造によって分類されます：

クラス	形式	内容の例
Σ₀ = Π₀	量化なし	x + y = z など
Σ₁	∃x ϕ(x), ϕはΣ₀	停止性問題など
Π₁	∀x ϕ(x), ϕはΣ₀	全称命題（反証困難）
Σ₂	∃x ∀y ϕ(x,y)	より複雑な停止性問題
…	…	…

• 証明可能性（provability）は、Σ₁レベルの命題で特徴づけられる。
• Gödel文 G は「PAでは証明できないΣ₁文」である。

🔷 4. Gödel Numbering とメタ理論的階層

• Gödelは命題・証明・証明手続きを自然数で符号化（Gödel Numbering）した。
• 「φはPAで証明可能」という主張自体も数式化され、 Prov_PA(⌜φ⌝) という形で表現できる。

このメタレベルの主張は、内部言語での再帰的定義によって、自己言及構造を作り出し、 不完全性定理につながります。

🔷 5. Löbの定理と証明可能性の条件付き構造

Löbの定理：

PA ⊢ Prov(⌜φ⌝) → φ ⟹ PA ⊢ φ

つまり、「φが証明可能ならφが成り立つ」が証明できたら、もうφ自体が証明されてしまう。

これは「証明可能性」のメタ論理的な制約を表します。

🔷 6. 論理体系の拡張と階層性（PA vs ZFC vs ACA₀, etc）

体系の強さに応じて、証明できる命題の範囲が広がります：

論理体系	証明可能性の階層位置	証明できる主張
PA	Σ₁の証明可能性	基本的な数論
ACA₀	Σ₁, Π₁の解析的命題	実数列の存在など
ZFC	高階の集合論命題	カーディナル、選択公理など
ZFC + L	更に高階の階層へ	内的整列可能性など

🔷 7. 証明可能性階層と強さの対応（Reverse Mathematicsとの関連）

Reverse Mathematicsでは、命題から逆に「どの公理が必要か？」を問う。 その過程で、命題が属する階層（WKL₀, ACA₀, ATR₀, Π¹₁-CA₀など）で整理される。

🔷 補足：Turing Jumpと証明可能性のつながり

• Turing Jumpは、**証明不能性の「飛び級」**を形式化する。
• PAが証明できるのは0′以下の問題（Σ₁命題）。
• 0″に属する命題（例：停止性問題の停止性）はPAでは絶対に扱えない。

✴ まとめ：階層的な構図

  Turing Degrees:       0 < 0′ < 0″ < ...
  Arithmetical Hierarchy: Σ₀ < Σ₁ < Σ₂ < ...
  Logical Systems:       Q < PA < ACA₀ < ZFC < ...
  Provability:           decidable < provable < true < unknowable

このように、「何が証明できるか」は、

• 命題の構造（量化）
• 体系の強さ（公理）
• 問題の計算難易度（Turing Degree）

という三層の階層構造に従って分かれています。