公理集合论系统的逻辑定理
由公理集合论的逻辑公理和分离规则可见公理集合论的逻辑基础是在命题逻辑演算形式系统和一阶谓词逻辑演算形式系统上扩展的，因此，我们根据命题逻辑演算形式系统和一阶谓词逻辑演算形式系统中的元定理和定理可以得到如下定理。
元定理
演绎定理
元定理1（演绎定理）：
(1) 对任意公式集 $\Gamma$ 和公式 $A,B$ ，有 $$\begin{aligned} \Gamma \cup \set{A} \vdash B \miff \Gamma \vdash A \imp B \tag{1}\end{aligned}$$
(1) 对任意公式集 $\Gamma$ 和公式 $A,B$ ，有 $$\begin{aligned} \Gamma \cup \set{A} \vdash B \miff \Gamma \vdash A \imp B \tag{1}\end{aligned}$$
(2) 对任意公式集 $\Gamma$ 和公式 $A_1,A_2,\cdots,A_n,B$ ，有
$$\begin{aligned} \Gamma \cup \set{A_1,A_2,\cdots,A_n} \vdash B \miff \Gamma \vdash A_1 \imp A_2 \imp \cdots \imp A_n \imp B \tag{2}\end{aligned}$$(3) 对任意公式集 $\Gamma$ 和公式 $A_1,A_2,\cdots,A_n,B$ ，有
$$\begin{aligned} \Gamma \cup \set{A_1,A_2,\cdots,A_n} \vdash B \miff \Gamma \vdash A_1 \and A_2 \cdots \and A_n \imp B \tag{3}\end{aligned}$$(4) 对任意公式集 $\Gamma$ 和公式 $A,B,C$ ，有
$$\begin{aligned} \Gamma \cup \set{A} \vdash B \imp C \miff \Gamma \vdash A \and B \imp C \tag{4}\end{aligned}$$(5) 对任意公式集 $\Gamma$ 和公式 $A_1,A_2,\cdots,A_n,B,C$ ，有
$$\begin{aligned} \Gamma \cup \set{A_1,A_2,\cdots,A_n} \vdash B \imp C \miff \Gamma \vdash A_1 \and A_2 \and \cdots \and A_n \and B \imp C \tag{5}\end{aligned}$$元规则
$\imp$ 消除
元规则1（ $\imp$ 消除）：对任意公式 $A,B$
$$\begin{aligned}
\set{A,A \imp B} \vdash B
\tag{6}\end{aligned}$$
命题逻辑
$\imp$ 部分
同一律
定理1（同一律）：对任意公式 $A$ ，$\boxed{A \imp A}$ 。
$\imp$ 传递
定理2（ $\imp$ 传递）：
#1 对任意公式 $A,B,C$ ，$\boxed{(A \imp B) \and (B \imp C) \imp (A \imp C)}$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n$ ，$\boxed{(A_1 \imp A_2) \and (A_2 \imp A_3) \and \cdots \and (A_{n-1} \imp A_n) \imp (A_1 \imp A_n)}$ 。
#1 对任意公式 $A,B,C$ ，$\boxed{(A \imp B) \and (B \imp C) \imp (A \imp C)}$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n$ ，$\boxed{(A_1 \imp A_2) \and (A_2 \imp A_3) \and \cdots \and (A_{n-1} \imp A_n) \imp (A_1 \imp A_n)}$ 。
$\imp$ 继位
定理3（ $\imp$ 继位）：
#1 对任意公式 $A,B,C,D$ ，$\boxed{(A \imp (B \imp C)) \imp ((C \imp D) \imp (A \imp (B \imp D)))}$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n,B,C$ $$\begin{aligned} \boxed{(A_1 \imp A_2 \imp \cdots \imp A_n \imp B) \imp ((B \imp C) \imp (A_1 \imp A_2 \imp \cdots \imp A_n \imp C))} \tag{7}\end{aligned}$$
#1 对任意公式 $A,B,C,D$ ，$\boxed{(A \imp (B \imp C)) \imp ((C \imp D) \imp (A \imp (B \imp D)))}$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n,B,C$ $$\begin{aligned} \boxed{(A_1 \imp A_2 \imp \cdots \imp A_n \imp B) \imp ((B \imp C) \imp (A_1 \imp A_2 \imp \cdots \imp A_n \imp C))} \tag{7}\end{aligned}$$
$\imp$ 左引入
定理4（ $\imp$ 左引入）：
#1 对任意公式 $A,B$ ，$\boxed{A \imp (B \imp A)}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ ，$\boxed{A \imp (B_1 \imp B_2 \imp \cdots \imp B_n \imp A)}$ 。
#1 对任意公式 $A,B$ ，$\boxed{A \imp (B \imp A)}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ ，$\boxed{A \imp (B_1 \imp B_2 \imp \cdots \imp B_n \imp A)}$ 。
$\imp$ 对 $\imp$ 左分配
定理5（ $\imp$ 对 $\imp$ 左分配）：
#1 对任意公式 $A,B,C$ ，$\boxed{(A \imp (B \imp C)) \iff ((A \imp B) \imp (A \imp C))}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ $$\begin{aligned} \boxed{(A \imp (B_1 \imp B_2 \imp \cdots \imp B_n)) \iff ((A \imp B_1) \imp (A \imp B_2) \imp \cdots \imp (A \imp B_n))} \tag{8}\end{aligned}$$
#1 对任意公式 $A,B,C$ ，$\boxed{(A \imp (B \imp C)) \iff ((A \imp B) \imp (A \imp C))}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ $$\begin{aligned} \boxed{(A \imp (B_1 \imp B_2 \imp \cdots \imp B_n)) \iff ((A \imp B_1) \imp (A \imp B_2) \imp \cdots \imp (A \imp B_n))} \tag{8}\end{aligned}$$
$\imp$ 对 $\imp$ 右插入
定理6（ $\imp$ 对 $\imp$ 右插入）：
#1 对任意公式 $A,B,C$ ，$\boxed{((A \imp B) \imp C) \imp ((A \imp C) \imp (B \imp C))}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ $$\begin{aligned} \boxed{((B_1 \imp B_2 \imp \cdots \imp B_n) \imp A) \imp ((B_1 \imp A) \imp (B_2 \imp A) \imp \cdots \imp (B_n \imp A))} \tag{9}\end{aligned}$$
#1 对任意公式 $A,B,C$ ，$\boxed{((A \imp B) \imp C) \imp ((A \imp C) \imp (B \imp C))}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ $$\begin{aligned} \boxed{((B_1 \imp B_2 \imp \cdots \imp B_n) \imp A) \imp ((B_1 \imp A) \imp (B_2 \imp A) \imp \cdots \imp (B_n \imp A))} \tag{9}\end{aligned}$$
$\imp$ 对 $\imp$ 左置换
定理7（ $\imp$ 对 $\imp$ 左置换）：
#1 对任意公式 $A,B,C$ ，$\boxed{(A \imp (B \imp C)) \iff (B \imp (A \imp C))}$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n,B$ $$\begin{aligned} \boxed{(A_1 \imp A_2 \imp \cdots \imp A_n \imp B) \iff (\text{ $A_1 \imp A_2 \imp \cdots \imp A_n \imp B$ 中 $A_1,A_2,\cdots,A_n$ 任意置换})} \tag{10}\end{aligned}$$
#1 对任意公式 $A,B,C$ ，$\boxed{(A \imp (B \imp C)) \iff (B \imp (A \imp C))}$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n,B$ $$\begin{aligned} \boxed{(A_1 \imp A_2 \imp \cdots \imp A_n \imp B) \iff (\text{ $A_1 \imp A_2 \imp \cdots \imp A_n \imp B$ 中 $A_1,A_2,\cdots,A_n$ 任意置换})} \tag{10}\end{aligned}$$
$\imp$ 对 $\imp$ 左引入
定理8（ $\imp$ 对 $\imp$ 左引入）：
#1 对任意公式 $A,B,C$ ，$\boxed{(B \imp C) \imp ((A \imp B) \imp (A \imp C))}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ $$\begin{aligned} \boxed{(B_1 \imp B_2 \imp \cdots \imp B_n) \imp ((A \imp B_1) \imp (A \imp B_2) \imp \cdots \imp (A \imp B_n))} \tag{11}\end{aligned}$$
#1 对任意公式 $A,B,C$ ，$\boxed{(B \imp C) \imp ((A \imp B) \imp (A \imp C))}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ $$\begin{aligned} \boxed{(B_1 \imp B_2 \imp \cdots \imp B_n) \imp ((A \imp B_1) \imp (A \imp B_2) \imp \cdots \imp (A \imp B_n))} \tag{11}\end{aligned}$$
$\imp$ 对 $\imp$ 右逆引入
定理9（ $\imp$ 对 $\imp$ 右逆引入）：对任意公式 $A,B,C$ ，$\boxed{(A \imp B) \imp ((B \imp C) \imp (A \imp C))}$ 。
$\imp$ 对 $\imp$ 左归一
定理10（ $\imp$ 对 $\imp$ 左归一）：
#1 对任意公式 $A,B$ ，$\boxed{(A \imp A \imp B) \iff (A \imp B)}$ 。
#2 对任意公式 $A,B$ ，$\boxed{(A \imp A \imp \cdots \imp A \imp B) \iff (A \imp B)}$ 。
#1 对任意公式 $A,B$ ，$\boxed{(A \imp A \imp B) \iff (A \imp B)}$ 。
#2 对任意公式 $A,B$ ，$\boxed{(A \imp A \imp \cdots \imp A \imp B) \iff (A \imp B)}$ 。
$\iff$ 部分
$\iff$ 等价式
定理11（ $\iff$ 等价式）：对任意公式 $A,B$ ，$\boxed{(A \iff B) \iff (A \imp B) \and (B \imp A)}$ 。
$\iff$ 自反
定理12（ $\iff$ 自反）：对任意公式 $A$ ，$\boxed{A \iff A}$ 。
$\iff$ 对称
定理13（ $\iff$ 对称）：对任意公式 $A,B$ ，$\boxed{(A \iff B) \imp (B \iff A)}$ 。
$\iff$ 传递
$\iff$ 替换
$\iff$ 分解
定理14（ $\iff$ 分解）：
(1) $\iff$ 正分解：对任意公式 $A,B$ ，$\boxed{(A \iff B) \imp (A \imp B)}$ 。
(2) $\iff$ 逆分解：对任意公式 $A,B$ ，$\boxed{(A \iff B) \imp (B \imp A)}$ 。
(1) $\iff$ 正分解：对任意公式 $A,B$ ，$\boxed{(A \iff B) \imp (A \imp B)}$ 。
(2) $\iff$ 逆分解：对任意公式 $A,B$ ，$\boxed{(A \iff B) \imp (B \imp A)}$ 。
$\iff$ 合成
定理15（ $\iff$ 合成）：对任意公式 $A,B$ ，$\boxed{(A \imp B) \and (B \imp A) \imp (A \iff B)}$ 。
$\iff$ 消除
定理16（ $\iff$ 消除）：
(1) $\iff$ 正消除：对任意公式 $A,B$ ，$\boxed{A \and (A \iff B) \imp B}$ 。
(2) $\iff$ 逆消除：对任意公式 $A,B$ ，$\boxed{B \and (A \iff B) \imp A}$ 。
(1) $\iff$ 正消除：对任意公式 $A,B$ ，$\boxed{A \and (A \iff B) \imp B}$ 。
(2) $\iff$ 逆消除：对任意公式 $A,B$ ，$\boxed{B \and (A \iff B) \imp A}$ 。
$\iff$ 结合
定理17（ $\iff$ 结合）：
#1 对任意公式 $A,B,C$ ，$\boxed{((A \iff B) \iff C) \iff (A \iff (B \iff C))}$ 。
#1 对任意公式 $A,B,C$ ，$\boxed{((A \iff B) \iff C) \iff (A \iff (B \iff C))}$ 。
$\iff$ 交换
定理18（ $\iff$ 交换）：
#1 对任意公式 $A,B$ ，$\boxed{(A \iff B) \iff (B \iff A)}$ 。
#1 对任意公式 $A,B$ ，$\boxed{(A \iff B) \iff (B \iff A)}$ 。
$\imp$ 对 $\iff$ 左分配
定理19（ $\imp$ 对 $\iff$ 左分配）：
#1 对任意公式 $A,B,C$ ，$\boxed{(A \imp (B \iff C)) \iff ((A \imp B) \iff (A \imp C))}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ $$\begin{aligned} \boxed{(A \imp (B_1 \iff B_2 \iff \cdots \iff B_n)) \iff ((A \imp B_1) \iff (A \imp B_2) \iff \cdots \iff (A \imp B_n))} \tag{12}\end{aligned}$$
#1 对任意公式 $A,B,C$ ，$\boxed{(A \imp (B \iff C)) \iff ((A \imp B) \iff (A \imp C))}$ 。
#2 对任意公式 $A,B_1,B_2,\cdots,B_n$ $$\begin{aligned} \boxed{(A \imp (B_1 \iff B_2 \iff \cdots \iff B_n)) \iff ((A \imp B_1) \iff (A \imp B_2) \iff \cdots \iff (A \imp B_n))} \tag{12}\end{aligned}$$
$\neg$ 部分
$\neg$ 引出
定理20（ $\neg$ 引出）：对任意公式 $A,B$ ，$\boxed{A \imp (\neg A \imp B)}$ 。
$\neg$ 消除
定理21（ $\neg$ 消除）：对任意公式 $A,B$ ，$\boxed{\neg A \imp (A \imp B)}$ 。
左 $\neg$ 置换
定理22（左 $\neg$ 置换）：对任意公式 $A,B$ ，$\boxed{(\neg A \imp B) \iff (\neg B \imp A)}$ 。
右 $\neg$ 置换
定理23（右 $\neg$ 置换）：对任意公式 $A,B$ ，$\boxed{(A \imp \neg B) \iff (B \imp \neg A)}$ 。
逆 $\neg$ 等价
定理24（逆 $\neg$ 等价）：对任意公式 $A,B$ ，$\boxed{(A \imp B) \iff (\neg B \imp \neg A)}$
左 $\neg$ 自蕴
定理25（左 $\neg$ 自蕴）：对任意公式 $A$ ，$\boxed{(\neg A \imp A) \imp A}$ 。
右 $\neg$ 蕴否
定理26（右 $\neg$ 蕴否）：对任意公式 $A$ ，$\boxed{(A \imp \neg A) \imp \neg A}$ 。
$\neg\neg$ 等价
定理27（ $\neg\neg$ 等价）：对任意公式 $A$ ，$\boxed{A \iff \neg\neg A}$ 。
$\and,\or$ 部分
排中律
定理28（排中律）：对任意公式 $A$ ，$\boxed{A \or \neg A}$ 。
矛盾律
定理29（矛盾律）：对任意公式 $A$ ，$\boxed{\neg (A \and \neg A)}$ 。
$\and$ 分解
定理30（ $\and$ 分解）：
#1 对任意公式 $A,B$ ，$\boxed{A \and B \imp A}$ 。
#2 对任意公式 $A,B$ ，$\boxed{A \and B \imp B}$ 。
#3 对任意公式 $A_1,A_2,\cdots,A_n$ 和自然数 $i(1 \le i \le n)$ ，$\boxed{A_1 \and A_2 \and \cdots \and A_n \imp A_i}$ 。
#1 对任意公式 $A,B$ ，$\boxed{A \and B \imp A}$ 。
#2 对任意公式 $A,B$ ，$\boxed{A \and B \imp B}$ 。
#3 对任意公式 $A_1,A_2,\cdots,A_n$ 和自然数 $i(1 \le i \le n)$ ，$\boxed{A_1 \and A_2 \and \cdots \and A_n \imp A_i}$ 。
$\and$ 合成
定理31（ $\and$ 合成）：
#1 对任意公式 $A,B$ ，$\boxed{A \and B \imp A \and B}$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n$ ，$\boxed{A_1 \and A_2 \and \cdots \and A_n \imp A_1 \and A_2 \and \cdots \and A_n}$ 。
#1 对任意公式 $A,B$ ，$\boxed{A \and B \imp A \and B}$ 。
#2 对任意公式 $A_1,A_2,\cdots,A_n$ ，$\boxed{A_1 \and A_2 \and \cdots \and A_n \imp A_1 \and A_2 \and \cdots \and A_n}$ 。
$\or$ 附加
定理32（ $\or$ 附加）：
#1 对任意公式 $A,B$ ，$\boxed{A \imp A \or B}$ 。
#2 对任意公式 $A,B$ ，$\boxed{B \imp A \or B}$ 。
#3 对任意公式 $A_1,A_2,\cdots,A_n$ 和自然数 $i(1 \le i \le n)$ ，$\boxed{A_i \imp A_1 \or A_2 \or \cdots \or A_n}$ 。
#1 对任意公式 $A,B$ ，$\boxed{A \imp A \or B}$ 。
#2 对任意公式 $A,B$ ，$\boxed{B \imp A \or B}$ 。
#3 对任意公式 $A_1,A_2,\cdots,A_n$ 和自然数 $i(1 \le i \le n)$ ，$\boxed{A_i \imp A_1 \or A_2 \or \cdots \or A_n}$ 。
一阶谓词逻辑
限域
推广运算律
任何一样东西，你渴望拥有它，它就盛开。一旦你拥有它，它就凋谢。― Marcel Proust, 《追忆似水年华》