「証明できない」ということを証明する — Löbの定理をLeanで100行

ちょっとした数学の読み物をスタンドアロンで公開した。

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

きっかけ

6月にClaudeと雑談していて、「全宇宙を掌握した推論機械は、掌握し終えたことを自分で証明できるのか」という話になった。たぶん無理。閉じた系は自分の完全性を自分では確かめられないので、検証は外側に錨を下ろして続けるしかない。

当時のClaudeはこれを「母定理」と呼び始めたんだけど、後で検証してみたら硬い部分は全部既知の定理（Löb・ゲーデル・Tarski・Lawvere）の言い換えで、柔らかい部分は価値判断だった。なので「母原理」に格下げ。

じゃあ定理の層だけLeanで書いてみるか、というのがこの読み物。

中身

• □（可証性述語）に課す4つの約束、D1〜D3と対角化を構造体のフィールドとして置いて、その上でLöb・第2不完全性・「検証器の健全性は自己認証できない」・Tarskiを証明。Lean 4.22.0、Mathlibなし、約100行、#print axioms は公理依存なし
• Löbの証明を11段、ボタンで一段ずつ歩ける
• 約束をON/OFFするスイッチ。D3を外すとWillardの自己検証体系、対角化を外すとPresburger算術になって、どの定理が消えるかが見える
• 対角線論法の家系図と、親戚の定理12件の一覧
• 定義・公理から定理への依存グラフ

正直なところ

この100行は数学的には何も新しくない。抽象可証性論理でのLöbの証明は教科書の演習問題で、Quaife（1988）、Paulson/Bailitis（Isabelle）、Foundation（Lean 4）といった先行の機械検証がすでにある。自分の100行と先人の数千行の差は、D1〜D3と対角化を「仮定する」か「証明する」かの差でしかない。

ただ面白かったのはそこで、「自分の正しさは自分では保証できない」というエンジニアの実用知識と、70年前に証明済みの定理との間に、硬さの違う4つの層があるのがコードの形で見えた。機械に検証させられるのはいちばん上の層だけ。6月の大きな言葉が3か月かけて小さな定理に縮んでいった記録ということで、置いておく。