ZFの公理 公理は全部書けたと思ったら選択公理忘れてた。でもとにかく書けた+テストケースになりそうなことを一つずつはやったので満足。というわけで、ひとまず公開した。 https://github.com/ishiut/fo_zfc 一応、最低限のドキュメントは書いたつもりなの…

関係を表す論理式 すでに書いた通り、関係を表す論理式は自由変数をプレイスホルダーとして記述することにする。 例えばv2はv1のシングルトンであるというのはこのように書ける。 def intIsSingleton : LZFC.BoundedFormula ℕ 0:= ∀'((bv 1 0) ∈' fv 1 1⇔ (b…

replaceFVの定義 次回予告では違うこと書いたのだけれども、それの前にもう1ステップ必要になる。(tsN : ℕ → (L.Term (ℕ ⊕ Fin n)))が与えられているときにfvN n kをtsN kに置き換える関数を作りたい。 名前はreplaceFVとする。関数なのでlowerCamelCaseで、…

Fin.snocの件がようやく落ち着いてきた とりあえずFin.snocの件はこれでほとんど問題ないはず。 import Mathlib.Data.Set.Basic import Mathlib.Data.Fin.Tuple.Basic universe u namespace VSnoc variable {V: Type u} /-- Fin.snoc for the type V-/ def V…

報告 ちょっとまだ乱雑なのでエントリは書けないんだけど、とにかく置換公理ができた。というクラス関数による集合Aが集合であることは証明できたので、多分大丈夫だと思う。思いつくハマった点を書いていく。 クラス関数というか論理式による関数の表現を、…

分出公理 なんかすごい勢いで更新していたのが止まったのでどうしたのだろうと思っている人もいるかもしれない。いや、お勉強というかプロジェクトは一生懸命やっているのだけれども、ブログを書いているのは妻に見られたくないので、隠れてやれるタイミング…

前回: 空集合の存在するモデル書き直し - kururu_goedel’s diary realize_or、realize_and 前回書いた通り、できる限りsimpでモデルの充足を外側での命題に書き換えられるようにしたい。というわけで、orとandをrealizeするための定理を作る。いや、realize_…

前回: 空集合の公理が成り立つクラス - kururu_goedel’s diary 大幅書き直し 対集合の公理をやろうと思っていたのだけれども、simpタクティクで論理式のモデルによる充足から外側での記述に変換できるようになっていることに気がついた。具体的にはrealize_*…

前回: 文字列変換ニューバージョン - kururu_goedel’s diary 型クラス 予告通り、集合論の公理を満たす型クラスを定義していく。 いやー、ハマったハマった。思ったより型クラスのところでは苦労しなかったのだけれども、証明がなかなか通らず通ってもグチャ…

前回: これまでのまとめ＋ちょっと書き直し - kururu_goedel’s diary 項 自由変数のインデックスの型をαという型変数に変更したので文字列変換もそれに応じて直さないといけない。 αという型が文字列変換できるかは定かでないのだけれども、それはToStringと…

前回: 文字列変換 - kururu_goedel’s diary これまでのまとめ これまで定義したものをまとめてみた。それに際して、いくつか変更した。 universe変数uとvを定義して、それぞれ構造のユニバースと自由変数のインデックスの型にあてた ユニバースの型はvariabl…

前回: キャスト - kururu_goedel’s diary 文字列変換 特に命題が複雑になってきたときには、(Leanの)変数に格納されている論理式を表示してチェックしたい。そのような機構はMathlib.ModelTheoryにはない。本格的に公理化された集合論のモデルをやり始める前…

前回: andとorと中置演算子 - kururu_goedel’s diary キャスト 自分で書いてないとわかりにくいけど、BoundedFormula α nのn、すなわち未束縛変数の数がなかなか面倒である。面倒なだけではなく本質的でない。しかも、下記のような問題が起きうる。 項を受け…

前回: 存在量化子 - kururu_goedel’s diary andとor なんか前回安請負しておいて、andとかorがどうやって定義されているか知らなかった。orは⊔(\supで出る)、andは⊓(\inf)という中置演算子で定義されている。命題論理はこんな感じになる。 def ϕtop := ϕbot.…

前回: 全称量化子 - kururu_goedel’s diary 等号 すでに書いた通り、BoundedFormulaの定義にあるのはallだけで存在量化子に対応するものはない。それでも存在量化子を付け加えるのに対応する、BoundedFormula.exという関数が用意されており、定義はこう。 @[…

前回: 二項関係 - kururu_goedel’s diary 等号 全称量化子、すなわち∀を付け加えるBoundedFormula.allは下記の型を持つ。L.BoundedFormula α (n+1)の元を受け取ってL.BoundedFormula α nの元を返す。最終的に束縛される変数（さすがに面倒なので「未束縛変数…

前回: 構造の定義 - kururu_goedel’s diary 二項関係 論理式の定義 次回予告どおりに関係とその充足について。BoundedFormulaの定義を再掲。 /-- `BoundedFormula α n` is the type of formulas with free variables indexed by `α` and up to `n` additiona…

構造 定義 ここまでの定義はだいたい残っている状態からスタートするとする。 構造のユニバースになる型が必要で、とかでもいいんだけど、区別をつけたいので新しい型Vを定義。ただ自然数でインデックスしているだけ。 inductive V : Type | obj (n : Nat) :…

前回: Mathlib.ModelTheory事始め - kururu_goedel’s diary 論理式 項はできたんで次は論理式。定義はMathlib.ModelTheory.Syntaxにある。 /-- `Formula α` is the type of formulas with all free variables indexed by `α`. -/ abbrev Formula := L.Bounde…

イントロダクション 昔からずっと言っている、集合論における初等部分モデルや初等埋め込みを使った議論を証明支援系でやりたいというやつ、プロポーザル書いちゃったし（通るかどうかはわからないけど）、とりあえず開始しようと思う。使うのはLean。正直、…