近況報告

分出公理

なんかすごい勢いで更新していたのが止まったのでどうしたのだろうと思っている人もいるかもしれない。いや、お勉強というかプロジェクトは一生懸命やっているのだけれども、ブログを書いているのは妻に見られたくないので、隠れてやれるタイミングがないと更新できない。 というのに加えて、相変わらずFin.snocに苦しめられつつも、和集合、無限、べき集合、正則性はひとまずできているんだけれども、分出公理のところで問題が発覚した。これまでのcastUpの仕組みでは十分な対応ができず、Fin n→V型の関数の真ん中を開けて値をぶちこめないとまずい。例えば、∀v ∀w ∃x ∀y(y∈x↔y∈w∧φ(v, w, y))みたいな論理式を考え、さらにφのなかでも量化子が使われているとする。全称量化子が一つ前についた分出公理の一つである。 これが成り立っているときにwになんか項tを代入したいとする。∀wが消えて∀v ∃x ∀y(y∈x↔y∈t∧φ(v, w, y))になる。ところが、Mathlib.ModelTheoryはde Brujin indexを採用しているのでx以降の量化子のインデックスがずれる。手書きの部分は修正するとしてもφの中身はいちいち変更したくない。 というわけで、この状況でvのインデックスは変わらないけれどもx以降の量化子のインデックスは下げられる仕組みを作りたい。方針としては逆で、∀y(y∈x↔y∈w∧φ(v, w, y))のwとxを項t1、t2に置き換えた論理式∀y(y∈t2↔y∈t1∧φ(v, t1, y))をwとxの量化を無視してt1とt2の関数として表現して、量化子が挿入されなければそのまま、量化子が挿入されたらそれより大きいインデックスをもっている量化をその分ずらしてやるようにしたい。これまであった仕組みはインデックスが大きいところに新しい量化を付け加えるもので、それだけでは対応できない。上記の例だとvのインデックスは変わらないので。 というわけで、そういうのを書いている。あとついでに言うと、分出公理のときに変数が自由であるかを判定しないといけないのでそれもある。そしてこれが終わったら多分それ以前のも書き換えることになるので、ブログに書くのを躊躇しているのである。

まあ頑張ってますよということで。