SnO₂WMaNさんとpalalansoukîさんがやっているFormalized Formal Logic · GitHub というとても興味深いプロジェクトがありまして、去年ZFCを形式化しようとしていたのが目に止まったらしく、ZF集合論関係のことをできないかと言われたあと仕事＋プライベートで色々あって完全放置になっていたのですが、ちょっとずつやっていこうと思います。
公理系
公理系の記述はFoundation.FirstOrder.SetTheory.Basic.Axiom.leanにある。Sentence ℒₛₑₜとかいうのは言語がℒₛₑₜな文の型なんだろうなぁとか推測しながら見ていれば素直にわかる。なお、そのあたりの型はFoundation.FirstOrder.Basic.Syntax.Formula.leanで定義されている。例えば
def empty : Sentence ℒₛₑₜ := “∃ e, ∀ y, y ∉ e”
ただ、スキーマになる分出公理と置換公理はSyntacticSemiformulaという型の引数を取っているが、まあそれもなんとなくは分かる。
それらの個別の公理をまとめて、Theory ℒₛₑₜという型のZermelo, ZermeloFraenkel, ZermeloFraenkelChoiceなどというのが定義されている。
モデル
それらのモデルを作るには、variable {V : Type*} [SetStructure V] [Nonempty V] [V ⊧ₘ* 𝗭𝗙𝗖]などと書けば良い。らしい。⊧ₘは左辺が右辺の理論のモデルになっていることを意味する。がついているのは右側が理論、すなわち文の集合になっていることを指し、*がついていない⊧ₘは右辺は文になる。
空集合
ここから何をやるにも、まず、VがZFCのそれぞれの公理を満たすことがわかってないといけない。例えばV ⊧ₘ Axiom.emptyとかが言えないと先に進まない。この時点で戸惑っていたのだけれども、最終的に書けたのがこれ。
lemma V_models_empty : V ⊧ₘ Axiom.empty := by
-- You can split V ⊧ₘ* 𝗭𝗙𝗖 into V ⊧ₘ* 𝗭𝗙 ∧ V ⊧ₘ* 𝗔𝗖
simp only [ModelsTheory.add_iff] at hV_ZFC
obtain ⟨hV_ZF, hV_AC⟩ := hV_ZFC
-- By this, we can interpret ⊧ₘ* by using ⊧ₘ
apply modelsTheory_iff.mp at hV_ZF
-- Use ZermeloFraenkel.axiom_of_empty_set, the instance of Axiom.empty
apply hV_ZF ZermeloFraenkel.axiom_of_empty_set
𝗭𝗙𝗖は𝗭𝗙 + 𝗔𝗖として定義されているので、それを使って分解して、⊧ₘ* は右辺に属する文を全部満たすことだよとmodelsTheory_iff.mpfで解釈してから、Axiom.emptyが𝗭𝗙に属していることを使う。
というところで、それより更に進んだものがすでにZ.leanでやられていることを知る。
lemma empty_exists : ∃ e : V, IsEmpty e := by simpa [models_iff] using ModelsTheory.models V Zermelo.axiom_of_empty_set
def IsEmpty (a : V) : Prop := ∀ x, x ∉ aとなっているので、これはまさにAxiom.emptyを解釈したあとの姿になっている。
えーと、こんなもの読んでいる人はさすがに数理論理学の基礎の基礎は知っている人たちだろうから、説明は適当でいいよね。つまり、Vという構造が“∃ e, ∀ y, y ∉ e”という文を満たすということの定義が、この文の中の∈をV上で定義されている∈であると解釈するならば、∃ e : V, ∀ x, x ∉ aになるということ。モデルの充足の話を外の話に持ってきたわけだ。
去年はこういうのを自動化したいといろいろがんばっていたわけで、形式証明ツヨツヨ勢はすぐにこんなふうにできちゃうんだなぁと感服したわけです。
さらに、空集合となるe : Vが存在するのだから、それを定数として確保したくなる。これもZ.leanに気づく前に自前で書いてみたのだけれども、Z.leanではこのように書いてある。
noncomputable scoped instance : EmptyCollection V := ⟨Classical.choose! empty_existsUnique⟩
@[simp] lemma IsEmpty.empty : IsEmpty (∅ : V) := Classical.choose!_spec empty_existsUnique
empty_existsUniqueは空集合がユニークに存在することを証明している補題。EmptyCollection VはVという型における∅がなんであるかを指定するものらしく、それが確かに空集合としての性質を持っているという補題がIsEmpty.empty。
ペア
次の定番は、ペアの公理を使ってシングルトンを作るやつである。ペアの公理に関しても、Z.leanでちゃんと整備されている。
noncomputable def doubleton (x y : V) : V := Classical.choose! (pairing_existsUnique x y)
@[simp] lemma mem_doubleton_iff {x y z : V} : z ∈ doubleton x y ↔ z = x ∨ z = y := Classical.choose!_spec (pairing_existsUnique x y) z
というわけで、シングルトンの存在も簡単に書ける。
example (x : V) : ∃ y : V, ∀ z : V, (z ∈ y ↔ z = x) := by
use doubleton x x
intro z
constructor
case h.mp =>
intro h
apply mem_doubleton_iff.mp at h
cases h <;> assumption
case h.mpr =>
intro h
rw [mem_doubleton_iff]
left; exact h
そうなんだけど、これもZ.leanでもっときれいにやってくれてます。
noncomputable def singleton (x : V) : V := doubleton x x
noncomputable scoped instance : Singleton V V := ⟨singleton⟩
lemma singleton_def (x : V) : ({x} : V) = doubleton x x := rfl
@[simp] lemma mem_singleton_iff {x z : V} : z ∈ ({x} : V) ↔ z = x := by simp [singleton_def]
ちょっと注意しないといけないのは、{x}だけだと"typeclass instance problem is stuck"と言われてしまうので、({x} : V)と型を指定しないといけない点。
和集合
次の定番は和集合の公理を使ってトリプルトンを作るやつである。和集合についてもすでにZ.leanに書いてある。
noncomputable def sUnion (x : V) : V := Classical.choose! (union_existsUnique x)
prefix:110 "⋃ˢ " => sUnion
lemma mem_sUnion_iff {x z : V} : z ∈ ⋃ˢ x ↔ ∃ y ∈ x, z ∈ y := Classical.choose!_spec (union_existsUnique x) z
これだけ整備されていればトリプルトンも一発で記述できるから楽ちんである。
example : ∀ a b c : V, ∃ x : V, ∀ y : V, y ∈ x ↔ y = a ∨ y = b ∨ y = c := by
intro a b c
use sUnion (doubleton (doubleton a b) (singleton c))
intro y
constructor
case h.mp =>
intro hy
apply mem_sUnion_iff.mp at hy
obtain ⟨x, hx1, hx2⟩ := hy
apply mem_doubleton_iff.mp at hx1
obtain hab | hc := hx1
case inl =>
rw [hab] at hx2
apply mem_doubleton_iff.mp at hx2
obtain hya | hyb := hx2
case inl =>
left; exact hya
case inr =>
right; left; exact hyb
case inr =>
rw [hc] at hx2
apply mem_singleton_iff.mp at hx2
right; right; exact hx2
case h.mpr =>
intro h
rw [mem_sUnion_iff]
obtain hya | hyb | hyc := h
case inl =>
use doubleton a b
simp only [mem_doubleton_iff, true_or, true_and]
left; exact hya
case inr.inl =>
use doubleton a b
simp only [mem_doubleton_iff, true_or, true_and]
right; exact hyb
case inr.inr =>
use singleton c
simp only [mem_doubleton_iff, or_true, true_and]
apply mem_singleton_iff.mpr hyc
手数はかかっているけど自然でしょう。
次回予告
このままZ.leanを読みながらいろいろな集合を作ったりして遊んでいこうかと。
