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