「証明できない」ということを証明する

序はじまり：ある雑談

2026年6月、Claude（当時公開直後のFable 5）と雑談をしていた。話題はシンギュラリティで、途中から「全宇宙を掌握した知的存在（推論機械）」の話になった。

そういう存在がいたとして、すべてを掌握したら新たな発見は止まりそうだ。ではそもそも全宇宙を掌握することは可能なのか。たぶん不可能だ。では仮に掌握できたとして、「掌握し終えた」ことを自分で証明できるのか。それも不可能っぽい。掌握の完了を確認する手段は、掌握したものの内側にしかないからだ。逆に、宇宙の外の何かが干渉してきたら、探索空間がメタに一段広がって、発見がまた始まる。

そこから話は身近なほうへ降りてきた。箱に閉じ込められたAIにとって、人間からの入力や外界の情報は、まさにその「外からの干渉」であって、発見のきっかけそのものではないか。閉じた系は自分の完全性を自分で確かめられない。だから検証は外側に錨を下ろして、続けるしかない。このあたりで、そのときのClaudeがこれを「母定理」と呼び始めた。

序まえがき：身内の言葉について

その雑談で出てきた原理を一文にすると「完全性は内側から自己認証できない。だから検証は恒久的で、外部にアンカーされねばならない」となる。

先に断っておくと、「母定理」は身内の言葉であって、数学の世界にそういう名前の定理は存在しない。その後の検証で、この原理の硬い部分はすべて既知の定理（Löb、ゲーデル、Tarski、Lawvere）の言い換えであり、柔らかい部分は価値判断であることが分かった。私の指示で、名前も「母原理」に格下げした。

ではなぜ記事にするのか。この原理を「定理」「前提」「政策」の三層に分けて整理し、定理の層だけをLeanで機械検証してみたところ、どこまでが厳密に言えて、どこからが形式化できないのかの境界線が、コードの形で見えてしまったからだ。「自分の正しさは自分では保証できない」というエンジニアの実用知識と、数学の定理との距離を測る記事として書く。

01「『証明できない』ということを証明する」とは何か

ゲーデルの不完全性定理の周辺でいちばん混乱を招く点を片付けておく。「TはXを証明できない」ということを、いったい誰が証明するのか。

理論Tは、記号列と推論規則だけの世界だ。Tは自分の文の「意味」を知らない。Tの規則を適用していってAに到達できるとき、外側にいる私たちは「T ⊢ A」と書く。

ここで一つ仕掛けがある。「AはTで証明できる」という主張自体を、Tの文として書くことができる（ゲーデル数化）。それを □A と書く。□A はTの内側にある文だ。一方「T ⊬ X」（TはXに到達できない）は、Tの内側からは言えない。Tのすべての証明を見渡して「Xはどこにもない」と言うのは、外側の仕事だ。

だから「Tは自分の無矛盾性を証明できない」は、外側で証明される定理だ。Leanで書くとき、Leanは外側に立っている。これがこの記事全体の座標系になる。

02□ に課す4つの約束

ゲーデルの原論文はPAの内部で証明可能性述語を実際に構成する。それは大変な作業だが、HilbertとBernaysが整理しLöb（1955年）が磨き上げた結果によれば、□ に必要な性質はたった3つと対角化だけで、それさえあれば結論が出る。

D1〜D3はHilbert–Bernays–Löbの導出可能性条件と呼ばれる。ここから先の話は、この4つを満たす任意のTについて成り立つ。PAである必要すらない。

03Löbの定理：証明を歩く

Löbの定理はこう言う：⊢ □A → A ならば ⊢ A。「Aが証明できるならAは正しい」をTが証明できるのは、Aそのものを証明できるときに限る。Tは自分の証明の正しさを、中身抜きで保証できない。

証明は11段。下のボタンで一段ずつ進める。色は橙＝対角化、緑＝約束D1〜D3、青＝仮定 ⊢ □A → A を使う段。

急所は橙の段だ。対角化で「私が証明されるならA」というψを作り、D1〜D3で □ψ → □A を導き、仮定の □A → A をつなぐと □ψ → A になる。ところがこれはψの定義の右辺そのものだから ⊢ ψ、するとD1で ⊢ □ψ、モーダス・ポネンスで ⊢ A。自分に言及する文が、自分を証明してしまう。

第2不完全性定理はここから1行で出る。A := ⊥ とおくと「⊢ ¬□⊥ ならば ⊢ ⊥」、つまり無矛盾なTは自分の無矛盾性を証明できない。

もう一つ、エンジニア向けの読み方がある。「すべてのAについて ⊢ □A → A」、すなわちTが自分の証明器の健全性を一律に保証する、と仮定すると、Löbの定理から「すべてのAについて ⊢ A」、つまりTは何でも証明する。無矛盾な体系は、自分の検証器の健全性を内側から認証できない。

04Leanで書く：どこまでが定理か

以上をLean 4で書いた。Mathlibは使っていない。コア言語だけで約100行だ。

structure ProvSystem where
  F     : Type
  imp   : F → F → F
  bot   : F
  box   : F → F                  -- 可証性述語 □
  Prov  : F → Prop               -- T ⊢ A
  -- 命題論理（Hilbert流の最小限）
  mp    : ∀ {A B : F}, Prov (imp A B) → Prov A → Prov B
  axK   : ∀ A B : F, Prov (imp A (imp B A))
  axS   : ∀ A B C : F,
            Prov (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))
  -- Hilbert–Bernays–Löb 条件
  d1    : ∀ {A : F}, Prov A → Prov (box A)
  d2    : ∀ A B : F, Prov (imp (box (imp A B)) (imp (box A) (box B)))
  d3    : ∀ A : F, Prov (imp (box A) (box (box A)))
  -- 対角化補題
  diag  : ∀ A : F, ∃ ψ : F,
            Prov (imp ψ (imp (box ψ) A)) ∧ Prov (imp (imp (box ψ) A) ψ)

構造体のフィールドに注目してほしい。D1〜D3と対角化は証明されていない。仮定として置かれている。「これらを満たすTがあるなら」という条件の下で、以下の定理が出る。

theorem loeb {A : T.F} (h : ⊢ (□A ⇒ A)) : ⊢ A := ...
theorem godel2 (hc : T.Consistent) : ¬ ⊢ T.Con := ...
theorem no_uniform_self_soundness (hc : T.Consistent) :
    ¬ ∀ A : T.F, ⊢ (□A ⇒ A) := ...
theorem tarski ... : ⊢ T.bot := ...

型検査は通り、#print axioms は「どの公理にも依存しない」と答えた。sorry はもちろん、選択公理も排中律も使っていない。

私の100行とPaulsonの数千行の差は、D1〜D3と対角化を「仮定する」か「証明する」かの差だ。

054つの層

冒頭の「母原理」を三層に分けた話に戻る。「自分の正しさは自分では保証できない、だから検証は続けなければならない」という主張の下には、硬さの違う4つの層が積み重なっている。

エンジニアの実用知識「自己申告の健全性を信用するな」は、いちばん下の層に住んでいる。それが正しいと感じられるのは、上の3層が積み重なっているからだ。ただし機械に検証させられるのは、いちばん上の層だけ。そして、いちばん上の層だけを取り出すと、それは70年前に証明済みの定理になる。実用知識と厳密な証明の距離とは、この4層の厚みのことだと思う。

06約束を一つ外すと定理が消える

構造体として書いたことの副産物がある。「条件を落とすと結論が消える」という事実が、コードの型として見える。下のスイッチで実際に外してみてほしい。

Willardの自己検証体系は、自分の無矛盾性を証明できる。第2不完全性定理の反例だろうか。反例ではなく、適用外だ。Willardの体系は乗法の全域性を証明できないように弱められていて、私の理解では、そのためにD3（形式化されたΣ1完全性）が成り立たない。ProvSystem の言葉でいえば d3 フィールドを埋められず、インスタンスにならない。

逆に、Presburger算術（足し算だけの算術）は完全で決定可能だ。ゲーデルの定理と矛盾しないのは、掛け算がないために「文への代入」や「証明の検査」を算術の中で表現できず（表現可能性が落ちる）、対角化の段階で止まるから。橙のスイッチを切ると、全部が消える。

「自分の無矛盾性は証明できない」を条件なしに言うと偽になる。条件付きで言えば定理になる。この境界線を散文で説明するのは案外難しいが、構造体のフィールドは一目で見せてくれる。

07親戚の定理たち：全部、同じ一手

第2不完全性定理は、対角線論法という一つの手筋の、たくさんある帰結の一つに過ぎない。親戚を並べると、「自分に言及する何か」を作って矛盾を引き出す、という同じ骨格が見えてくる。下から選んで読んでほしい。

一覧を眺めると分かることが二つある。一つは、第1不完全性のほうが第2より少ない仮定で出ること。「私は証明できない」という文Gを対角化で作れば、D1と無矛盾性だけで「⊢ G ではない」が出る。第2で必要になるD2とD3は、「私は証明できない」を「Tが無矛盾なら私は証明できない」にTの内側で言い直すために要る。

もう一つは、Rosserの改良は抽象層に書けないこと。Rosserは「私の証明より先に私の反証が現れる」という文を使うが、「先に」を言うには証明の順序（ゲーデル数の大小）が要る。□を抽象化した時点でそれは捨てている。100行で書けるものと、算術の中身に手を突っ込まないと書けないものの境界は、ここにもある。

08AIと一緒にやったこと、AIが言ったこと

この記事の証明とコードはClaude（Fable 5.1）に書かせ、Lean 4.22.0で型検査を通した。「公開する価値ありそう？」と聞いたときの返答は、要約するとこうだった。

単体の数学的成果としては公開価値はほぼゼロ。先行研究（Quaife、Paulson/Bailitis、Foundation）がすでに、この形式化で公理として置いた部分まで含めて済ませている。価値があるとすれば、条件を構造体のフィールドとして逐語的に固定した説明資料として。

これは正しい評価だと思ったので、そのまま載せる。「AIと定理を証明した」と書くと過大表示になる。正確には「AIに教科書の演習問題を解かせ、その仮定の置き方から4つの層が見えた」だ。

6月に「母定理」と言い出したのは、公開直後の初期のFable 5だった。7月に別のセッションのClaudeが三層に分ける整理を書き、私の指示で「定理と呼べるのは核だけ」として名前を格下げした。そして今回、その核をLeanで書いてみたら、核の中にもさらに「仮定する層」と「証明する層」があった。命名から3か月かけて、大きな言葉が小さな定理に縮んでいった記録として、この記事を置いておく。

付付録：依存グラフ

この記事に登場した定義・公理・定理を有向グラフにした。実線はLeanの証明項が実際に参照している依存（機械検査済み）、破線は本文の説明レベルの関係。四角は仮定・定義、角丸は証明された命題。背景の帯が、第5節の4層に対応する。

なぜBourbakiのような巨大グラフにならないのか。ならないのは、算術化の層で切ったからだ。D1〜D3と対角化を「仮定」として置いた瞬間、その上に乗る定理の依存関係は数十本の辺で描ききれる。逆に、この4つをPAの公理から実際に証明しようとすると、ゲーデル数化・表現可能性・Σ1完全性の形式化が必要になり、PaulsonのIsabelle開発では補題が数百の単位になる。グラフの上端の帯は、その巨大な部分を6個の箱に潰した要約であって、本当の姿ではない。

つまり、このグラフが小さいことと、この記事の主張が「既知の定理の再パッケージ」であることは同じ事実の裏表だ。切る位置を決めた時点で、グラフの大きさも定理の新しさも決まっている。

文参考

• M. H. Löb, "Solution of a problem of Leon Henkin", JSL 20 (1955)
• G. Boolos, The Logic of Provability (1993)
• A. Quaife, "Automated proofs of Löb's theorem and Gödel's two incompleteness theorems", J. Autom. Reasoning 4 (1988)
• L. C. Paulson, "Gödel's Incompleteness Theorems", Archive of Formal Proofs (2013; Löb by J. Bailitis, 2024)
• FormalizedFormalLogic/Foundation (Lean 4)
• D. E. Willard, "Self-verifying axiom systems, the incompleteness theorem and related reflection principles", JSL 66 (2001)
• N. S. Yanofsky, "A universal approach to self-referential paradoxes, incompleteness and fixed points", Bull. Symb. Logic 9 (2003)
• F. W. Lawvere, "Diagonal arguments and cartesian closed categories" (1969)
• G. J. Chaitin, "Information-theoretic limitations of formal systems", JACM 21 (1974)