関係を表す論理式 すでに書いた通り、関係を表す論理式は自由変数をプレイスホルダーとして記述することにする。 例えば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_*…