Zenn
🔲

Gödelの第一不完全性定理の形式的証明をする

2023/12/04に公開
math
logic
lean
tech

はじめに

これは定理証明支援系 Advent Calendar 2023の記事です。参加してくださった皆さんありがとうございます。

https://adventar.org/calendars/9022

証明支援言語であるLean4を用いてlean4-logicというプロジェクトでGödelの第一不完全性定理の証明を行ったので、その解説を書きます。数理論理学や不完全性定理の詳しい解説はしないので、適切な教科書を参考にしてください。ある程度Lean4の構文を知っているとわかりやすいかもしれません。

背景

他の重要な定理と比べて第一不完全性定理のコンピュータ等による形式的証明の歴史はかなり古く、おそらく最古のものはNqthmを使用した第一不完全性の証明で、1986年にはすでに形式化されています[1]。また2005年にはCoqによる形式化[2]、2009年にHOL Lightによる形式化が行われています。第二不完全性定理の証明の形式化は最近になって2013年にIsabelleによって（おそらく初めて？）形式化されました[3]。

Leanによる一階論理やその完全性定理、連続体仮説の独立性の証明の形式化はすでになされていますが[4]、Missing theorems from Freek Wiedijk's list of 100 theoremsの記述によると2023年時点では不完全性定理はまだ証明されていないようなので、おそらく最初の例でしょう。

不完全性定理には様々な表現方法がありますが、現代的な形では以下のように表現されることが多いようです[5]。

第一不完全性定理：\mathbf{PA}を含む計算可能で\omega-無矛盾な理論Tにおいて、Tから証明も反証もできない文が存在する。

第二不完全性定理：\mathbf{PA}を含む計算可能で無矛盾な理論Tにおいて、その無矛盾性を示す文は証明も反証もできない。

lean4-logicでは上に述べたものより強い以下の定理を証明します。

第一不完全性定理'：\mathbf{PA}^-を含む計算可能で\Sigma_1-健全な理論Tにおいて、Tから証明も反証もできない文が存在する。

基礎

まず論理式や証明や意味論と言った基礎的な道具を揃える必要があります。Lean4の標準的なライブラリであるmathlib4でも論理式や意味論などの概念は定義されていますが[6]、後述するようにTait計算を証明の基礎に用いたかったため、独自に定義します。

項・論理式

一階論理の論理式を定義する方法は色々ありますが、De Bruijn indexによる方法がhydra-battles(Coq)やflypitch(Lean)などでは採用されています。lean4-logicでもこの方法で形式化しています[7]。

言語FirstOrder.Languageはアリティkの関数記号L.func kと関係記号L.rel kの組です。

structure Language where
  func : Nat → Type u
  rel  : Nat → Type u

型μの変数を持つ言語Lの項Term L μは以下のように定義されます[8]。

inductive Subterm (L : Language) (μ : Type v) (n : ℕ)
  | bvar : Fin n → Subterm L μ n
  | fvar : μ → Subterm L μ n
  | func {arity: ℕ} :
    L.func arity → (Fin arity → Subterm L μ n) → Subterm L μ n

abbrev Term (L : Language) (μ : Type v) := Subterm L μ 0

ここでSubterm.bvar x : Subterm L μ nはx : Fin n番目の束縛変数、Subterm.fvar x : Subterm L μ nはx : μの自由変数を意味します（すなわち、Subterm L μ nは型μの自由変数と最大n個の束縛変数を持つ項を意味します）。Subterm.bvar xは#x, Subterm.fvar xは&xと略記されます。

同様に論理式Formula L μは以下のように定義されます。[9]

inductive Subformula (L : Language.{u}) (μ : Type v) :
    ℕ → Type (max u v) where
  | verum  {n} : Subformula L μ n
  | falsum {n} : Subformula L μ n
  | rel  {n} {arity : ℕ} :
    L.rel arity → (Fin arity → Subterm L μ n) → Subformula L μ n
  | nrel {n} {arity : ℕ} :
    L.rel arity → (Fin arity → Subterm L μ n) → Subformula L μ n
  | and    {n} : Subformula L μ n → Subformula L μ n → Subformula L μ n
  | or     {n} : Subformula L μ n → Subformula L μ n → Subformula L μ n
  | all    {n} : Subformula L μ (n + 1) → Subformula L μ n
  | ex     {n} : Subformula L μ (n + 1) → Subformula L μ n

abbrev Formula (L : Language) (μ : Type v) := Subformula L μ 0

一般的な論理学の用語では、これはLに\muの定数を追加した論理式L[\mu]であるとも解釈できます。論理式は以下のようなあまり一般的ではない方法で構成されることに注意してください：

  • アリティkの関係記号r \in L、k個の項t_0,t_1,...,t_{k-1}についてr(t_0,t_1,...,t_{k-1}), r^{-}(t_0,t_1,...,t_{k-1})は論理式である
  • \top, \botは論理式である。
  • \varphi, \psiが論理式であるとき、\varphi \land \psi, \varphi \lor \psi, \forall x. \varphi, \exists x. \varphiは論理式である

論理式の否定を示す論理式\lnot \varphiは以下のように再帰的に定義されます。

  • \lnot r(t_0,t_1,...,t_{k-1}) \coloneqq r^{-}(t_0,t_1,...,t_{k-1})
  • \lnot r^{-}(t_0,t_1,...,t_{k-1}) \coloneqq r(t_0,t_1,...,t_{k-1})
  • \lnot \top \coloneqq \bot
  • \lnot \bot \coloneqq \top
  • \lnot (\varphi \land \psi) \coloneqq (\lnot\varphi) \lor (\lnot\psi)
  • \lnot (\varphi \lor \psi) \coloneqq (\lnot\varphi) \land (\lnot\psi)
  • \lnot (\forall x. \varphi) \coloneqq \exists x. (\lnot \varphi)
  • \lnot (\exists x. \varphi) \coloneqq \forall x. (\lnot \varphi)

古典論理において論理式は\toと\botの記号ですべて表現できるのでこの定義は冗長に見えますが、これはTait計算の論理式を定義するためです。

分かりやすさのため論理式の記法を定義します（→や∧などはLean4の予約語で使えないため似た文字を用いています）。

通常の記法 lean4-logicにおける記法
真 \top ⊤
偽 \top ⊥
論理積 p \land q p ⋏ q
論理和 p \lor q p ⋎ q
否定 \lnot p ~p
含意 p \to q p ⟶ q
同値 p \leftrightarrow q p ⟷ q
全称量化子 \forall ∀'
存在量化子 \exists ∃'

またLean4の強力なメタプログラミング能力を用いて、“ ... ”の記法で自然に論理式が書けるようにしました。例えば<の推移律を表す文を“∀ ∀ ∀ (#2 < #1 → #1 < #0 → #2 < #0)”のように書くことが可能です。

Tait計算

Tait計算はGentzenの推件計算に似た証明体系で、以下の推論規則からなります。\Delta, \Gamma, ...は論理式の有限集合を表すとし、\varphi, \Gammaは\{\varphi\} \cup \Gammaの省略記法だとします。Tait計算の導出関係\vdash_\mathsf{T} \Deltaは次のように定義されます。

  1. (AxL)：アリティkの関係記号r、k個の項t_0,t_1,...,t_{k-1}について\vdash_\mathsf{T} r(t_0,t_1,...,t_{k-1}), r^{-}(t_0,t_1,...,t_{k-1}), \Delta
  2. (\top)：\vdash_\mathsf{T} \top, \Delta
  3. (\land)：\vdash_\mathsf{T} \varphi, \Deltaかつ\vdash_\mathsf{T} \psi, \Deltaならば\vdash_\mathsf{T} \varphi \land \psi, \Delta
  4. (\lor)：\vdash_\mathsf{T} \varphi, \psi, \Deltaならば\vdash_\mathsf{T} \varphi \lor \psi, \Delta
  5. (\forall)：\vdash_\mathsf{T} \varphi(x), \Deltaならば\vdash_\mathsf{T} \forall x. \varphi(x), \Delta. ただし変数記号xは\Deltaに登場しないとする
  6. (\exists)：\vdash_\mathsf{T} \varphi(t), \Deltaならば\vdash_\mathsf{T} \exists x. \varphi(x), \Delta
  7. (Cut)：\vdash_\mathsf{T} \varphi, \Deltaかつ\vdash_\mathsf{T} \lnot\varphi, \Deltaのとき\vdash_\mathsf{T} \Delta

Tait計算が優れているのは推論規則が少ないことです。Gentzenの推件計算では\vdashの両側に推件があるので右と左にそれぞれ論理記号の導入規則が必要ですが、Tait計算は一つで済みます。また(Cut)はカット除去定理によって除くことができ、その証明もlean4-logicで形式化されています。

証明体系の形式化においては『ただし変数記号xは\Deltaに登場しないとする』という部分が問題になります。\forall x.の導入規則を適応する際に一々x \notin \mathrm{FV}(\Delta)のメタ証明を書くのは非常に面倒です。なので以下のように対処します。自由変数は可算無限個存在するとします（v_0, v_1, ...）。

  • \varphi^+を、\varphiに登場する自由変数v_0, v_1, ...をインクリメントした論理式とする（例えば(v_0 < v_1 + v_2)^+ = (v_1 < v_2 + v_3)）。また\Delta^+ \coloneqq \{\varphi^+ | \varphi \in \Delta\}とする。
  • \mathsf{fr}\varphiを、束縛変数xを自由変数v_0に変換し、自由変数v_0, v_1, ...をインクリメントした論理式とする（例えば\mathsf{fr}(x \cdot v_0 < v_1) = (v_0 \cdot v_1 < v_2)）
  • 以下の推論規則を(\forall)の代わりに導入する：
    • \vdash_\mathsf{T} \mathsf{fr}\varphi, \Delta^+ならば\vdash_\mathsf{T} \forall x. \varphi, \Delta

\mathsf{fr}\varphiに登場する自由変数v_0は\varphiの束縛変数x以外の場所で登場せず、また\Delta^+にも現れないので、自由変数の交換のもとで同等の推論規則であることがわかります[10]。lean4-logicでは以下のように形式化されます。

inductive DerivationCR (P : SyntacticFormula L → Prop) :
    Sequent L → Type u
| axL   : ∀ (Δ : Sequent L) {k} (r : L.rel k) (v : Fin k → SyntacticTerm L),
    rel r v ∈ Δ → nrel r v ∈ Δ → DerivationCR P Δ
| verum : ∀ (Δ : Sequent L), ⊤ ∈ Δ → DerivationCR P Δ
| or    : ∀ (Δ : Sequent L) (p q : SyntacticFormula L),
    DerivationCR P (insert p $ insert q Δ) →
      DerivationCR P (insert (p ⋎ q) Δ)
| and   : ∀ (Δ : Sequent L) (p q : SyntacticFormula L),
    DerivationCR P (insert p Δ) →
      DerivationCR P (insert q Δ) →
        DerivationCR P (insert (p ⋏ q) Δ)
| all   : ∀ (Δ : Sequent L) (p : SyntacticSubformula L 1),
    DerivationCR P (insert (Rew.free.hom p) (shifts Δ)) →
      DerivationCR P (insert (∀' p) Δ)
| ex    : ∀ (Δ : Sequent L) (t : SyntacticTerm L) (p : SyntacticSubformula L 1),
    DerivationCR P (insert ([→ t].hom p) Δ) →
      DerivationCR P (insert (∃' p) Δ)
| cut   : ∀ (Δ Γ : Sequent L) (p : SyntacticFormula L), P p →
    DerivationCR P (insert p Δ) → DerivationCR P (insert (~p) Γ) →
      DerivationCR P (Δ ∪ Γ)

SyntacticTerm, SyntacticFormulaは自由変数が\Nである項・論理式を意味します。
（上の形式化においてP : SyntacticFormula L → Propのパラメータを用いているのはカット除去定理の証明のために(Cut)の使用が制限されたTait計算が必要だからです）

理論Tからの証明可能性T \vdash \Deltaは、\tau_0, \tau_1, ... \in Tが存在して\vdash_\mathsf{T} \lnot \tau_0, \lnot \tau_1, ..., \Deltaを満たすことと定義します。

structure DerivationCRWA (P : SyntacticFormula L → Prop) (T : Theory L) (Δ : Sequent L) where
  leftHand : Finset (Sentence L)
  hleftHand : ↑leftHand ⊆ (~·) '' T
  derivation : ⊢ᶜ[P] Δ ∪ (leftHand.image Rew.emb.hom)

scoped notation :45 T " ⊢ᶜ[" P "] " Γ:45 => DerivationCRWA P T Γ

意味論

言語LのM上の構造s : Structure L Mは関数記号fの解釈s.func f : (Fin k → M) → Mと関係記号rの解釈s.rel r : (Fin k → M) → Propの組です。

@[ext] class Structure (L : Language) (M : Type*) where
  func : ⦃k : ℕ⦄ → L.func k → (Fin k → M) → M
  rel : ⦃k : ℕ⦄ → L.rel k → (Fin k → M) → Prop

これはL, Mの型クラスとして定義されています。よく言語Lの構造\mathfrak Aをその台集合|\mathfrak A|で略記することがよくありますが、それと似たように構造を扱うことができます。

項の解釈Subterm.valを定義したあと、Tarskiの真理定義にしたがって論理式の解釈を定義します。

def Eval' (s : Structure L M) (ε : μ → M) :
    ∀ {n}, (Fin n → M) → Subformula L μ n → Prop
  | _, _, ⊤        => True
  | _, _, ⊥        => False
  | _, e, rel p v  => s.rel p (fun i => Subterm.val s e ε (v i))
  | _, e, nrel p v => ¬s.rel p (fun i => Subterm.val s e ε (v i))
  | _, e, p ⋏ q    => p.Eval' s ε e ∧ q.Eval' s ε e
  | _, e, p ⋎ q    => p.Eval' s ε e ∨ q.Eval' s ε e
  | _, e, ∀' p     => ∀ x : M, (p.Eval' s ε (x :> e))
  | _, e, ∃' p     => ∃ x : M, (p.Eval' s ε (x :> e))

等号について

この体系では等号の記号が言語に含まれることを必ずしも要求していませんでした。また推論規則にも等号の推論規則は含まれないので、等号に関する諸規則は理論Tに等号の公理Theory.Eqを含めることによって代用します。

inductive Eq : Theory L
  | refl : Eq “∀ #0 = #0”
  | symm : Eq “∀ ∀ (#1 = #0 → #0 = #1)”
  | trans : Eq “∀ ∀ ∀ (#2 = #1 → #1 = #0 → #2 = #0)”
  | funcExt {k} (f : L.func k) :
    Eq “∀* (!(Subformula.vecEq varSumInL varSumInR) →
      !!(Subterm.func f varSumInL) = !!(Subterm.func f varSumInR))”
  | relExt {k} (r : L.rel k) :
    Eq “∀* (!(Subformula.vecEq varSumInL varSumInR) →
      !(Subformula.rel r varSumInL) → !(Subformula.rel r varSumInR))”

Theory.Eqを含む理論Tが充足可能ならば、そのモデルMを同値関係a \equiv b \iff M \models (a = b)で割ったモデルM'が得られ、そのモデルでは等号が通常の解釈と同様に扱うことができます。

完全性定理

一階論理の完全性定理の証明にはいろいろな方法がありますが、形式的証明の多くはHenkin流のものです[11]。lean4-logicの前身であるlean-logicですでにHenkin流の証明を行っていたので別の方法で証明したいと思い、Tait計算の証明探索で完全性定理を証明しました。数学的な解説は国立公園に書いたのでそちらを参照してください。

算術

基礎的な準備がだいたい整ったのでより具体的な内容に移ります。

順序環の言語L_\mathrm{OR}は0,1,+,\cdot,=,<の記号からなる言語です（lean4-logicではℒₒᵣに対応します）。ペアノの公理\mathbf{PA}のフラグメントである公理\mathbf{PA}^-を次のように定義します。

inductive PAminus : Theory L
  | addZero       : PAminus “∀ #0 + 0 = #0”
  | addAssoc      : PAminus “∀ ∀ ∀ (#2 + #1) + #0 = #2 + (#1 + #0)”
  | addComm       : PAminus “∀ ∀ #1 + #0 = #0 + #1”
  | addEqOfLt     : PAminus “∀ ∀ (#1 < #0 → ∃ #2 + #0 = #1)”
  | zeroLe        : PAminus “∀ (0 ≤ #0)”
  | zeroLtOne     : PAminus “0 < 1”
  | oneLeOfZeroLt : PAminus “∀ (0 < #0 → 1 ≤ #0)”
  | addLtAdd      : PAminus “∀ ∀ ∀ (#2 < #1 → #2 + #0 < #1 + #0)”
  | mulZero       : PAminus “∀ #0 * 0 = 0”
  | mulOne        : PAminus “∀ #0 * 1 = #0”
  | mulAssoc      : PAminus “∀ ∀ ∀ (#2 * #1) * #0 = #2 * (#1 * #0)”
  | mulComm       : PAminus “∀ ∀ #1 * #0 = #0 * #1”
  | mulLtMul      : PAminus “∀ ∀ ∀ (#2 < #1 ∧ 0 < #0 → #2 * #0 < #1 * #0)”
  | distr         : PAminus “∀ ∀ ∀ #2 * (#1 + #0) = #2 * #1 + #2 * #0”
  | ltIrrefl      : PAminus “∀ ¬#0 < #0”
  | ltTrans       : PAminus “∀ ∀ ∀ (#2 < #1 ∧ #1 < #0 → #2 < #0)”
  | ltTri         : PAminus “∀ ∀ (#1 < #0 ∨ #1 = #0 ∨ #0 < #1)”

第一不完全性定理を示すだけなら\mathbf{PA}^-より弱い\mathbf{Q}でもよいし、むしろこのほうが一般的に用いられている気がしますが、\mathbf{PA}^-はそのモデルが割と自然な性質を持っているためMathlibで証明された様々な性質を利用でき（例えばLinearOrderedCommSemiringやCanonicallyOrderedAddCommMonoidなどのインスタンスになることが示せます）、モデル論的な証明可能性の証明が書きやすいです。

算術の\Sigma_n, \Pi_n論理式を以下のように定義します。ちなみにこれは嘘ですが[12]、ここでは問題ありません。

local notation "Σ" => Bool.true
local notation "Π" => Bool.false

inductive Hierarchy : Bool → ℕ → {n : ℕ} → Subformula L μ n → Prop
  | verum (b s n)                             :
    Hierarchy b s (⊤ : Subformula L μ n)
  | falsum (b s n)                            :
    Hierarchy b s (⊥ : Subformula L μ n)
  | rel (b s) {k} (r : L.rel k) (v)           :
    Hierarchy b s (Subformula.rel r v)
  | nrel (b s) {k} (r : L.rel k) (v)          :
    Hierarchy b s (Subformula.nrel r v)
  | and {b s n} {p q : Subformula L μ n}      :
    Hierarchy b s p → Hierarchy b s q → Hierarchy b s (p ⋏ q)
  | or {b s n} {p q : Subformula L μ n}       :
    Hierarchy b s p → Hierarchy b s q → Hierarchy b s (p ⋎ q)
  | ball {b s n} {p : Subformula L μ (n + 1)} :
    (t : Subterm L μ n) →
      Hierarchy b s p → Hierarchy b s “∀[#0 < !!(Rew.bShift t)] !p”
  | bex {b s n} {p : Subformula L μ (n + 1)}  :
    (t : Subterm L μ n) →
      Hierarchy b s p → Hierarchy b s “∃[#0 < !!(Rew.bShift t)] !p”
  | ex {s n} {p : Subformula L μ (n + 1)}     :
    Hierarchy Σ (s + 1) p → Hierarchy Σ (s + 1) (∃' p)
  | all {s n} {p : Subformula L μ (n + 1)}    :
    Hierarchy Π (s + 1) p → Hierarchy Π (s + 1) (∀' p)
  | sigma {s n} {p : Subformula L μ (n + 1)}  :
    Hierarchy Π s p → Hierarchy Σ (s + 1) (∃' p)
  | pi {s n} {p : Subformula L μ (n + 1)}     :
    Hierarchy Σ s p → Hierarchy Π (s + 1) (∀' p)

完全性定理より、モデル論的に証明可能性を扱うことで\mathbf{PA}^-を含む理論Tについて\Sigma_1-完全性を証明することができます。

theorem sigma_one_completeness
    {σ : Sentence ℒₒᵣ} (hσ : Hierarchy.Sigma 1 σ) :
    ℕ ⊧ σ → T ⊢ σ := fun H =>
  Complete.complete (consequence_of _ _ (fun M _ _ _ _ _ => by
    haveI : Theory.Mod M (Theory.PAminus ℒₒᵣ) :=
      Theory.Mod.of_subtheory (T₁ := T) M (Semantics.ofSystemSubtheory _ _)
    simpa using
      @Model.sigma_one_completeness M _ _ _ _ _ _ hσ ![]
        (by simpa[models_iff] using H)))

計算可能性

不完全性定理を証明するにあたっての目標の一つがr.e.集合の表現定理です。またTが計算可能であるとき証明可能な論理式の集合\{\sigma \in L_\mathrm{OR} | T \vdash \sigma\}が適切なエンコーディングのもとr.e.集合であることを示す必要があります。後者はあまり厳密に証明されることがない事実ですが、形式的証明では十分に厳密に書く必要があり、おそらく最も厳しい証明でした。

mathlib4では計算可能性や原始再帰的関数に関する諸定理が形式化されているので、これを用います。SubtermやSubformulaについて、それぞれの計算論的な定義や証明を行うのはとても辛いと考えられるためまず適当な条件を満たすW-typeについてエンコーディングやインダクションの原始再帰性を証明します。SubtermやSubformulaはあるW-typeのSubtypeであるため、UTermやUFormulaといった補助的な型を経由してその計算論的性質を示しました。またよくある方法によってTait計算の証明可能性がr.e.であることが示せます。よって以下が証明できます[13]。

lemma provable_RePred : RePred (T ⊢! ·) :=
  (provableFn_partrec T).of_eq <| by
    intro σ; ext; simp[←provable_iff_provableFn]

r.e.集合の表現定理を示すため、L_\mathrm{OR}の\Sigma_1論理式でそのグラフが表現されるような（部分）関数をArith₁(ArithPart₁)と定義します。

inductive ArithPart₁ : ∀ {n}, (Vector ℕ n →. ℕ) → Prop
  | zero {n} : @ArithPart₁ n (fun _ => 0)
  | one {n} : @ArithPart₁ n (fun _ => 1)
  | add {n} (i j : Fin n) :
    @ArithPart₁ n (fun v => v.get i + v.get j : Vector ℕ n → ℕ)
  | mul {n} (i j : Fin n) :
    @ArithPart₁ n (fun v => v.get i * v.get j : Vector ℕ n → ℕ)
  | proj {n} (i : Fin n) :
    @ArithPart₁ n (fun v => v.get i : Vector ℕ n → ℕ)
  | equal {n} (i j : Fin n) :
    @ArithPart₁ n (fun v => isEqNat (v.get i) (v.get j) : Vector ℕ n → ℕ)
  | lt {n} (i j : Fin n) :
    @ArithPart₁ n (fun v => isLtNat (v.get i) (v.get j) : Vector ℕ n → ℕ)
  | comp {m n f} (g : Fin n → Vector ℕ m →. ℕ) :
    ArithPart₁ f → (∀ i, ArithPart₁ (g i)) →
      ArithPart₁ fun v => (mOfFn fun i => g i v) >>= f
  | rfind {n} {f : Vector ℕ (n + 1) → ℕ} :
    ArithPart₁ (n := n + 1) f →
      ArithPart₁ (fun v => rfind fun n => some (f (n ::ᵥ v) = 0))

def Arith₁ (f : Vector ℕ n → ℕ) := ArithPart₁ (n := n) f

isEqNat n mはn = mであるとき1, そうでないとき0を返す関数です（isLtNatも同様）。ArithPart₁はr.e.部分関数のクラスPartrec'と同等であることがGödelのβ関数を用いて示せます。

表現定理

ArithPart₁の構成に関する帰納法により、ArithPart₁の部分関数のグラフを表現する論理式を構成します。

def codeAux : {k : ℕ} → Nat.ArithPart₁.Code k → Formula ℒₒᵣ (Fin (k + 1))
  | _, Code.zero _    => “&0 = 0”
  | _, Code.one _     => “&0 = 1”
  | _, Code.add i j   => “&0 = !!&i.succ + !!&j.succ”
  | _, Code.mul i j   => “&0 = !!&i.succ * !!&j.succ”
  | _, Code.equal i j =>
    “(!!&i.succ = !!&j.succ ∧ &0 = 1) ∨ (!!&i.succ ≠ !!&j.succ ∧ &0 = 0)”
  | _, Code.lt i j    =>
    “(!!&i.succ < !!&j.succ ∧ &0 = 1) ∨ (¬!!&i.succ < !!&j.succ ∧ &0 = 0)”
  | _, Code.proj i    => “&0 = !!&i.succ”
  | _, Code.comp c d  =>
    exClosure (((Rew.bind ![] (&0 :> (#·))).hom (codeAux c)) ⋏
      Matrix.conj fun i =>
        (Rew.bind ![] (#i :> (&·.succ))).hom (codeAux (d i)))
  | _, Code.rfind c   =>
    (Rew.bind ![] (⸢0⸣ :> &0 :> (&·.succ))).hom (codeAux c) ⋏
    (∀[“#0 < &0”] ∃' “#0 ≠ 0” ⋏
      (Rew.bind ![] (#0 :> #1 :> (&·.succ))).hom (codeAux c))

Nat.ArithPart₁.Code kは部分関数f : Vector ℕ k →. ℕがArithPart₁であることを表す命題のメタ証明から非構成的にしか得られないことに注意してください。またこの論理式は\Sigma_1なので、Tの\Sigma_1完全性と\Sigma_1健全性から表現定理が証明可能です。

theorem representation {f : α →. σ} (hf : Partrec f) {x y} :
    T ⊢! (graph f)/[⸢y⸣, ⸢x⸣] ↔ y ∈ f x := by
  let f' : Vector ℕ 1 →. ℕ :=
    fun x => Part.bind (decode (α := α) x.head) fun a => (f a).map encode
  have : Nat.Partrec' f' :=
    Nat.Partrec'.part_iff.mpr
      (Partrec.bind
        (Computable.ofOption $
	  Primrec.to_comp $ Primrec.decode.comp Primrec.vector_head)
      (Partrec.to₂ <|
        Partrec.map (hf.comp .snd) (Computable.encode.comp₂ .right)))
  simpa[Matrix.constant_eq_singleton] using
    provable_iff_mem_partrec this (y := encode y) (v := ![encode x])

ここでp/[t,u,...]は論理式pの変数に#0 ↦ t, #1 ↦ u, ...を代入した論理式を表します。

不完全性定理

聡明なる皆さんはすでにお気づきかと思いますが、この第一不完全性定理の証明はよくある証明と異なり対角化補題を証明しませんし、可証性述語を明示的に用いることさえしません。これは計算論的な証明で、Current research on Gödel's incompleteness theorems[5:1]で分類されている内のRecursion-theoretic proofsの変種だと考えています（完全に計算論的か？と言われるとそうでもない気がしますが）。

第一不完全性定理

まず証明可能性はr.eであることと、代入の操作が原始再帰的であることから集合Dはr.e.です。

D \coloneqq \{\varphi\ |\ T \vdash \lnot\varphi(\ulcorner \varphi \urcorner)\} 
private lemma diagRefutation_re : RePred (fun σ => T ⊢! ~σ/[⸢σ⸣]) := by
  -- 省略

表現定理よりDを表現する論理式ρが存在します。

lemma diagRefutation_spec (σ : FormulaFin ℒₒᵣ 1) :
    T ⊢! ρ/[⸢σ⸣] ↔ T ⊢! ~σ/[⸢σ⸣] := by
  simpa[diagRefutation] using
    pred_representation (diagRefutation_re T) (x := σ)

ここでγ := ρ/[⸢ρ⸣]と置くと、Tが無矛盾であることから、γが証明も反証もできない文であることが証明できます。

lemma independent : System.Independent T γ := by
  have h : T ⊢! γ ↔ T ⊢! ~γ := by simpa using diagRefutation_spec T ρ
  exact
    ⟨System.unprovable_iff_not_provable.mpr
       (fun b => inconsistent_of_provable_and_refutable' b (h.mp b) 
	 (consistent_of_sigmaOneSound T)),
     System.unprovable_iff_not_provable.mpr
       (fun b => inconsistent_of_provable_and_refutable' (h.mpr b) b 
         (consistent_of_sigmaOneSound T))⟩

したがって第一不完全性定理が示されました。

theorem main : ¬System.Complete T := 
  System.incomplete_iff_exists_independent.mpr ⟨γ, independent T⟩

第二不完全性定理

第一不完全性定理を証明したので第二不完全性定理も証明したいのですが、第一のために行った証明は表現定理を使った非構成的なもので、この方法で第二不完全性定理を証明するのはおそらく不可能です。証明可能な論理式の集合はr.e.なのでそれを表現する論理式は存在しますが、可導性条件などを導出するのは難しく、根本的に別の方法で証明する必要があるように思います。実際Isabelleによる第二不完全性定理の証明では算術の理論ではなく遺伝的集合の理論
の上で示されており、そのような工夫が必要になると考えています。

参考文献

  • J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis
  • W. Pohlers, Proof Theory: The First Step into Impredicativity
  • P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic
  • R. Kaye, Models of Peano Arithmetic
  • 田中 一之, ゲーデルと20世紀の論理学
脚注

  1. https://www.cs.utexas.edu/users/moore/best-ideas/nqthm/index.html ↩︎

  2. https://arxiv.org/abs/cs/0505034 ↩︎

  3. https://arxiv.org/abs/2104.13792 ↩︎

  4. https://github.com/flypitch/flypitch ↩︎

  5. ↩︎ ↩︎

  6. https://leanprover-community.github.io/mathlib4_docs//Mathlib/ModelTheory/Basic.html ↩︎

  7. ちなみにIsabelleによる第二不完全性定理の形式的証明ではnominal typesによって表現されています。 ↩︎

  8. Fin kは有限集合\{0,1,...,k-1\}のようなもので、Fin k → αは長さkのαの列を表します。 ↩︎

  9. 束縛変数が束縛されていない項・論理式に対しSubterm, Subformulaとい名称を用いていますが、この名称は論理学において別の意味を持つことがあるので、あまり適切ではないかもと思っています。 ↩︎

  10. このような手法はflypitchのコードを読んで初めて知ったのですが、もしかしたら一般的な対処法かもしれません。 ↩︎

  11. 前述したflypitchやhydra-gamesなど ↩︎

  12. 通常\Sigma_n(\Pi_n)論理式は\Sigma_0論理式に量化子が\exists(\forall)からはじまり交互にn個現れる論理式として、またそのような論理式と理論Tで同等であることが証明できるものとして定義されます。Hierarchyの定義は\Sigma_n,\Pi_n論理式が限定量化で閉じているように書かれていますが、これはTが\Sigma_{n}採集原理\mathbf{B}\Sigma_{n}を含意していればTで成立します ↩︎

  13. lean4-logicにおいてT ⊢ σはTにおけるσの証明を意味します。一方T ⊢! σはTにおけるσの証明が存在するという命題を意味します（実際単なるNonempty (T ⊢ σ)の略記です） ↩︎

Discussion