はじめに
最初に述べておかなくてはならないのは、このサイトの製作者（算散士）は、 型理論をあまりよく知らない とうことである。そもそも、Coqをいじることを決心するまで型理論がどんなものかもよく知らなかった（今もあまり知らない）。従って、型理論に基づいているCoqに対しても、深い理解をしているとは言いがたい。というより、理解はとても浅い。 Coqのようなコンピュータソフトをどうしてもいじりたくなったのは次の理由からである。
コンピュータソフトでしたかったのは、自分で書いた形式的証明の検証なので、本当に適しているのは定理の証明を支援するCoqよりも、まさに定理の証明を検証してくれるMizarの方なのかもしれない。しかし、Mizarの方は使い方がよくわからなかったのである。まあ、Coqだっていまだに使い方をよく知ってるとは言えないが、Coqはリファレンスマニュアルやチュートリアルが Coqのページ においてある。それでCoqを使うことにしたのである。Coq上で証明を完了することができれば、少しは証明の検証になるだろうと思ったのである。また、上記の１．はCoqを使えば自動的にできるわけではない（と思う）。が、それは証明のファイルを細かくし、定理の証明に使用しない定理や公理のファイルを参照しないようにすることで解決した（と思っている）。そうすることによって、Checkコマンドで公理を呼び出してみれば、使用していない公理を呼び出したときは「そんなものないよ」とCoqに叱られる、という寸法である。
いいわけ
そもそもは、集合論（ZFC）を形式言語（1階の述語論理）で書き下そうということから始まった。最初のうちは、証明の検証ソフトや証明の支援ソフトのようなものに手を出すつもりはまったくなかった。というより、（寄り道を嫌って）絶対手を出さないようにしようと思っていた。しかし、上記の１．をやろうとすると、どうしても機械的に処理したくなる。そしてふと気がつくと、ない知恵を絞って WSH(Windows Script Host)やLispに手を出して、自分の集合論のノートを処理するプログラムを書こうとしている自分がいたのである。どうせ時間をかけるなら、既存のソフトをつかったほうがいいに決まってる。ということで、Coqに手を出した。
はじめに２
上記の「はじめに」から月日がたち、今度こそ集合論を形式言語で書き下し始めた。 上記の１．に関しては、極力公理をAxiomとして宣言せずに、公理に名前をつけて、Theoremで証明する論理式の前件に全て含めることにしてしまった。また、直観主義論理をする気はないのだが、排中律を使用せずにどこまで行けるのか試してみたところ、排中律が証明 できるところまで行ってしまったので、排中律が証明できるまでは、排中律はAxiomとして宣言していない。ちなみに証明は、竹内外史著「直観主義的集合論」（紀伊國屋書店）のp.45（第2章直観主義的集合論§２直観主義的集合論の体系の無限の公理の後ろあたり）にある論法である。ここでは直観主義をする気がないので、上記竹内の本に出てくる 述語Eにあたるものは出てこない。また、Coqの表現力の強さに誘惑されて、少なくとも表記上は1階述語論理の範囲を超えてしまっている。が、Coqを利用する目的は、そういう範囲にこだわることではないので、気にしないことにした。