3 その他の公理
3.1 自然数
先の4公理（ax_∅, ax_set2, ax_℘, ax_⋃）は初等的な集合を作り出しますが無限集合はできません。
von Neumannは自然数を \(n+1=n\cup\{n\}\) により作成しました。Matheliaでは自然数全体を次で作るのが自然です。
word(,s) …
\(\mathbb{M}\)𝕄. …
\(\mathbb{M} = \{ n \mid \forall M \, ( \emptyset \in M , \forall x \in M . x \cup \{ x \} \in M \Longrightarrow n \in M ) \}\) ax_∞ …
\(\exists M ( \emptyset \in M , \forall x \in M . x \cup \{ x \} \in M )\) \(\blacktriangleleft\) 𝕄.3.2 正則性公理(基礎の公理)
次の公理はvon Neumannによって導入されたものです。
ax0 …
\(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\) \(\mathbb{V}_0 = \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax03.3 置換公理
\(! x P\) で「Pを満たすxは高々1つ」を表します。
abbr …
\(! x P\) ≈
\(\forall y , z \in \{ x \mid P \} . y = z\) 置換公理は「関数的な性質による集合の像は集合である」ことを要請します。
ax_r …
\(\forall \mathbin{p} ( \forall x \, ! y \, x \mathbin{p} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{p} y \} )\) \(\mathbin{p}\) は2項の述語変数です。ZFの置換公理は ??p^ に入る式ごとに1つの公理（無限個の公理の集まり）で、ax_r は「すべての ??p^ について」とまとめて書いたものです。
Mathelia は ax_r を、??p^ に式を代入した実例としてだけ使います（ZF の公理図式と同じ働き）。
ax_r の ??p^ に式を代入するときは、ax_r の中の
x ??p^ y にならい、1番目の引数を x、2番目の引数を y と書きます。
分出公理はax_rから導かれます。??p^ に「x∈_C_ and y=x」を代入したインスタンスを使います。
ax_s
\(\blacktriangleleft\) ax_r1段目の 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\) となり ∅. に反するため）。
le_set2 …
\(\exists C \, \exists^* s , t ( s , t \in C )\) \(\blacktriangleleft\) \(\mathbb{W}.\)相異なる2元 s, t を持つ集合 C に対し、??p^ に「s を u へ、t を v へ送る」関係を代入すると、C の像は \(\{u, v\}\) です。対集合の定義 set2. は使っていません。
ax_set2
\(\blacktriangleleft\) ax_r ，le_set23.4 関数の像
word+(s,s→s,c) …
\(\text{^}\)lower …
\(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃
\(\{ \mathbin{{\sf f}} a \mid a \in A \}\) \(\stackrel{\text{^}}{{f}} X\) は X の ?f による像 \(\{?f(x) \mid x \in X\}\) です。置換公理から、関数の像は集合です。
ax_im …
\(\forall X \, \dot\exists ( \stackrel{\text{^}}{{f}} X )\) ax_im
\(\blacktriangleleft\) ax_r3.5 全域の関数的関係の置換公理
abbr …
\(\exists! x P\) ≈
\(\exists x P , ! x P\) ax_r の「高々1つ」(！) を「ちょうど1つ」(∃！) に変えたものが ax_rt です。ax_r は ax_rt と ax_∅ を合わせたものと同値です。
ax_rt …
\(\forall \mathbin{p} ( \forall x \, \exists! y \, x \mathbin{p} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{p} y \} )\) \(\forall x \, \exists! y \, x \mathbin{q} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{q} y \}\) \(\blacktriangleleft\) ax_r ax_s
\(\blacktriangleleft\) ax_rt ，ax_∅ \(\forall x \, ! y \, x \mathbin{q} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{q} y \}\) \(\blacktriangleleft\) ax_rt ，ax_∅ここまでで、Book を書いて査読する基本（word の紹介・prop・Thm と prf・backend・定義による展開）が揃いました。
実際の数学の本としては、まずは articles1 の本を見ることをお勧めします。