1 集合の存在について

1.1 無限公理

後続関数を準備しておきます。von Neumannは自然数を \(0 = \emptyset\) , \(1 = \emptyset \textit{+1}\) , … と作っていきました。
word(s,s) … \(\textit{+1}\)
suc. … \(n \textit{+1} = n \cup \{ n \}\)
先の4公理は初等的な集合を作り出しますが、無限集合は次の公理により初めて生まれます。
空集合公理 は 無限公理 から導出されます。ただし下の prf は ∅. も前提に使っているので（ax_∞ の式自体が ∅ を含む）、「無限公理だけから空集合の存在が出る」ことを示す例にはなっていません。
ax_∅ \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_∞

1.2 分出公理

集合の部分クラスは集合である、ことが要請されます。
ax_s … \(\exists X \, C \subset X \Longrightarrow \dot\exists C\)
宇宙も固有クラスになります(ax0からも導出されます)。
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) ax_s

ax_sはZFの分出公理と同値です。ZFは一階論理なので、分出公理は ?R^ をパラメータとする公理図式（無限個の公理の集まり）で、schema で書きます。
schema ax_s'(?R^;x;C_) := \(\forall X \dot\exists \{ x \in X \mid {R} ( x ) \}\)
\(\forall X \dot\exists \{ x \in X \mid {R} ( x ) \}\) \(\blacktriangleleft\) ax_s
ax_s \(\blacktriangleleft\) ax_s'

空集合公理 はax_sからも導出されます。
ax_∅ \(\blacktriangleleft\) ax_s

1.3 置換公理

置換公理は、関数的な性質による集合の像は集合である、ことを要請します。順序対は使いません。
abbr … \(! x P\) ≈ \(\forall y , z \in \{ x \mid P \} . y = z\)
abbr … \(\exists! x P\) ≈ \(\exists x P , ! x P\)
\(! y P\) は「Pを満たすyは高々1つ」です。 \(\forall x \, ! y \, x \mathbin{p} y\) は「??p^ は各xに高々1つのyを対応させる」ことを表します。
ZFの置換公理は\(\mathbin{p}\)をパラメータとする公理図式(無限個の公理の集まり)で、ax_rはその全体を表します。
schema の宣言は schema 名(述語変数;その引数の変数;共有変数) :=`ψ` の形です。ax_r では、??p^ が2項の述語変数、x,y はその1番目・2番目の引数の名前（代入する式の中で x が1番目、y が2番目を表します）、C_,s,t,u,v は代入する式の中に自由なまま残してよい変数（共有変数）です。共有変数に無い自由変数を代入する式に書くと、「代入式の自由な個体変数はラムダ引数か共有変数に含めてください」と拒否されます。

分出公理はax_rから導かれます。??p^ に「x∈_C_ and y=x」を代入したインスタンスを使います。
ax_s \(\blacktriangleleft\) ax_r
1段目の sos の ax_r[??p^:=`x ∈_ C_ and y = x`] は、ax_r の ??p^ に「x∈_C_ and y=x」を代入した実例です。代入した実例はこのように段の sos に直接書けます。最後の ax_s ◀ ax_r h; で「ax_r から導かれる」という形のThmにまとめます。代入する式に x と y の両方が現れる必要はありません（例えば ax_r[??p^:=`y = ∅`] で「X の各元を ∅ に送った像は集合」が示せます）。

対集合公理もax_rから導かれます。まず、相異なる2元を持つ集合があることを、空集合とべき集合だけから示します（ \(\wp ( \wp \emptyset )\) は \(\emptyset\) と \(\wp \emptyset\) を元に持ち、 \(\emptyset \in \wp \emptyset\) なので両者は異なります。等しいとすると \(\emptyset \in \emptyset\) となり ∅. に反するため）。
相異なる2元 s, t を持つ集合 C に対し、??p^ に「s を u へ、t を v へ送る」関係を代入すると、C の像は \(\{u, v\}\) です。対集合の定義 set2. は使っていません。
ax_set2 \(\blacktriangleleft\) ax_r ，le_set2