不完全性定理クイックインストール（素描）

川井 新 (X@squawai)
論計舎 (X@ronkeisha_info) / 在野研究者（数理論理学・理論計算機科学）

エンジニアのゆるっと数学勉強会 LT — 2026-06-25

この発表について（読み上げません）

  • 目的: 不完全性定理の「骨格」を直観として提供
  • 厳密な証明・形式的定義はすべて省略
  • 説明のために擬似コードを提示（動きません）
  • 正確な記述は Gödel (1931) または入門書を参照してください

素描として受け取り、気になった方は続きをご自分で。

第一不完全性定理（ラフに）

どんな「まともな証明システム」にも、
その中では証明も反証もできない文が存在する。

  • 考えるのは 形式体系 — 公理と推論規則で証明を進める仕組み
  • 「まとも」= 健全（公理が自然数で真）かつ公理が計算可能（＝次ページで具体化）
  • ねらい：この「穴」がなぜ必ず空くのかを直観で渡す

形式体系をプログラムとして見る

def is_T_axiom(s: str) -> bool:    # 「s は T の公理か？」を判定（必ず停止する）
    return s in {"S(x) ≠ 0", "x + 0 = x", "x × 0 = 0", ...}  # 例: Robinson算術 Q

def T_theorems():                              # T の定理を全部 enumerate する
    for proof in enumerate_candidate_proofs():  # 証明の候補を短い順（BFS）に並べる
        if proof_checker(is_T_axiom, proof):    # 各行が公理かMP等の規則か検査（必ず停止）
            yield proof.conclusion              # 受理された証明の結論だけ出力
  • 形式体系 T ≒ 公理の判定器（必ず Yes/No を返す）＋proof_checker（推論規則の検査）
  • T の定理 = 機械的に検査を通った証明の結論（定理の集合は r.e.）
  • なぜBFS？ 候補を短い証明の順に並べれば、どの定理にも必ずいつか到達する

相手は「算術」：Q と PA

不完全性が刺さるのは、Q を含む健全な計算可能公理化理論すべて（自然数と +, × を語れれば十分）

  • 算術 = 自然数についての理論（記号 0, S（次の数）, +, × ＋論理）
  • Robinson算術 Q = 帰納法を持たない最小の算術（公理は有限個）。Q を含めば自己言及を表現する力は足り、不完全性が刺さる
  • PA（ペアノ算術） = Q に帰納法を足した標準理論。自然数の性質はほぼここ
  • なぜ算術か：ゲーデル数化は「文」や「証明」を自然数に符号化する。算術なら、その数を理論の内部で計算・検証できる → provable を T 自身が語れる

停止問題：同じ構造の先輩

停止問題 = 「任意のプログラムが停止するか」を判定するアルゴリズムは存在するか？
Turing (1936) が「存在しない」と証明した定理。

def halts(code: str, input) -> bool: ...  # 存在すると仮定

def diagonal():
    me = inspect.getsource(diagonal)   # 自分のコードを取得
    if halts(me, None):
        while True: pass   # 停止するなら止まらない
    # 停止しないなら：if を抜けて関数が正常終了（＝停止する）→ 矛盾
  • inspect.getsource = 「プログラムが自分を参照できる」
  • これと同じ自己言及をゲーデルは算術の言語で作った

ゲーデルの構成

# ① ゲーデル数化：文 → int（encode = 算術版 getsource）
def encode(statement: str) -> int: ...

# ② 証明可能性「述語」Prov_T(n)：算術の論理式（実行する判定器ではない）
#    Prov_T(n) ⇔「結論の encode 値が n の証明が存在する」
def provable(T, n: int) -> bool:           # ↓は Prov_T の意味を説明するだけの擬似コード
    for proof in enumerate_proofs(T):
        if encode(proof.conclusion) == n:
            return True
    # 証明がなければ永遠に返らない → 実行可能な bool ではない

# ③ 自己言及する文：対角線補題が「不動点」の存在を保証
phi = lambda n: not provable(T, n)   # φ(n) = ¬Prov_T(n)（Python の not ではなく算術の論理式 ¬）
G   = diagonal_lemma(phi)            # G ⇔ phi(encode(G)) を満たす不動点（= の代入ではない）
  • 素朴には not provable(T, encode(repr(G))) と書きたい。repr(G) = G 自身のソース表現だが、G の定義に G が要り循環する
  • これを断ち切るのが対角線補題（不動点定理）：
    任意の述語 φ に対し T ⊢ G ⇔ φ(encode(G)) を満たす文 G が必ず存在する（G は φ ごとの不動点）
  • ③のゲーデル文は φ =「¬provable」を選んだ特殊ケース — このとき G ⇔ ¬provable(encode(G))
  • diagonal() が getsource で自分のコードを見たのと同じ —
    対角線補題は算術版の getsource。自己言及を「作れること」自体が定理

場合分け：G は証明も反証もできない

# G の本文:  G ⇔ ¬Prov_T(encode(G))   "T は G を証明しない"

# ── 方向1: T ⊬ G（無矛盾性のみで示せる）──
assume T.proves(G)             # 外側(メタ): G に証明がある と仮定
  # 証明があれば証明番号が存在 → 算術の中で T ⊢ Prov_T(encode(G))
  # だが G ⇔ ¬Prov_T(encode(G)) なので       T ⊢ ¬Prov_T(encode(G)) も
  raise Contradiction("T ⊢ Prov_T(G) かつ T ⊢ ¬Prov_T(G)")
# → 無矛盾なら T ⊬ G

# ── 方向2: T ⊬ ¬G（健全性から）──
# T ⊬ G が示されたので、G の中身「T は G を証明しない」は実際に真
# T が健全（真の文しか証明しない）なら、偽である ¬G を証明できない
# → T ⊬ ¬G
  • 方向1: G に証明があると仮定 → T が矛盾。よって T ⊬ G
  • 方向2: T ⊬ G が判明 → G は真 → 健全な T は T ⊬ ¬G
  • 両方合わせて、G は T において独立（証明も反証もできない）

公理を増やしても逃げられない

「公理を増やせば G のような文も証明できるのでは？」

# T とは p.4 の「公理の判定器を持つ体系」のこと
def is_T2_axiom(s):            # T' = T に G を公理として足したもの
    return is_T_axiom(s) or s == G   # 判定器は依然として必ず停止する

G2 = diagonal_lemma(lambda n: not provable(is_T2_axiom, n))  # T' のゲーデル文 G'
# G は真なので T+G も健全 → T' ⊬ G'（穴は埋まらず再生産される）

計算可能な方法で公理を足し続ける限り、穴は再生産される。

逃げ道は「計算不可能な公理系」（例: True Arithmetic — 真な文すべてを公理にする）。
だが公理かどうかを判定するアルゴリズムが存在するという前提（p.3 の「まとも」）を捨てており、もう土俵の外。

まとめ

形式体系の限界 ≡ 計算可能性の限界

  • 算術の言語は自己言及を構成できる（ゲーデル数化＋対角線補題）
  • 健全な計算可能公理化体系には、証明も反証もできない文が必ず存在する
  • 公理を計算可能に追加しても、独立文は再生産される

台本: 方向1。外側(メタ)で T が G を証明できると仮定する。 証明番号が存在するので、算術の中で T ⊢ Prov_T(encode(G))。 だが G ⇔ ¬Prov_T(encode(G)) なので T ⊢ ¬Prov_T(encode(G)) も成り立ち矛盾。 よって無矛盾なら T ⊬ G。ここまでは無矛盾性だけで出る。 方向2。T ⊬ G が示されたので、G の言っている内容「T は G を証明しない」は実際に真。 T が健全、つまり真の文しか証明しない体系なら、偽である ¬G は証明できない。 よって T ⊬ ¬G。両方合わせて G は T で独立。 内部の Prov_T と外部の T.proves を取り違えないことがポイント。