ZFC公理系统的形式化定义
本质是一个形式系统，因此，我们需要用形式系统的方式给出明确定义。关于形式系统的初步研究详见数理逻辑。
集合论语言
字符集
元定义1（公理集合论字符集）：
(1) 个体变元： $x,y,z,u,v,w,\cdots$
(2) 个体常元：
(3) $n$ 元函词：
(4) $n$ 元谓词： $\in$
(5) 否定联结词 $\neg$ ： $\neg$
(6) 蕴涵联结词 $\imp$ ： $\imp$
(7) 全称量词 $\forall$ ： $\forall$
(8) 辅助括号 $(,)$ ： $(,)$
(1) 个体变元： $x,y,z,u,v,w,\cdots$
(2) 个体常元：
(3) $n$ 元函词：
(4) $n$ 元谓词： $\in$
(5) 否定联结词 $\neg$ ： $\neg$
(6) 蕴涵联结词 $\imp$ ： $\imp$
(7) 全称量词 $\forall$ ： $\forall$
(8) 辅助括号 $(,)$ ： $(,)$
注意到原本的ZFC公理系统是没有常元和函词的，原子谓词也只有一个：$\in$ 。但是后续我们讲述如何通过保守扩充的方式引入新的常元、函词和谓词。
形成规则
元定义2（公理集合论的项）：
(1) 个体常元，个体变元是项。
(2) 若 $f^{(n)}$ 是一个 $n$ 元函词，且 $t_1,t_2,\cdots,t_n$ 为项，则 $f^{(n)}(t_1,t_2,\cdots,t_n)$ 是项。
(3) 由(1)(2)有限次复合产生的结果是项。
(1) 个体常元，个体变元是项。
(2) 若 $f^{(n)}$ 是一个 $n$ 元函词，且 $t_1,t_2,\cdots,t_n$ 为项，则 $f^{(n)}(t_1,t_2,\cdots,t_n)$ 是项。
(3) 由(1)(2)有限次复合产生的结果是项。
元定义3（公理集合论的公式）：
(1)原子谓词是公式。
(2)若 $A$ 为公式，则 $\neg A$ 也是公式。
(3)若 $A,B$ 为公式，且无变元 $x$ 在 $A,B$ 中一个是约束的，而在另一个是自由的，则 $A \imp B$ 均是公式。
(4)若 $A$ 是公式，而 $x$ 在 $A$ 中为自由变元，则 $\forall x A(x),\exists x A(x)$ 均是公式。
(5)由(1)~(4)有限次所复合所形成的公式均为公式。
(1)原子谓词是公式。
(2)若 $A$ 为公式，则 $\neg A$ 也是公式。
(3)若 $A,B$ 为公式，且无变元 $x$ 在 $A,B$ 中一个是约束的，而在另一个是自由的，则 $A \imp B$ 均是公式。
(4)若 $A$ 是公式，而 $x$ 在 $A$ 中为自由变元，则 $\forall x A(x),\exists x A(x)$ 均是公式。
(5)由(1)~(4)有限次所复合所形成的公式均为公式。
元定义4（公理集合论的基本形成规则）：下面的 $A,B$ 均为语法变元，可代表FC中的任意公式。
(1) 析取联结词 $\or$ ： $A \or B \strdefine \neg A \imp B$
(2) 合取联结词 $\and$ ： $A \and B \strdefine \neg(A \imp \neg B)$
(3) 等价联结词 $\iff$ ： $A \iff B \strdefine (A \imp B) \and (B \imp A)$
(4) 特称量词 $\exists$ ： $\exists x A \strdefine \neg\forall x \neg A$
(5) 否定特称量词 $\nexists$ ： $ \nexists \strdefine \neg\exists$
(6) $\neg$ 的堆叠： $\neg\neg\cdots\neg A \strdefine (\neg(\neg\cdots(\neg A)\cdots))$
(7) $\imp$ 的堆叠： $A_1 \imp A_2 \imp A_3 \imp \cdots \imp A_n \strdefine (A_1 \imp (A_2 \imp \cdots \imp (A_{n-1} \imp A_n) \cdots ))$
(8) $\or$ 的堆叠： $ A_1 \or A_2 \or A_3 \or \cdots \or A_n \strdefine (( \cdots ((A_1 \or A_2) \or A_3) \or \cdots )\or A_n)$
(9) $\and$ 的堆叠： $A_1 \and A_2 \and A_3 \and \cdots \and A_n \strdefine (( \cdots ((A_1 \and A_2) \and A_3) \and \cdots )\and A_n)$
(10) $\iff$ 的堆叠： $A_1 \iff A_2 \iff A_3 \iff \cdots \iff A_n \strdefine (A_1 \iff (A_2 \iff \cdots \iff (A_{n-1} \iff A_n) \cdots ))$
(11) $\forall$ 的堆叠： $\forall v_1 \forall v_2 \cdots \forall v_n A \strdefine (\forall v_1 (\forall v_2 \cdots (\forall v_n A)))$
(12) $\exists$ 的堆叠： $\exists v_1 \exists v_2 \cdots \exists v_n A \strdefine (\exists v_1 (\exists v_2 \cdots (\exists v_n A)))$
(13) $\neg,\forall,\exists$ 的堆叠： $\text{U}_1v_1\text{U}_2v_2 \cdots \text{U}_n v_n A \strdefine (\text{U}_1 v_1(\text{U}_2 v_2 \cdots (\text{U}_n v_n A) \cdots ))$ ，其中 $\text{U}_i$ 是 $\neg$ 、$\forall$ 或 $\exists$ 。
(14) 符号优先级： $\set{\neg,\forall,\exists} > \set{\and,\or} > \set{\imp} > \set{\iff}$ 。
(1) 析取联结词 $\or$ ： $A \or B \strdefine \neg A \imp B$
(2) 合取联结词 $\and$ ： $A \and B \strdefine \neg(A \imp \neg B)$
(3) 等价联结词 $\iff$ ： $A \iff B \strdefine (A \imp B) \and (B \imp A)$
(4) 特称量词 $\exists$ ： $\exists x A \strdefine \neg\forall x \neg A$
(5) 否定特称量词 $\nexists$ ： $ \nexists \strdefine \neg\exists$
(6) $\neg$ 的堆叠： $\neg\neg\cdots\neg A \strdefine (\neg(\neg\cdots(\neg A)\cdots))$
(7) $\imp$ 的堆叠： $A_1 \imp A_2 \imp A_3 \imp \cdots \imp A_n \strdefine (A_1 \imp (A_2 \imp \cdots \imp (A_{n-1} \imp A_n) \cdots ))$
(8) $\or$ 的堆叠： $ A_1 \or A_2 \or A_3 \or \cdots \or A_n \strdefine (( \cdots ((A_1 \or A_2) \or A_3) \or \cdots )\or A_n)$
(9) $\and$ 的堆叠： $A_1 \and A_2 \and A_3 \and \cdots \and A_n \strdefine (( \cdots ((A_1 \and A_2) \and A_3) \and \cdots )\and A_n)$
(10) $\iff$ 的堆叠： $A_1 \iff A_2 \iff A_3 \iff \cdots \iff A_n \strdefine (A_1 \iff (A_2 \iff \cdots \iff (A_{n-1} \iff A_n) \cdots ))$
(11) $\forall$ 的堆叠： $\forall v_1 \forall v_2 \cdots \forall v_n A \strdefine (\forall v_1 (\forall v_2 \cdots (\forall v_n A)))$
(12) $\exists$ 的堆叠： $\exists v_1 \exists v_2 \cdots \exists v_n A \strdefine (\exists v_1 (\exists v_2 \cdots (\exists v_n A)))$
(13) $\neg,\forall,\exists$ 的堆叠： $\text{U}_1v_1\text{U}_2v_2 \cdots \text{U}_n v_n A \strdefine (\text{U}_1 v_1(\text{U}_2 v_2 \cdots (\text{U}_n v_n A) \cdots ))$ ，其中 $\text{U}_i$ 是 $\neg$ 、$\forall$ 或 $\exists$ 。
(14) 符号优先级： $\set{\neg,\forall,\exists} > \set{\and,\or} > \set{\imp} > \set{\iff}$ 。
注：上面的使用正整数 $n$ 的表示并不是一个关于正整数 $n$ 的公式，它只是元语言层面的一个简写表示，所以不可使用集合论面的数学归纳法。同样，定义中出现的省略号仅表示一种字符串的模式匹配方法，$A_1,A_2,\cdots,A_n$ 只是一种单纯的符号区分，和集合论层面的关于正整数集的映射序列有本质区别。
元定义5（属于符号 $\in$ 的几种扩展）：
(1) 不属于谓词 $\notin$ ： $x \notin y \strdefine \neg (x \in y)$
(2) 包含于谓词 $\ni$ ： $x \ni y \strdefine y \in x$
(3) 不包含于谓词 $\notni$ ： $x \notni y \strdefine y \notin x$
(1) 不属于谓词 $\notin$ ： $x \notin y \strdefine \neg (x \in y)$
(2) 包含于谓词 $\ni$ ： $x \ni y \strdefine y \in x$
(3) 不包含于谓词 $\notni$ ： $x \notni y \strdefine y \notin x$
元定义6（量词的受限域）：
(1) $\forall$ 受限： $(\forall x \in y) A \strdefine \forall x ((x \in y) \imp A)$
(2) $\exists$ 受限： $(\exists x \in y) A \strdefine \exists x ((x \in y) \and A)$
(3) $\forall$ 受限堆叠： $(\forall x_1,x_2,\cdots,x_n \in y) A \strdefine (\forall x_1 \in y)(\forall x_2 \in y)\cdots(\forall x_n \in y) A$
(4) $\exists$ 受限堆叠： $(\exists x_1,x_2,\cdots,x_n \in y) A \strdefine (\exists x_1 \in y)(\exists x_2 \in y)\cdots(\exists x_n \in y) A$
(1) $\forall$ 受限： $(\forall x \in y) A \strdefine \forall x ((x \in y) \imp A)$
(2) $\exists$ 受限： $(\exists x \in y) A \strdefine \exists x ((x \in y) \and A)$
(3) $\forall$ 受限堆叠： $(\forall x_1,x_2,\cdots,x_n \in y) A \strdefine (\forall x_1 \in y)(\forall x_2 \in y)\cdots(\forall x_n \in y) A$
(4) $\exists$ 受限堆叠： $(\exists x_1,x_2,\cdots,x_n \in y) A \strdefine (\exists x_1 \in y)(\exists x_2 \in y)\cdots(\exists x_n \in y) A$
公理集合论系统的理论
逻辑公理
公理1（公理集合论的逻辑公理）：下列公理模式及其全称化均为公理。其中 $A,B,C$ 为语法变元，可代表ZFC中的任意公式，$x$ 为任意变元，$t$ 为任意项。
(1) A1： $A \imp (B \imp A)$
(2) A2： $(A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C))$
(3) A3： $(\neg A \imp \neg B) \imp (B \imp A)$
(4) A4： $\forall x A \imp A(x/y)$ （在 $A$ 上项 $y$ 对 $x$ 可代入）
(5) A5： $\forall x (A \imp B) \imp (\forall x A \imp \forall x B)$
(6) A6： $A \imp \forall x A$ （$x$ 在 $A$ 中无自由出现）
(1) A1： $A \imp (B \imp A)$
(2) A2： $(A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C))$
(3) A3： $(\neg A \imp \neg B) \imp (B \imp A)$
(4) A4： $\forall x A \imp A(x/y)$ （在 $A$ 上项 $y$ 对 $x$ 可代入）
(5) A5： $\forall x (A \imp B) \imp (\forall x A \imp \forall x B)$
(6) A6： $A \imp \forall x A$ （$x$ 在 $A$ 中无自由出现）
非逻辑公理
非逻辑公理将在后续讲述。实际上，不同的公理集合论系统正是采用了不同的非逻辑公理来区分，常见的公理集合论系统有ZF系统、ZFC系统、NBG系统等。我们主要研究ZFC系统，因为这是大多数现代数学的基石。
推理规则
规则1（FC的推理规则(分离规则)）：ZFC只有一个推理规则，即若有结论 $A$ 及 $A \imp B$ 成立，则必有结论 $B$ 成立，可用形式化推理序列表示为
$$\begin{aligned}
A,A \imp B,B
\tag{1}\end{aligned}$$
定理推导
定理推导是ZFC形式系统中的重要内容，包括所有的推理结论及推理过程。
元定义7（公理集合论的证明）：称下列公式序列为公式 $A$ 在FC中的一个证明
$$\begin{aligned}
A_1,A_2,\cdots,A_m(=A)
\tag{2}\end{aligned}$$
其中 $A_i(i=1,\cdots,m-1)$ 或为FC的公理，或为 $A_j(j < i)$ ，或为 $A_j,A_k(j,k < i)$ ，使用 $r_{mp}$ 导出的，而 $A_m$ 即为公式 $A$ 。
元定义8（公理集合论的定理）：如果公式 $A$ 在FC中有一个证明序列，则称 $A$ 为定理，记为 $\vdash_{ZFC} A$ ，或简记为 $\vdash A$ 。其中符号“ $\vdash$ ”表示其后的公式在FC中是可证明的。
元定义9（公理集合论的演绎）：设 $\Gamma$ 为FC中若干公式构成的公式集，称下列公式序列为公式 $A$ 以 $\Gamma$ 为前提的演绎，即
$$\begin{aligned}
A_1,A_2,\cdots,A_m(=A)
\tag{3}\end{aligned}$$
其中 $A_i$ 或为FC的公理，或为 $\Gamma$ 中的成员，或为 $A_j(j < i)$ ，或为 $A_j,A_k(0 < j,k < i)$ 使用 $r_{mp}$ 导出的，而 $A_m$ 即为公式 $A$ 。记为 $\Gamma \vdash_{FC} A$ 或简记为 $\Gamma \vdash A$ ，并称 $A$ 为 $\Gamma$ 的演绎结果。若 $\Gamma$ 中仅有一个成员，如 $\Gamma=\set{B}$ ，此时 $\Gamma \vdash A$ 即为 $B \vdash A$ ，表示公式 $A$ 可由前提 $B$ 在FC中演绎出来。若公式集 $\Gamma'$ 中的每一个公式都可以以 $\Gamma$ 为前提演绎出来，则记为 $\Gamma \vdash \Gamma'$ 。$\Gamma \cup \Gamma_1 \vdash \Gamma_2$ 也可以记为 $\Gamma \Vdash \set{\Gamma_1 \vdash \Gamma_2}$ 。
元定义10（演绎等价）：若公式 $A,B$ 有 $A \vdash B$ 且 $B \vdash A$ ，则称公式 $A,B$ 演绎等价，记为 $A \vdashv B$ 。若公式集 $\Gamma_1,\Gamma_2$ 有 $\Gamma_1 \vdash \Gamma_2$ 且 $\Gamma_2 \vdash \Gamma_1$ ，则称公式集 $\Gamma_1,\Gamma_2$ 演绎等价，记为 $\Gamma_1 \vdashv \Gamma_2$ 。若公式集 $\Gamma,\Gamma_1,\Gamma_2$ 有 $\Gamma \cup \Gamma_1 \vdash \Gamma_2,\Gamma \cup \Gamma_2 \vdash \Gamma_1$ ，则称公式集 $\Gamma_1,\Gamma_2$ 以 $\Gamma$ 为前提演绎等价，记为 $\Gamma \Vdash \Gamma_1 \vdashv \Gamma_2$ 。
ZFC理论的谓词保守扩充
由公理集合论字符集可以看出，初始的ZFC公理系统并没有常元和函词，只有一个二元谓词 $\in$ 。我们先来讲如何扩充谓词，后续我们会讲到如何扩充常元和函词。
元定义11（谓词保守扩充）：对任何一个彰显自由变元的公式 $\phi(x_1,x_2,\cdots,x_n)$ ，若希望将其命名成一个与原系统谓词符号不冲突的谓词 $P(x_1,x_2,\cdots,x_n)$ ，可以通过向系统中的谓词符号表添加 $P(x_1,x_2,\cdots,x_n)$ 并添加如下定义公理。
$$\begin{aligned}
\forall x_1 \forall x_2 \cdots \forall x_n (P(x_1,x_2,\cdots,x_n) \iff \phi(x_1,x_2,\cdots,x_n))
\tag{4}\end{aligned}$$
如果希望这个谓词在某个受限域或某个条件之下才能使用，也可以添加如下定义公理。
$$\begin{aligned} & (\forall x_1 \in X_1)(\forall x_2 \in X_2)\cdots(\forall x_n \in X_n)\\[5pt] &(\psi_1(x_1,x_2,\cdots,x_n) \imp \psi_2(x_1,x_2,\cdots,x_n) \cdots \imp \psi_m(x_1,x_2,\cdots,x_n) \\[5pt] &\imp (P(x_1,x_2,\cdots,x_n) \iff \phi(x_1,x_2,\cdots,x_n))) \tag{5}\end{aligned}$$其中 $\psi_1,\psi_2,\cdots,\psi_m$ 是任意彰显自由变元的公式，$x_1,x_2,\cdots,x_n$ 可以受限也可以不受限。
通过如下元定理我们可以看到，这样的扩充实际上并没有引入新的信息，扩充后的公理系统与扩充前的公理系统的理论是等价的。
元定理1（谓词保守扩充后的系统与原系统的理论等价）：假设 $L$ 是原本的公理集合论系统， $T$ 是 $L$ 的公理集；$L^*$ 是通过谓词保守扩充进行有限次谓词保守扩充后的公理系统，$T^*$ 是 $L^*$ 的公理集。对任意一个 $L^*$ 中的公式 $\psi^*$ ，存在一个翻译 $\psi^* \mapsto \psi$ 将 $\psi^*$ 翻译成 $L$ 中的公式 $\psi$ 。设 $\Gamma^*$ 是 $L^*$ 的任一公式集，$\Gamma$ 是将 $\Gamma^*$ 中所有公式翻译到 $L$ 后的公式集，若 $\Gamma^* \vdash_{L^*} \psi^*$ ，则 $\Gamma \vdash_{L} \psi$ 。
〔证明元定理1〕考虑添加一次谓词的情况。我们直接考虑式(5)的情形，式(4)的情形可以看做是其特殊情况。对任何一个 $L^*$ 中的公式 $\psi^*$ ，我们定义 $\psi$ 为 $\psi^*$ 中将所有的 $P(x_1,x_2,\cdots,x_n)$ 替换为 $\phi(x_1,x_2,\cdots,x_n)$ 的公式。〔元定理1证毕〕
任何一样东西，你渴望拥有它，它就盛开。一旦你拥有它，它就凋谢。― Marcel Proust, 《追忆似水年华》