「母原理」を別のAIに監査してもらった — 第二不完全性定理から意味論へ

一昨日のLöbの記事の続き。

→ 「正しさ」は、どこまで自分で保証できるか

経緯

「母定理」を「母原理」に格下げしたところまでは前回書いた。今回は、その原理のページをGPT-6 astraに見せて、どこまでが本当に定理で、どこからが言い過ぎなのかを洗ってもらった。出てきたものが面白かったので、スタンドアロンのページとして残しておく。

要点

• 「正しい」を三つに分ける。証明が通る（T ⊢ A）、指定した解釈で真（M ⊨ A）、モデルが現実に合う。前回の記事はこの三つをわりと一語で言っていた
• 厳密に成立する部分は小さい。第二不完全性の適用条件の下で、保証Cから無矛盾性への橋 T ⊢ C → Con(T) が内部で証明されているなら T ⊬ C。既知の定理の直接の系で、それ以上ではない
• 「閉じた体系だから自己保証できない」は出ない。命題論理の条件とD1〜D3を満たしつつ全反映が成り立つ二値モデルが反例になる。効いているのは対角化のほう
• 「理解し終えた」が証拠から分かるかは、同じ証拠で保証対象の真偽が異なる二世界を作れば否定できる。ただし現実にそういう二世界が残るかは経験仮定で、定理からは出ない
• 「検証を続けるべき」は不可能性定理だけからは導けない。効果・費用・誤りの共有という別の前提が要る

前回の記事の表現を直す点も四つ挙がっていて、自分の掲載Leanコードの射程（no_uniform_self_soundness の ∀A は外側のLeanの量化であって、対象理論内部の単一の文ではない）も指摘された。次に書くなら保証文Cを受け取る補題 no_internal_certificate だという構想まで付いてきたが、型検査はまだしていない。

正直なところ

6月に大きく言った話が、Claudeとの検証で定理の層に縮み、今回さらに「確定した補題」「反証された橋」「未証明命題」の三段に仕分けられた。残った研究の場所は、自然言語の「保証」を意味を保ったまま内部文Cに移して橋を作るところ、という結論になっている。ページ自体は新定理を主張していないし、自分もそう思う。