2 NBG

集合論の公理系についてはNBG(von Neumann-Bernays-Gödel)も有名です。
Bernaysは2ソート論理で、Gödelはクラスの導入で、形式化をしました。default.formel の言語（s-Form と c-Form）は、そのどちらにも自然な翻訳があります。

NBGの公理は、補題として準備されます。まず2つ。
NBG-B2 … \(\exists X \forall x \, ( x \in X \Longleftrightarrow x \in A , x \in B )\)
\(\forall x \, ( x \in \{ y \mid y \in A , y \in B \} \Leftrightarrow ( x \in A , x \in B ) )\) \(\blacktriangleleft\) O
NBG-B3 … \(\exists X \forall x \, ( x \in X \Longleftrightarrow x \notin A )\)
\(\forall x \, ( x \in \{ y \mid y \notin A \} \Leftrightarrow x \notin A )\) \(\blacktriangleleft\) O

3 集合のwordを含んだ公理

word(ss,p) … \(\in\)
word(ss,s)F … \(\mathsf{pr}\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
NBG-B1 … \(\forall x \, \forall y \, ( \langle x , y \rangle \in \{ w \mid \exists u \, \exists v \, ( w = \langle u , v \rangle , u \in v ) \} \Leftrightarrow \exists u \, \exists v \, ( \langle x , y \rangle = \langle u , v \rangle , u \in v ) )\)
NBG-B1 \(\blacktriangleleft\) O

NBG-B4 … \(\exists X \forall x \, ( x \in X \Longleftrightarrow \exists z \, ( \langle x , z \rangle \in A ) )\)
\(\forall x \, ( x \in \{ y \mid \exists z \, ( \langle y , z \rangle \in A ) \} \Leftrightarrow \exists z \, ( \langle x , z \rangle \in A ) )\) \(\blacktriangleleft\) O