以下, 「(言語$L$で)成り立つ」とは一階述語論理と言語$L$を用いて証明できることをいう.
集合の言語$L_{ZFC}$は変数記号とアリティ$2$の関係記号$\in, =$をもち, 関数記号をもたない.
$L_{ZFC}$の変数記号を集合という.
$x, y$を集合とするとき, $\neg(x \in y)$を$x \notin y$, $\neg(x = y)$を$x \neq y$と略記する.
$\forall x \forall y$のように$\forall$が続く場合, $\forall x, y$のような略記を用いる.$\exists $に対しては混乱のもととなるため, この記法は用いない.
$x, X$を集合, $\psi(x)$を$L_{ZFC}$-論理式とする.
(1) $\forall x [x \in X \Rightarrow \psi(x)]$を$\forall x \in X [\psi(x)]$と略記する.
(2) $\exists x [x \in X \land \psi(x)]$を$\exists x \in X [\psi(x)]$と略記する.
以下において,
(1) ある記法$P$を$L_{ZFC}$-論理式$\psi$により定義するとき, $P :\Leftrightarrow \psi$と表す.
(2) ある集合$X$を$Y$という既知の集合によって定義するとき, $X \coloneqq Y$と表す.
$x, y$を集合とする.
$x \subset y :\Leftrightarrow \forall z [z \in x \Rightarrow z \in y]$と定め, このとき$x$は$y$の部分集合であるという.
$\forall x, y [x \subset y \land y \subset x \Rightarrow x = y]$という外延性公理を導入する.下記の公理において存在が保証される集合が$=$であるかどうかを除いてただひとつであることを主張するために有用である.
$\forall x, y \exists z \forall a [a \in z \Leftrightarrow (a = x \vee a = y)]$という対の公理を導入する.
この公理で存在が保証される集合$z$は$x, y$のみに依存する.
$\{x, y\}$と表し, $\{x, x\}$を特に$\{x\}$と略記する.
$\forall x \exists y \forall z [z \in y \Leftrightarrow \exists a \in x [z \in a]]$という和集合の公理を導入する.
この公理で存在が保証される集合$y$は$x$のみに依存する.
$\bigcup x$と表し, $x$のunionという.$\bigcup x, y$を特に$x \cup y$と略記し, $x$と$y$の和集合とよぶ.
対の公理と和集合の公理を合わせることで, $\{x, y, z\} = \{x, y\} \cup \{z\}$のような集合が得られる.このような記法を外延的記法という.
$\forall x \exists y \forall a [a \in y \Leftrightarrow a \subset x]$というベキ集合の公理を導入する.
この公理で存在が保証される集合は$x$のみに依存する.
$2^x$または$\mathcal{P}(x)$と表し, $x$のベキ集合という.
$n$をメタ自然数とし, $\psi$を$n+2$個の自由変数をもち$y$を自由変数にもたない$L_{ZFC}$-論理式とする.
$\forall x, t_1, \dots, t_n\exists y \forall z [z \in y \Leftrightarrow (z \in x) \land \psi(x, z, t_1, \dots, t_n)]$という分出公理を導入する.
この公理で存在が保証される集合$y$は$x, t_1, \dots, t_n$のみに依存する.
$\{z \in x \mid \psi(x, z, t_1, \dots, t_n)\}$と表す.このような記法を内包的記法という.
$n$をメタ自然数とし, $\psi$を$n+3$個の自由変数をもつ$L_{ZFC}$-論理式とする.
$\forall X, t_1, \dots, t_n [\forall x \in X \exists! y [\psi(x, y, X, t_1, \dots, t_n)]\Rightarrow \exists Y\forall z[z \in Y \Leftrightarrow \exists a \in X [\psi(a, z, X, t_1, \dots, t_n)]]]$
という置換公理を導入する.
$\exists x [\exists a \in x [\forall b \in a [\bot]] \land \forall y \in x [y \cup \{y\} \in x]]$という無限公理を導入する.
この公理で存在が保証される集合$x$をこの資料では$\infty_1$と表すことにする.
$\forall x [\forall a \in x [\bot] \vee \exists y \in x \forall z [z \notin x \vee z \notin y]]$という正則性公理を導入する.
以上の公理をZFとよぶ.
$\exists x [\forall y \in x [\bot]]$が成り立つ.
この命題で存在がいえる集合$x$は$=$による区別を除きただひとつである.$\varnothing$と略記する.
存在性を主張する場合, ひとつ論理式をみたす集合をとれれば, $\exists E$規則を用いることで主張が従う.
$x = \{a \in \infty_1 \mid \bot\}$を考えると, 分出公理の主張から$\forall y \in x [\bot]$がいえる.
集合$a$に対し, $\forall b \in a[\bot]$が導けたとき, $b \in a \Leftrightarrow \bot \Leftrightarrow b \in x$により外延性公理から$a = x$が導ける.
$x, X$を集合, $\psi(x)$を$L_{ZFC}$-論理式とする.以下が成り立つ.
(1) $\neg(\forall x \in X [\psi(x)]) \Leftrightarrow \exists x \in X [\neg\psi(x)]$
(2) $\neg(\exists x \in X [\psi(x)]) \Leftrightarrow \forall x \in X [\neg\psi(x)]$