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

• 理論の構文的完全性：各文 A について、A またはその否定を証明できる。
• 一階論理の意味論的完全性：すべてのモデルで成り立つ帰結を、証明でも導ける。ここで「すべてのモデルで」は、一つの意図したモデルでの真理とは違う。
• 現実把握の完了：何を観測し、何を説明・予測できれば完了とするのか、別途定義する必要がある。

このページでは、この三つを「完全性」という一語で置き換えない。

典型例は、公理を機械的に列挙でき、十分な算術を含む理論と、その標準的な可証性述語。より抽象的には、命題論理の規則、次のD1〜D3、Löbの証明に必要な対角化を使う。

• D1：T ⊢ A なら T ⊢ □A
• D2：T ⊢ □(A → B) → (□A → □B)
• D3：T ⊢ □A → □□A

□A は「AにTでの証明がある」という内部文。対角化により、ψ ↔ (□ψ → A) という文ψを構成できる。これらの下で、Löbの定理は「T ⊢ □A → A なら T ⊢ A」を与える。Aを矛盾⊥にすると第二不完全性の形になる。

以上は適用条件を固定するための説明であり、すべての論理・知性・有限の装置に自動適用する条件ではない。

Chao–Seraji（2016）は、理論の定義可能性と健全性に条件を置き、第二不完全性定理を一般化している。PAを含む理論TがΣ_n+1定義可能で、Σ_n健全なら、同論文で定める自己のΣ_n健全性の文をTで証明できない。[2]

Σ_n健全とは、その複雑さの範囲に属する偽の文を証明しないこと。「どの程度の意味的な正しさまで、自分で保証できるか」が、具体的な数学の問題になっている。

この結果を使うときも、理論の強さ・定義の複雑さ・健全性・採用した符号化を保持する。

「Tから証明できる文は、Tのすべてのモデルで真である」という論理の健全性は、Tにモデルが一つもない場合にも空虚に成立する。したがって、これだけではTの無矛盾性は保証されない。

上の例ではモデルが存在することもCに含めている。「すべてのモデルでの帰結」「特定のモデルでの真理」「モデルの存在」を分ける必要がある。

ここでは証明論的な形で述べる。必要な対角化ができる無矛盾な理論Tについて、その言語Lの中で定義した述語Trueが、すべてのLの文Aに対する次の同値をTで証明できる、と要求する。

すると「私は真ではない」という文λを作れてしまい、この同値の要求と無矛盾性が両立しない。ここで問題になるのは、同じ言語の全文に適用できる一様な真理述語である。複雑さを限定した真理述語、対象言語とメタ言語を分ける方法、強いメタ理論での意味論は残る。[3]

「意味や真理について何も書けない」と一般化してはいけない。

世界の集合をW、利用可能な証拠をE : W → D、保証対象をP : W → {0,1} とする。

このような二世界があれば、どんな関数J : D → {0,1} も、すべてのwについて J(E(w)) = P(w) を満たせない。入力が同じなら出力も同じなのに、正解は異なるからである。

「保留」を許す判定器なら、間違わずに保留することはできる。だが、全世界で正しい肯定保証を要求する判定器は、この共通の証拠に「完了」とは答えられない。

これは識別不能性の補題であり、第二不完全性定理の証明でも、その無条件の一般化でもない。両者を接続するには、世界・証拠・保証・理論の対応を別途示す。

元記事の no_uniform_self_soundness は、次の主張を扱う。

ここでの∀Aは、外側のLeanでの量化である。対象理論Tの内部で「自分の定理がすべて意図した世界で真」と述べる単一の文とは区別する。

tarski は、Tスキーマと嘘つき文の不動点を別々の引数として受け取る矛盾補題である。tr : F → F という型だけでは、同一言語中の真理述語と構文符号化を実装したことにはならない。定義可能な真理述語から必要な不動点を作る部分は、さらに形式化する対象になる。

ここでの評価は掲載ソースの論理構造の確認に基づく。このページで元コードのLean実行を再検証したという主張はしない。

記事と同じ抽象化の一部を使い、次の小さな二値モデルを作る。算術の文を表現する体系ではない。

このモデルは無矛盾で、命題論理の条件とD1〜D3を満たし、全てのAについて自己反映が成立する。一方、A = ⊥ に対するLöb型の対角化は、ψ ↔ ¬ψ を要求するので成立しない。

無条件の自己保証不能を退ける反例であり、条件付きの第二不完全性定理への反例ではない。ここでは全二値の組合せについて、命題論理の条件・D1〜D3・反映・対角化の成否を確認している。

元記事の ProvSystem 名前空間内に、次の形の補題を追加する構想がある。

theorem no_internal_certificate
    {C : T.F}
    (hc : T.Consistent)
    (bridge : T.Prov (T.imp C T.Con)) :
    ¬ T.Prov C := by
  intro hC
  exact T.godel2 hc (T.mp bridge hC)

追加案。掲載コードと合わせたLeanでの型検査は、このページでは未実施。

この数行の先で必要なのは、保証文Cの定義と、引数 bridge の証明を実際に作ること。Cを単にCon(T)の別名にすれば補題は使えるが、元の意味的な問いへの接続はそれでは進まない。