lean4-logic
https://scrapbox.io/files/63fd8080c66d48001bfbb2aa.png
L：言語
μ：自由変数の型
k：アリティ
f：関数記号
r：関係記号
ω τ ...：書き換え
Φ Ψ ...：言語の書き換え
t u ...：項
M N ...：モデル
名前空間
FirstOrderがMathlib4と競合しているため論理学に関するものはすべてLO下に定義することにした 一階論理
項, 論理式
例によってDe Bruijn indexを採用する
自由変項を&x, 束縛変項を#xと書く
LO.FirstOrder.SubFormula L μ n
$ n個の束縛されない束縛変数を持ちうる部分論理式
LO.FirstOrder.Formula L μ
LO.FirstOrder.SubFormula L μ 0のabbreviation
LO.FirstOrder.Sentence L
LO.FirstOrder.SubFormula L Empty 0のabbreviation
LO.FirstOrder.SyntacticFormula L n
証明などに用いる
記法
LO.FirstOrder.SubFormulaは“”で囲んで“&0 < &1 → ∃ ∃ #0 < #1”のように記述できる
別のp : SubFormula L μ nを用いるときは“ ... !p ... ”とかく
LO.FirstOrder.SubTermはT“”で囲んでT“0 + &2 * #9”のように記述できる
項の書き換え
LO.FirstOrder.Rew
LO.FirstOrder.Rewは以下を満たすような写像$ \omegaのクラス
$ \omega (f(t_1, ..., t_k)) = f(\omega(t_1), ..., \omega(t_k))
自然に論理式の写像に拡張できる. (LO.FirstOrder.Rew.hom)
$ \omega(r(t_1, ..., t_k)) = r(\omega(t_1), ..., \omega(t_k))
$ \omega(\top) = \top
$ \omega(\bot) = \bot
$ \omega(\varphi \land \psi) = \omega(\varphi) \land \omega(\psi)
$ \omega(\varphi \lor \psi) = \omega(\varphi) \lor \omega(\psi)
$ \omega(\forall\varphi) = \forall\omega^q(\varphi)
$ \omega(\exists\varphi) = \exists\omega^q(\varphi)
$ \omega^qは以下のように定義される
$ \omega^q(\#0) \coloneqq \#0
$ \omega^q(\#(x+1)) \coloneqq \mathsf{bShift}(\omega(\# x))
$ \omega^q(\& x) \coloneqq \mathsf{bShift}(\omega(\& x))
なので今までのように項と論理式で二重に定義しなくて良い
LO.FirstOrder.Rew.bind
以降のすべての書き換えはbindの制限である
LO.FirstOrder.Rew.map
LO.FirstOrder.Rew.rewrite
LO.FirstOrder.Rew.substs
LO.FirstOrder.Rew.emb
LO.FirstOrder.Rew.bShift
LO.FirstOrder.Rew.shift
LO.FirstOrder.Rew.free
LO.FirstOrder.Rew.fix
証明
普通の数学をやるならLO.FirstOrder.ProofとLO.FirstOrder.DerivationCWAでよい
LO.FirstOrder.Derivation ⊢ᵀ Δ
LO.FirstOrder.DerivationC ⊢ᶜ Δ
LO.FirstOrder.DerivationWA T ⊢ᵀ Δ
LO.FirstOrder.DerivationCWA T ⊢' Δ
LO.FirstOrder.Proof T ⊢ σ
文の証明
構造
mathlibを参考にし一階論理の構造LO.FirstOrder.Structureをクラスとして定義する 等号$ =を持つとは限らない
等号は普通の二項関係と同様に扱う
等号の公理を満たす構造が存在すれば同値関係で割って通常の意味でのモデルが得られるので, おそらく問題ない 自動証明
壊れている
Tait計算の証明探索
by proveTautoで量化子を含まない簡単なトートロジーを証明できる
by prove, by prove [t, u, ...]で量化子を含む命題の簡単な証明ができる
[t, u, ...]は存在量化子のwitnessとして使用される。指定しない場合は[&0, &1]
例：
code:lean4
example : valid “((!p → !q) → !p) → !p” := by proveTauto
example : valid “!p ∧ !q ∧ !r ↔ !r ∧ !p ∧ !q” := by proveTauto
example (d : 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” 完全性定理
$ T \vDash \varphi \iff \lnot\text{Satisfiable}(T \cup \{\lnot \varphi\})
$ \iff \exists_{U \in \mathcal{P}_{<\aleph_0}(T \cup \{\lnot \varphi\})} [\lnot \text{Satisfiable}(U)]
$ \iff \exists_{U \in \mathcal{P}_{<\aleph_0}(T)} [\lnot\text{Con}(U)]
より厳密には
可算言語$ L_Uを定義し, 言語の書き換え写像$ f \colon \text{Formula}(L_U) \to \text{Formula}(L)について$ f "(U') = Uを満たすような$ U'が取れる
$ \lnot\text{Satisfiable}(f"(U')) \implies \lnot\text{Satisfiable}(U')だから可算言語の完全性定理より$ \lnot\text{Con}(U') $ \lnot\text{Con}(U') \implies \lnot\text{Con}(f"(U'))だから$ \lnot\text{Con}(U)
$ \iff \lnot\text{Con}(T \cup \{\lnot \varphi\})
証明のコンパクト性
$ \iff T \vdash \varphi
感想
Tait計算の論理式を採用しているため直観主義の公理などを記述できない 普通にヒルベルト流の証明体系でヘンキン流の完全性定理の証明をするほうが楽な気がしてきた
Tait計算では$ \phi_1 \lor \phi_2 \lor \phi_3 \iff \phi_3 \lor \phi_2 \lor \phi_1, $ \lnot(\phi \to \forall \psi) \iff \phi \land \exists \lnot \psiなどが自明なのでずっと楽 これはヘンキン流でもそう
Many-sorted logic
量化子を$ (Q x. \phi(x))[\psi(x)] という式を基礎として定義している
うまくいったらLO.FirstOrderなどに取り入れる可能性がある