Zenn
Open5

lean4による論理学の形式化

lean4
ピン留めされたアイテム
palalansoukipalalansouki

https://github.com/iehality/lean4-logic

目標

  • lean3で書いたlean-logicをlean4で書き直す ✅
  • 完全性定理の証明をする ✅
  • カット除去定理を証明する ✅
  • 主に算術のメタ数学を展開するにあたって適切な記法やDSL、環境を整備する
    • a \le b \iff a = b \lor a < bなどの略記を適当に行えるようにする
      • SubTerm.Operator, FirstOrder.SubFormula.Operatorを整備する
    • 現状PrincipiaのDSLは補題などの宣言をformulaSyntaxToExprなどでExprに変換して扱っているが、これではformulaSyntaxToExprで対応していない記法は対応できないので、termに変換してelabTermなど汎用的な方法でExprに変換するようにする
  • Gödelの不完全性定理を証明する
palalansoukipalalansouki

自動証明

proveTautoやproveに関するメモ

戦略

素朴な方法だがTait計算の証明探索をそのまま行う。論理式をその構造で分解して
\vdash \varphi, \Gamma（ただし{\sim} \varphi \in \Gamma）または\vdash \top, \Gammaとなったときに証明を完了させる。またhypothesisで\vdash \Deltaがすでに証明されていたり仮定されたりするときそれも用いる。

メタプログラミング

証明探索に用いる論理式の推件は論理式SyntacticFormula LのExprのリストG : List Q(SyntacticFormula $L)として扱う（Lean4の証明ではtoQList G : Q(List (SyntacticFormula $L))に変換して埋め込む）。論理式の導出規則において上の推件の論理式を改変することがあるが、改変を計算するために論理式の正規化（この呼称が適切なのかわからない）が必要になる。

正規化

Lean4やMathlibでは何らかの項の正規化のために以下のような関数を用いることが多いようである：

result : (e : Q($α)) → MetaM ((res : Q($α)) × Q($e = $res))

（例：Lean.Meta.Simp.Result, Mathlib.Tactic.Ring.ResultおよびMathlib.Tactic.Ring.eval）
これらを参考にし同様のresultを定義した：FirstOrder.SubFormula.Meta.result。加えて実際の計算では何らかの関数f : α → βによる計算の正規化が必要になるため以下のような関数

result : (e : Q($α)) → MetaM ((res : Q($β)) × Q(f $e = $res))

も用いる（例：FirstOrder.SubFormula.Meta.resultNeg : (p : Q(SyntacticSubFormula $L $n)) → MetaM ((res : Q(SyntacticSubFormula $L $n)) × Q(~$p = $res))）

矛盾の検出\vdash \varphi, \Gamma, {\sim} \varphi \in \Gammaのためh : G.elem q(p) = trueというLean4のメタ証明からQ(p ∈ toQList G)を生成する必要があるが、これはQq.toQListOfElem {α : Q(Type u)} {a : Q($α)} : {l : List Q($α)} → l.elem a → Q($a ∈ $(toQList (u := u) l))で行っている（これはもっと効率的な方法がある気がする）。

証明探索

hypothesisの証明のチェックではisImplementationDetailでLean.MonadLCtx.getLCtxからゴールの命題や表示されない命題を除外できる。

proveTautoは量化子を考慮しない論理式の証明をおこなう。proveは量化子にも対応しており、... by prove [t, u, ...]のように書くことでt, u, ...を存在量化子の証明に使用されるwitnessに指定できる

example : Valid “((!p → !q) → !p) → !p” := by proveTauto
example : Valid “!p ∧ !q ∧ !r ↔ !r ∧ !p ∧ !q”  := by proveTauto
example (_ : Valid p) : Valid “!p ∨ !q”  := by proveTauto
example : Valid (L := oring) “&0 < &1 → ∃ ∃ #0 < #1” := by prove
example (_ : Valid (L := oring) “0 < 4 + 9”) :
    Valid (L := oring) “⊤ ∧ (∃ 0 < 4 + #0)”  := by prove [T“9”]

実装はできたがあまり速くはない。

palalansoukipalalansouki

一階論理の完全性定理の証明

https://github.com/iehality/lean4-logic/tree/master/Logic/Predicate/FirstOrder/Completeness

Tait計算の証明探索を用いて完全性定理を証明する。ただし証明探索は可算言語にのみ行える点に注意する。

証明の道筋

定理

  • \Gammaを可算言語の論理式の有限集合とする。以下が成り立つ
    • \Gammaの証明探索木がwell-foundedならば\Gammaは証明可能
      • FirstOrder.SearchTree.syntacticMainLemma_top
    • \Gammaの証明探索木がwell-foundedでないならば\Gammaのすべてが成立しない構造が存在する
      • FirstOrder.SearchTree.semanticMainLemma_top

定理：可算言語の狭義の完全性定理

  • 可算言語Lの有限集合\Gammaが以下を満たすとき\Gammaは証明可能
    • 任意のLの構造Mについて、ある\psi \in \Gammaが存在してM \models \psi
  • FirstOrder.completenessₙ_of_encodable

定理：狭義の完全性定理

  • 言語Lの有限集合\Gammaが以下を満たすとき\Gammaは証明可能
    • 任意のLの構造Mについて、ある\psi \in \Gammaが存在してM \models \psi
  • FirstOrder.completenessₙ

定理：完全性定理

  • 言語Lの理論T, 文\sigmaについて、T \models \sigmaならばT \vdash \sigma
  • FirstOrder.completeness

参考文献

  • Wolfram Pohlers, Proof Theory: The First Step into Impredicativity
    • この本では可算言語の完全性定理を証明探索から直接証明しているが、ここでは狭義のもので十分なのでその方法を用いた
    • その代わり言語の変換の意味論に関する諸定理やコンパクト性定理などを証明する必要がある
  • 田中 一之, 計算理論と数理論理学
    • 狭義の完全性定理からコンパクト性定理を用いて一般の完全性定理を証明するという方法はこれを参考にした
palalansoukipalalansouki

証明探索

https://github.com/iehality/lean4-logic/blob/master/Logic/Predicate/FirstOrder/Completeness/SearchTree.lean

リストの組み合わせ論的な？性質を証明するのが面倒だったため、証明方法は標準的でない。

論理式（ここではSyntacticFormula L: 自然数の変項\&0, \&1, \&2, ...を持つ論理式 を表すとする）の有限集合を\Gammaと表記する。述語Rの原子項をR(\vec v)と表記する。またLを可算言語とする。

順序FirstOrder.SearchTreeAt s(\prec_s)を定義する

  • \varphi, tを自然数にエンコードしたものを\ulcorner \varphi \urcorner, \ulcorner t \urcornerと表記する
  • 自然数の3つ組ペアをエンコードした自然数を\braket{n, m, i}と表記する
順序$\Delta \prec_s \Gamma$の定義
  • R(\vec v) \in \Gammaかつ\lnot R(\vec v) \notin \Gammaのとき
\Gamma \prec_{\braket{\ulcorner R(\vec v) \urcorner, \ulcorner t \urcorner, i}} \Gamma
  • \lnot R(\vec v) \in \GammaかつR(\vec v) \notin \Gammaのとき
\Gamma \prec_{\braket{\ulcorner \lnot R(\vec v) \urcorner, \ulcorner t \urcorner, i}} \Gamma
  • \bot \in \Gammaのとき
\Gamma \prec_{\braket{\ulcorner \bot \urcorner, \ulcorner t \urcorner, i}} \Gamma
  • \varphi \land \psi \in \Gammaのとき
\{\varphi\} \cup \Gamma \prec_{\braket{\ulcorner \varphi \land \psi \urcorner, \ulcorner t \urcorner, i}} \Gamma \\ \{\psi\} \cup \Gamma \prec_{\braket{\ulcorner \varphi \land \psi \urcorner, \ulcorner t \urcorner, i}} \Gamma
  • \varphi \lor \psi \in \Gammaのとき
\{\varphi, \psi\} \cup \Gamma \prec_{\braket{\ulcorner \varphi \lor \psi \urcorner, \ulcorner t \urcorner, i}} \Gamma
  • (\forall x) \varphi(x) \in \Gammaのとき
    • ただしv_\Gammaは\Gammaに登場する変数の最大値+1の自然数とする
\{\varphi(\& v_\Gamma)\} \cup \Gamma \prec_{\braket{\ulcorner (\forall x)\varphi(x) \urcorner, \ulcorner t \urcorner, i}} \Gamma
  • (\exists x) \varphi(x) \in \Gammaのとき
\{\varphi(t)\} \cup \Gamma \prec_{\braket{\ulcorner (\exists x)\varphi(x) \urcorner, \ulcorner t \urcorner, i}} \Gamma
  • s = \braket{\ulcorner \varphi \urcorner, \ulcorner t \urcorner, i}を満たすような\varphi \in \Gamma, tが存在しないとき
\Gamma \prec_{s} \Gamma

順序FirstOrder.SearchTree(\prec)を定義する

(\prec_s)をこのように

... \Delta_{s+1} \prec_s \Delta_s ... \Delta_3 \prec_2 \Delta_2 \prec_1 \Delta_1 \prec_0 \Delta_0 = \Gamma

\Delta_0 = \Gammaを最大値にして順に並べた順序を(\prec)とする