User:CaffeineP/笔记/集合论——对无穷概念的探索 (郝兆宽、杨跃)

集合论^w，集合^w，无穷^w

第一章 集合与公理

1.3 公理^w：ZFC公理系统^w

存在公理 0（Exi）

${\underset {x}{\exists }}\,{\mathit {true}}$

外延公理^w 1（Ext）：元素^w决定集合

${\underset {X,\,Y}{\forall }}\color {CadetBlue}\left(\color {black}{\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in X\Leftrightarrow u\in Y{\color {CadetBlue})}{\begin{aligned}\,{\overset {\text{axiom}}{\Longrightarrow }}\\{\underset {\text{logic}}{\Longleftarrow }}\,\end{aligned}}X=Y\right)$

1.3.1. 练习：外延公理在 (N,<) 中成立

${\underset {a\in \mathbb {N} ,\,b\in \mathbb {N} }{\forall }}\color {CadetBlue}\left(\color {black}{\underset {n\in \mathbb {N} }{\forall }}\,{\color {CadetBlue}(}n<a\Leftrightarrow n<b{\color {CadetBlue})}\Leftrightarrow a=b\right)$

分离公理模式^w 2（Sep）

唯一性使用：外延公理

${\underset {X}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}{\mathit {true}}&\Leftrightarrow {\underset {Y}{\exists }}\ {\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in Y\Leftrightarrow u\in X\land \varphi (u){\color {CadetBlue})}\land {\underset {Y_{1},\,Y_{2}}{\forall }}\color {CadetBlue}\left(\color {black}{\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in Y_{1}\Leftrightarrow u\in X\land \varphi (u)\Leftrightarrow u\in Y_{2}{\color {CadetBlue})}\Rightarrow Y_{1}=Y_{2}\right)\\&\Rightarrow {\underset {Y}{\exists !}}\color {CadetBlue}\left(\color {black}{\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in Y\Leftrightarrow u\in X\land \varphi (u){\color {CadetBlue})},\,Y=:\{u\in X|\varphi (u)\}\right)\end{aligned}}\right)$

避免罗素悖论^w；所有集合的集合不存在

${\boldsymbol {R}}:=\{x|x\notin x\},\ {\boldsymbol {R}}\in \mathbf {V} \Rightarrow {\color {CadetBlue}(}{\boldsymbol {R}}\in {\boldsymbol {R}}\Leftrightarrow {\boldsymbol {R}}\notin {\boldsymbol {R}}{\color {CadetBlue})}\Leftrightarrow {\mathit {false}}$

${\mathit {true}}\Rightarrow {\underset {X}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}R_{X}:=\{x\in X|x\notin x\},\,{\mathit {true}}&\Leftrightarrow {\color {CadetBlue}(}R_{X}\in R_{X}\Leftrightarrow R_{X}\in R_{X}\land R_{X}\notin R_{X}\Leftrightarrow {\mathit {false}}{\color {CadetBlue})}\\&\Rightarrow R_{X}\notin R_{X}\Leftrightarrow R_{X}\notin X\lor R_{X}\in R_{X}\Leftrightarrow R_{X}\notin X\end{aligned}}\right)\color {black}\Rightarrow {\underset {X}{\nexists }}\ {\underset {Y}{\forall }}\ Y\in X$

1.3.2. 空集^w的定义

使用：分离公理模式

$\varnothing :=\{x|{\mathit {false}}\},\ {\underset {X}{\forall }}\,\varnothing =\{x\in X|{\mathit {false}}\},\ {\underset {x}{\forall }}\,x\notin \varnothing$

1.3.3. 练习：空集唯一

使用：外延公理

${\underset {X}{\forall }}\,\varnothing _{X}:=\{x\in X|{\mathit {false}}\},\ {\underset {A,\,B}{\forall }}\color {CadetBlue}\left(\color {black}{\mathit {true}}\Leftrightarrow {\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in \varnothing _{A}\Leftrightarrow {\mathit {false}}\Leftrightarrow u\in \varnothing _{B}{\color {CadetBlue})}\Rightarrow \varnothing _{A}=\varnothing _{B}\right)$

1.3.5. 注：所有集合的类

$\mathbf {V} :=\{x|{\mathit {true}}\},\ {\underset {x}{\forall }}\,x\in \mathbf {V}$

${\boldsymbol {R}}=\{x|x\notin x\}\notin \mathbf {V}$

1.3.6. 交集^w、差集^w和任意交^w的定义

使用：分离公理模式

${\underset {X,\,Y}{\forall }}{\color {CadetBlue}(}X\cap Y:=\{u\in X|u\in Y\},\,X-Y:=\{u\in X|u\notin Y\}\color {CadetBlue})$

${\underset {X\neq \varnothing }{\forall }}\color {CadetBlue}\left(\color {black}\bigcap X:=\left\{u{\bigg |}{\underset {Y\in X}{\forall }}u\in Y\right\},\,{\underset {z\in X}{\forall }}\bigcap X=\left\{u\in z{\bigg |}{\underset {Y\in X}{\forall }}u\in Y\right\}\right)$

对集公理^w 3（Pai）；单点集

唯一性使用：外延公理

${\underset {a,\,b}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}{\mathit {true}}&\Leftrightarrow {\underset {c}{\exists }}\ {\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in c\Leftrightarrow x=a\lor x=b{\color {CadetBlue})}\land {\underset {c_{1},\,c_{2}}{\forall }}\color {CadetBlue}\left(\color {black}{\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in c_{1}\Leftrightarrow x=a\lor x=b\Leftrightarrow x\in c_{2}{\color {CadetBlue})}\Rightarrow c_{1}=c_{2}\right)\\&\Rightarrow {\underset {c}{\exists !}}\color {CadetBlue}\left(\color {black}{\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in c\Leftrightarrow x=a\lor x=b{\color {CadetBlue})},\,c=:\{a,b\}\right)\end{aligned}}\right)$

${\underset {a}{\forall }}\color {CadetBlue}\left(\color {black}\{a\}:=\{a,a\},\,{\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in \{a\}\Leftrightarrow x=a\color {CadetBlue})\right)$

并集^w公理^w 4（Uni）

唯一性使用：外延公理

${\underset {X}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}{\mathit {true}}&\Leftrightarrow {\underset {Y}{\exists }}\ {\underset {u}{\forall }}\color {CadetBlue}\left(\color {black}u\in Y\Leftrightarrow {\underset {z\in X}{\exists }}u\in z\right){\color {black}\land {\underset {Y_{1},\,Y_{2}}{\forall }}}\left(\color {black}{\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in Y_{1}\Leftrightarrow {\underset {z\in X}{\exists }}u\in z\Leftrightarrow u\in Y_{2}{\color {CadetBlue})}\Rightarrow Y_{1}=Y_{2}\right)\\&\Rightarrow {\underset {Y}{\exists !}}\color {CadetBlue}\left({\color {black}{\underset {u}{\forall }}}\left(\color {black}u\in Y\Leftrightarrow {\underset {z\in X}{\exists }}u\in z\right)\color {black},\,Y=:\bigcup X\right)\end{aligned}}\right)$

${\underset {X,\,Y}{\forall }}X\cup Y:=\bigcup \{X,Y\}=\{u|u\in X\lor u\in Y\}$

1.3.8. 子集^w和真子集的定义

${\underset {X,\,Y}{\forall }}\color {CadetBlue}\left(\color {black}X\subseteq Y:\Leftrightarrow {\underset {u\in X}{\forall }}u\in Y,\ X\subset Y:\Leftrightarrow X\subseteq Y\land X\neq Y\right)$

1.3.9. 练习：空集是任何集合的子集

${\underset {X}{\forall }}\color {CadetBlue}\left(\color {black}{\mathit {true}}\Leftrightarrow {\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in \varnothing \Rightarrow u\in X{\color {CadetBlue})}\Leftrightarrow \varnothing \subseteq X\right)$

幂集^w公理^w 5（Pow）

唯一性使用：外延公理

${\underset {X}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}{\mathit {true}}&\Leftrightarrow {\underset {Y}{\exists }}\ {\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in Y\Leftrightarrow u\subseteq X{\color {CadetBlue})}\land {\underset {Y_{1},\,Y_{2}}{\forall }}\color {CadetBlue}\left(\color {black}{\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in Y_{1}\Leftrightarrow u\subseteq X\Leftrightarrow u\in Y_{2}{\color {CadetBlue})}\Rightarrow Y_{1}=Y_{2}\right)\\&\Rightarrow {\underset {X}{\forall }}\ {\underset {Y}{\exists !}}\color {CadetBlue}\left(\color {black}{\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in Y\Leftrightarrow u\subseteq X{\color {CadetBlue})},\,Y=:{\mathcal {P}}(X)\right)\end{aligned}}\right)$

1.3.10. 后继^w的定义；自然数^w

使用：单点集，并集，空集

${\underset {x}{\forall }}\,S(x)=x^{+}:=x\cup \{x\}$

${\begin{alignedat}{4}&0:=&&\varnothing &&=\{\}&&\\&1:=0^{+}=\,&&\varnothing \cup \{\varnothing \}&&=\{\varnothing \}&&=\{0\}\\&2:=1^{+}=\,&&\{\varnothing \}\cup \{\{\varnothing \}\}&&=\{\varnothing ,\{\varnothing \}\}&&=\{0,1\}\\&3:=2^{+}=\,&&\{\varnothing ,\{\varnothing \}\}\cup \{\{\varnothing ,\{\varnothing \}\}\}&&=\{\varnothing ,\{\varnothing \},\{\varnothing ,\{\varnothing \}\}\}&&=\{0,1,2\}\\&\cdots \end{alignedat}}$

另见#3.1 自然数。

无穷公理^w 6（Inf）

${\underset {X}{\exists }}\color {CadetBlue}\left(\color {black}\varnothing \in X\land {\underset {x\in X}{\forall }}S(x)\in X\right)$

基础公理^w 7（Fnd）：非空集有最小元

${\underset {x\neq \varnothing }{\forall }}\ {\underset {y\in x}{\exists }}x\cap y=\varnothing$

1.3.11. 定理：没有集合属于自身

使用：基础公理

${\underset {x}{\forall }}\color {CadetBlue}\left(\color {black}x\in x\Leftrightarrow \{x\}\subseteq x\Leftrightarrow {\underset {u\in \{x\}}{\forall }}u\cap \{x\}=\{x\}\neq \varnothing \Leftrightarrow {\mathit {false}}\right)$

1.3.12. 练习：无穷下降链^w不存在

使用：基础公理

${\underset {\{x_{0},x_{1},\cdots \}}{\forall }}\color {CadetBlue}\left(\color {black}{\underset {n\in \{0,1,\cdots \}}{\forall }}x_{n+1}\in x_{n}\Leftrightarrow {\underset {n\in \{0,1,\cdots \}}{\forall }}\{x_{n+1}\}\subseteq x_{n}\Leftrightarrow {\underset {n\in \{0,1,\cdots \}}{\forall }}\varnothing \neq \{x_{n+1}\}\subseteq x_{n}\cap \{x_{0},x_{1},\cdots \}\Leftrightarrow {\mathit {false}}\right)$

1.3.13.“存在唯一”的定义

${\underset {x}{\exists !}}\,\psi (x):\Leftrightarrow {\underset {x}{\exists }}\,\psi (x)\land {\underset {x,\,y}{\forall }}(\psi (x)\land \psi (y)\Rightarrow x=y)$

替换公理模式^w 8（Rep）

推论使用：外延公理

${\underset {A}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}{\underset {x\in A}{\forall }}\ {\underset {y}{\exists !}}\,\psi (x,y)&\Rightarrow {\underset {B}{\exists }}\ {\underset {y}{\forall }}\color {CadetBlue}\left(\color {black}y\in B\Leftrightarrow {\underset {x\in A}{\exists }}\psi (x,y)\right){\color {black}\land {\underset {B_{1},\,B_{2}}{\forall }}}\left({\color {black}{\underset {y}{\forall }}}\left(\color {black}y\in B_{1}\Leftrightarrow {\underset {x\in A}{\exists }}\psi (x,y)\Leftrightarrow y\in B_{2}\right)\color {black}\Rightarrow B_{1}=B_{2}\right)\\&\Rightarrow {\underset {B}{\exists !}}\color {CadetBlue}\left({\color {black}{\underset {y}{\forall }}}\left(\color {black}y\in B\Leftrightarrow {\underset {x\in A}{\exists }}\psi (x,y)\right)\color {black},\,B=:\left\{y{\bigg |}{\underset {x\in A}{\exists }}\psi (x,y)\right\}\right)\end{aligned}}\right)$

1.3.14. 练习

使用：替换公理模式

$\{0,1,2,\,...\}\in \mathbf {V} \Rightarrow \{\{x\}|x\in \{0,1,2,\,...\}\}=\{\{0\},\{1\},\{2\},\,...\}\in \mathbf {V}$

选择公理^w 9（AC）

${\underset {X\neq \varnothing }{\forall }}\color {CadetBlue}\left(\color {black}\varnothing \notin X\land {\underset {x\in X,\,y\in X,\,x\neq y}{\forall }}x\cap y=\varnothing \Rightarrow {\underset {S}{\exists }}\ {\underset {x\in X}{\forall }}\ {\underset {y}{\exists !}}\,S\cap x=\{y\}\right)$，注意 $S$ 通常不唯一。

习题

1.4 习题

1.4.1. 集合运算的性质

子集的性质

（1）见#1.3.9. 练习：空集是任何集合的子集。

（2）任何集合是自身的子集：${\underset {X}{\forall }}\color {CadetBlue}\left(\color {black}{\mathit {true}}\Leftrightarrow {\underset {u}{\forall }}\,{\color {CadetBlue}(}u\in X\Rightarrow u\in X{\color {CadetBlue})}\Leftrightarrow X\subseteq X\right)$

（3）${\underset {X,\,Y}{\forall }}\color {CadetBlue}\left(\color {black}X\subseteq Y\land Y\subseteq X\Leftrightarrow {\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in X\Rightarrow x\in Y{\color {CadetBlue})}\land {\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in Y\Rightarrow x\in X{\color {CadetBlue})}\Leftrightarrow {\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in X\Leftrightarrow x\in Y{\color {CadetBlue})}\Leftrightarrow X=Y\right)$

（4）${\underset {X,\,Y}{\forall }}\color {CadetBlue}\left(\color {black}X\subseteq Y\land Y\subseteq Z\Leftrightarrow {\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in X\Rightarrow x\in Y{\color {CadetBlue})}\land {\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in Y\Rightarrow x\in Z{\color {CadetBlue})}\Rightarrow {\underset {x}{\forall }}\,{\color {CadetBlue}(}x\in X\Rightarrow x\in Z{\color {CadetBlue})}\Leftrightarrow X\subseteq Y\right)$

交换律

${\underset {X,\,Y}{\forall }}\color {CadetBlue}{\begin{cases}\!\color {black}{\begin{alignedat}{4}&X\cup Y&&=\bigcup \{X,Y\}&&=\bigcup \{Y,X\}&&=Y\cup X\\&&&=\{u|u\in X\lor u\in Y\}&&=\{u|u\in Y\lor u\in X\}&&=Y\cup X\\&X\cap Y&&=\{u|u\in X\land u\in Y\}&&=\{u|u\in Y\land u\in X\}&&=Y\cap X\end{alignedat}}\end{cases}}$

结合律

${\underset {X,\,Y,\,Z}{\forall }}\color {CadetBlue}{\begin{cases}\color {black}(X\cup Y)\cup Z=\{u|(u\in X\lor u\in Y)\lor u\in Z\}=\{u|u\in X\lor (u\in Y\lor u\in Z)\}=X\cup (Y\cup Z)\\\color {black}(X\cap Y)\cap Z=\{u|(u\in X\land u\in Y)\land u\in Z\}=\{u|u\in X\land (u\in Y\land u\in Z)\}=X\cap (Y\cap Z)\end{cases}}$

分配律

${\begin{aligned}&\forall _{X,\,Y,\,Z}\\&\color {CadetBlue}{\begin{cases}\color {black}X\cap (Y\cup Z)=\{u|u\in X\land (u\in Y\lor u\in Z)\}=\{u|(u\in X\land u\in Y)\lor (u\in X\land u\in Z)\}=(X\cap Y)\cup (X\cap Z)\\\color {black}X\cup (Y\cap Z)=\{u|u\in X\lor (u\in Y\land u\in Z)\}=\{u|(u\in X\lor u\in Y)\land (u\in X\lor u\in Z)\}=(X\cup Y)\cap (X\cup Z)\end{cases}}\end{aligned}}$

反演律

${\begin{aligned}&\forall _{X,\,Y,\,Z}\\&\color {CadetBlue}{\begin{cases}\!\color {black}X-(Y\cup Z)=\{u|u\in X\land \neg (u\in Y\lor u\in Z)\}=\{u|(u\in X\land u\notin Y)\land (u\in X\land u\notin Z)\}=(X-Y)\cap (X-Z)\\\!\color {black}X-(Y\cap Z)=\{u|u\in X\land \neg (u\in Y\land u\in Z)\}=\{u|(u\in X\land u\notin Y)\lor (u\in X\land u\notin Z)\}=(X-Y)\cup (X-Z)\end{cases}}\end{aligned}}$

1.4.2.

（1）${\underset {X,\,Y,\,Z}{\forall }}X\cap (Y-Z)=\{u|u\in X\land (u\in Y\land u\notin Z)\}=\{u|(u\in X\land u\in Y)\land u\notin Z\}=(X\cap Y)-Z$

（2）${\underset {X,\,Y}{\forall }}\color {CadetBlue}\left(\color {black}X-Y=\varnothing \Leftrightarrow {\underset {x\in X}{\nexists }}x\notin Y\Leftrightarrow {\underset {x\in X}{\forall }}x\in Y\Leftrightarrow X\subseteq Y\right)$

（3）对称差：${\underset {X,\,Y}{\forall }}X\bigtriangleup Y:=(X-Y)\cup (Y-X),\ {\underset {X}{\forall }}\,X\bigtriangleup X=(X-X)\cup (X-X)=\varnothing \cup \varnothing =\varnothing$

（4）${\underset {X,\,Y}{\forall }}X\bigtriangleup Y=(X-Y)\cup (Y-X)=(Y-X)\cup (X-Y)=Y\bigtriangleup X$

（5）记 ${\mathit {true}}=1,\,{\mathit {false}}=0$，则 ${\underset {X,\,Y,\,u}{\forall }}(u\in X\bigtriangleup Y)=((u\in X)+(u\in Y)){\bmod {2}}$

${\underset {X,\,Y,\,Z,\,u}{\forall }}(u\in (X\bigtriangleup Y)\bigtriangleup Z)=((((u\in X)+(u\in Y)){\bmod {2}})+(u\in Z)){\bmod {2}}$

$=((u\in X)+(u\in Y)+(u\in Z)){\bmod {2}}=((u\in X)+(((u\in Y)+(u\in Z)){\bmod {2}})){\bmod {2}}=(u\in X\bigtriangleup (Y\bigtriangleup Z))$

${\underset {X,\,Y,\,Z}{\forall }}(X\bigtriangleup Y)\bigtriangleup Z=X\bigtriangleup (Y\bigtriangleup Z)$

1.4.3. 越并越大，越交越小

${\underset {F,\,{\mathcal {F}}}{\forall }}\color {CadetBlue}\left({\color {black}F\in {\mathcal {F}}\Rightarrow {\underset {u}{\forall }}}\left(\color {black}u\in \bigcap {\mathcal {F}}\Leftrightarrow {\underset {z\in {\mathcal {F}}}{\forall }}u\in z\Rightarrow u\in F\Rightarrow {\underset {z\in {\mathcal {F}}}{\exists }}u\in z\Leftrightarrow u\in \bigcup {\mathcal {F}}\right)\color {black}\Leftrightarrow \bigcap {\mathcal {F}}\subseteq F\subseteq \bigcup {\mathcal {F}}\right)$

1.4.4.

（1）${\underset {{\mathcal {F}}\neq \varnothing ,\,X}{\forall }}\color {CadetBlue}\left(\color {black}{\underset {F\in {\mathcal {F}}}{\forall }}X\subseteq F\Leftrightarrow {\underset {F\in {\mathcal {F}}}{\forall }}\ {\underset {x\in X}{\forall }}x\in F\Leftrightarrow {\underset {x\in X}{\forall }}\ {\underset {F\in {\mathcal {F}}}{\forall }}x\in F\Leftrightarrow {\underset {x\in X}{\forall }}x\in \bigcap {\mathcal {F}}\Leftrightarrow X\subseteq \bigcap {\mathcal {F}}\right)$

（2）${\underset {{\mathcal {F}},\,X}{\forall }}\color {CadetBlue}\left({\color {black}{\underset {F\in {\mathcal {F}}}{\forall }}F\subseteq X\Rightarrow {\underset {u}{\forall }}}\left(\color {black}u\in \bigcup {\mathcal {F}}\Leftrightarrow {\underset {F\in {\mathcal {F}}}{\exists }}u\in F\subseteq X\Rightarrow u\in X\right)\color {black}\Rightarrow \bigcup {\mathcal {F}}\subseteq X\right)$

（3）

（4）

（5）

（6）

（7）

（8）

（9）

1.4.5.

（1）

（2）

1.4.6.

1.4.7.

因为没有集合属于自身，所以“所有集合的集合”不存在。

1.4.8.

1.4.9. 用弱对集、弱并集、弱幂集公理证明对集、并集、幂集公理

第二章 关系与函数

2.1 关系

2.1.1. 有序对^w的定义

使用：单点集，对集

${\underset {a,\,b}{\forall }}(a,b):=\{\{a\},\{a,b\}\}$

2.1.2. 练习：有序对是集合

使用：对集公理

${\underset {a,\,b}{\forall }}{\color {CadetBlue}(}{\mathit {true}}\Leftrightarrow \{a\}\in \mathbf {V} \land \{a,b\}\in \mathbf {V} \Rightarrow \{\{a\},\{a,b\}\}\in \mathbf {V} \color {CadetBlue})$

2.1.3. 命题：有序对的相等

${\underset {a,\,b,\,a',\,b'}{\forall }}{\color {CadetBlue}(}(a,b)=(a',b')\Leftrightarrow a=a'\land b=b'\color {CadetBlue})$，证明见课本。

2.1.4. 卡氏积^w的定义

使用：有序对

${\underset {X,\,Y}{\forall }}X\times Y:=\{(x,y)|x\in X\land y\in Y\},\ {\underset {X}{\forall }}\,X^{2}:=X\times X$

2.1.5. 练习：卡氏积是集合

使用：有序对是集合，替换公理模式，并集公理

${\underset {X,\,Y}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}{\overset {}{\mathit {true}}}&\Leftrightarrow {\underset {y\in Y}{\forall }}\{(x,y)|x\in X\}\in \mathbf {V} \Rightarrow \{\{(x,y)|x\in X\}|y\in Y\}\in \mathbf {V} \\&\Rightarrow {\underset {y\in Y}{\bigcup }}\{(x,y)|x\in X\}=\{(x,y)|x\in X\land y\in Y\}\in \mathbf {V} \end{aligned}}\right)$

2.1.6. 二元关系^w的定义

使用：卡氏积，子集

${\underset {R}{\forall }}\color {CadetBlue}\left(\color {black}R{\text{ is a binary relation}}:\Leftrightarrow {\underset {X,\,Y}{\exists }}R\subseteq X\times Y\Rightarrow {\underset {x,\,y}{\forall }}{\color {CadetBlue}(}R(x,y)\Leftrightarrow xRy:\Leftrightarrow (x,y)\in R\color {CadetBlue})\right)$

${\underset {R,\,X}{\forall }}{\color {CadetBlue}(}R{\text{ is a binary relation on }}X:\Leftrightarrow R\subseteq X^{2}\color {CadetBlue})$

2.1.8. 定义域^w和值域^w的定义

使用：二元关系

${\underset {R}{\forall }}\color {CadetBlue}\left(\color {black}R{\text{ is a binary relation}}\Rightarrow \mathrm {dom} R:=\left\{x{\bigg |}{\underset {y}{\exists }}\,R(x,y)\right\}\land \mathrm {ran} R:=\left\{y{\Big |}{\underset {x}{\exists }}\,R(x,y)\right\}\right)$

2.1.9. 练习：定义域和值域是集合

使用：分离公理模式

${\underset {R,\,X,\,Y}{\forall }}\color {CadetBlue}\left(\color {black}R\subseteq X\times Y\Rightarrow \mathrm {dom} R=\left\{x\in X{\bigg |}{\underset {y}{\exists }}\,R(x,y)\right\}\land \mathrm {ran} R=\left\{y\in Y{\Big |}{\underset {x}{\exists }}\,R(x,y)\right\}\right)$

2.1.11. 像、逆像、逆和复合的定义

使用：二元关系，值域，定义域，分离公理模式，有序对，替换公理模式

${\underset {R}{\forall }}\color {CadetBlue}\left({\color {black}R{\text{ is a binary relation}}\Rightarrow }\,{\begin{cases}\color {black}{\begin{alignedat}{6}{\underset {X}{\forall }}&&R[X]:={\bigg \{}&&y\in &&\mathrm {ran} R{\bigg |}&&{\underset {x\in X}{\exists }}&R(x,y){\bigg \}}\\{\underset {Y}{\forall }}\,&&R^{-1}[Y]:={\bigg \{}&&x\in &&\,\mathrm {dom} R{\bigg |}&&{\underset {y\in Y}{\exists }}&R(x,y){\bigg \}}\end{alignedat}}\\\color {black}R^{-1}:=\{(x,y)|(y,x)\in R\},\ (R^{-1})^{-1}=R\end{cases}}\right)$

${\underset {R,\,S}{\forall }}\color {CadetBlue}\left(\color {black}R{\text{ and }}S{\text{ are binary relations}}\Rightarrow S\circ R:=\left\{(x,z){\bigg |}{\underset {y}{\exists }}\,{\color {CadetBlue}(}(x,y)\in R\land (y,z)\in S\color {CadetBlue})\right\}\right)$，注意 $R$ 和 $S$ 的顺序。

2.1.13. 练习：逆像就是逆的像

${\underset {R}{\forall }}\color {CadetBlue}\left({\color {black}{\begin{array}{c}R{\text{ is a}}\\{\text{binary}}\\{\text{relation}}\end{array}}\Rightarrow }\left(\color {black}{\begin{aligned}{\mathit {true}}&\Leftrightarrow \mathrm {ran} (R^{-1})=\left\{y{\Big |}{\underset {x}{\exists }}\,(x,y)\in R^{-1}\right\}=\left\{y{\Big |}{\underset {x}{\exists }}\,(y,x)\in R\right\}=\left\{x{\bigg |}{\underset {y}{\exists }}\,(x,y)\in R\right\}=\mathrm {dom} R\\&\Rightarrow {\underset {Y}{\forall }}\,(R^{-1})[Y]=\left\{y\in \mathrm {ran} (R^{-1}){\bigg |}{\underset {x\in Y}{\exists }}(x,y)\in R^{-1}\right\}=\left\{x\in \mathrm {dom} R{\bigg |}{\underset {y\in Y}{\exists }}(y,x)\in R^{-1}\right\}\\&{\hphantom {\Rightarrow {\underset {Y}{\forall }}\,(R^{-1})[Y]\ }}=\left\{x\in \mathrm {dom} R{\bigg |}{\underset {y\in Y}{\exists }}(x,y)\in R\right\}=R^{-1}[Y]\end{aligned}}\right)\right)$

2.2 函数

2.2.1. 函数的定义

使用：二元关系

${\underset {f}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}f{\text{ is a function}}:\!&\Leftrightarrow f{\text{ is a binary relation}}\land {\underset {x,\,y,\,z}{\forall }}\,{\color {CadetBlue}(}(x,y)\in f\land (x,z)\in f\Rightarrow y=z\color {CadetBlue})\\&\Leftrightarrow f{\text{ is a binary relation}}\land {\underset {x\in \mathrm {dom} f}{\forall }}\ {\underset {y}{\exists !}}\,{\color {CadetBlue}(}(x,y)\in f,\,y=:f(x)\color {CadetBlue})\end{aligned}}\right)$

${\underset {f,\,X,\,Y}{\forall }}{\color {CadetBlue}(}f:X\rightarrow Y:\Leftrightarrow f{\text{ is a function}}\land \,\mathrm {dom} f=X\land \mathrm {ran} f\subseteq Y\color {CadetBlue})$

2.2.3. 练习：函数的相等

使用：外延公理

${\underset {f,\,g}{\forall }}\color {CadetBlue}\left({\color {black}{\begin{array}{c}f{\text{ and }}g{\text{ are}}\\{\text{functions}}\end{array}}\Rightarrow }\left(\color {black}{\begin{aligned}f=g&\Leftrightarrow {\underset {x,\,y}{\forall }}\,{\color {CadetBlue}(}(x,y)\in f\Leftrightarrow (x,y)\in g{\color {CadetBlue})}\Leftrightarrow {\underset {x\in \mathrm {dom} f}{\forall }}(x,f(x))\in g\land {\underset {x\in \mathrm {dom} g}{\forall }}(x,g(x))\in f\\&\Leftrightarrow {\underset {x\in \mathrm {dom} f}{\forall }}{\color {CadetBlue}(}x\in \mathrm {dom} g\land f(x)=g(x){\color {CadetBlue})}\land {\underset {x\in \mathrm {dom} g}{\forall }}{\color {CadetBlue}(}x\in \mathrm {dom} f\land g(x)=f(x)\color {CadetBlue})\\&\Leftrightarrow \mathrm {dom} f=\mathrm {dom} g\land {\underset {x\in \mathrm {dom} f}{\forall }}f(x)=g(x)\end{aligned}}\right)\right)$

2.2.4. 练习：函数的复合及其定义域

${\underset {f,\,g}{\forall }}\color {CadetBlue}\left({\color {black}{\begin{array}{c}f{\text{ and }}g{\text{ are}}\\{\text{functions}}\end{array}}\Rightarrow }\,{\begin{cases}\color {black}\!{\begin{aligned}{\mathit {true}}&\Leftrightarrow {\underset {x,\,z_{1},\,z_{2}}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}&(x,z_{1})\in g\circ f\land (x,z_{2})\in g\circ f\\\Leftrightarrow \,&{\underset {y_{1},\,y_{2}}{\exists }}{\color {CadetBlue}(}y_{1}=y_{2}=f(x)\land z_{1}=g(y_{1})\land z_{2}=g(y_{2})\color {CadetBlue})\\\Rightarrow \,&z_{1}=z_{2}=g(f(x))\end{aligned}}\!\right)\\&\Rightarrow g\circ f{\text{ is a function}}\land {\underset {x\in \mathrm {dom} (g\circ f)}{\forall }}(g\circ f)(x)=g(f(x))\end{aligned}}\\\color {black}\!{\begin{aligned}\mathrm {dom} (g\circ f)&=\left\{x{\Big |}{\underset {z}{\exists }}\,(x,z)\in g\circ f\right\}=\left\{x{\bigg |}{\underset {y,\,z}{\exists }}{\color {CadetBlue}(}y=f(x)\land z=g(y){\color {CadetBlue})}\right\}\\&=\{x\in \mathrm {dom} f|f(x)\in \mathrm {dom} g\}=f^{-1}[\mathrm {dom} g]\end{aligned}}\end{cases}}\!\!\right)$

2.2.5. 一一函数（单射）、满射、双射、可逆函数的定义

使用：函数，值域，逆

${\underset {f}{\forall }}\,\color {CadetBlue}{\begin{cases}\color {black}\!{\begin{aligned}f{\text{ is injective}}:\!&\Leftrightarrow f{\text{ is a function}}\land {\underset {x_{1}\in X,\,x_{2}\in X,\,x_{1}\neq x_{2}}{\forall }}f(x_{1})\neq f(x_{2})\\&\Leftrightarrow f{\text{ is a function}}\land {\underset {x_{1},\,x_{2}}{\forall }}{\color {CadetBlue}(}f(x_{1})=f(x_{2})\Rightarrow x_{1}=x_{2}\color {CadetBlue})\end{aligned}}\\\color {black}f{\text{ is an invertible function}}:\Leftrightarrow f{\text{ and }}f^{-1}{\text{ are functions}}\end{cases}}$

${\underset {f,\,X,\,Y}{\forall }}\color {CadetBlue}{\begin{cases}\color {black}f{\text{ is a surjection from }}X{\text{ to }}Y:\Leftrightarrow f:X\rightarrow Y\land \mathrm {ran} f=Y\\\color {black}f{\text{ is a bijection from }}X{\text{ to }}Y:\Leftrightarrow f{\text{ is injective}}\land f{\text{ is a surjection from }}X{\text{ to }}Y\end{cases}}$

2.2.6. 练习：可逆函数就是单射；逆函数亦可逆

${\underset {f}{\forall }}\,\color {CadetBlue}{\begin{cases}{\color {black}f{\text{ is a function}}\Rightarrow }\left(\color {black}{\begin{aligned}f{\text{ is invertible}}&\Leftrightarrow f^{-1}{\text{ is a function}}\Leftrightarrow {\underset {x,\,y,\,z}{\forall }}\color {CadetBlue}\left(\color {black}(x,y)\in f^{-1}\land (x,z)\in f^{-1}\Rightarrow y=z\right)\\&\Leftrightarrow {\underset {x,\,y,\,z}{\forall }}{\color {CadetBlue}(}(y,x)\in f\land (z,x)\in f\Rightarrow y=z{\color {CadetBlue})}\Leftrightarrow f{\text{ is injective}}\end{aligned}}\right)\\\color {black}\!{\begin{aligned}f{\text{ is an invertible function}}&\Leftrightarrow f{\text{ and }}f^{-1}{\text{ are functions}}\Leftrightarrow f^{-1}{\text{ and }}(f^{-1})^{-1}{\text{ are functions}}\\&\Leftrightarrow f^{-1}{\text{ is an invertible function}}\end{aligned}}\end{cases}}$

2.2.7. 函数的限制和扩张的定义

使用：函数，分离公理模式

${\underset {f,\,A}{\forall }}\color {CadetBlue}\left(\color {black}f{\text{ is a function}}\Rightarrow \color {CadetBlue}{\begin{cases}\color {black}{\text{the restriction of }}f{\text{ to }}A=f{\upharpoonright _{A}}:=\{(x,y)\in f|x\in A\}=\{(x,f(x))|x\in \mathrm {dom} f\cap A\}\\\color {black}f{\upharpoonright _{A}}{\text{ is a function}}\end{cases}}\right)$

${\underset {f,\,g}{\forall }}\color {CadetBlue}\left(\color {black}f{\text{ is an extension of }}g\Leftrightarrow f{\text{ is a function}}\land \,{\underset {A}{\exists }}\,g=f{\upharpoonright _{A}}\right)$

2.2.8. 函数相容和相容系统的定义

使用：函数，定义域

${\underset {f,\,g}{\forall }}\color {CadetBlue}\left(\color {black}{\begin{aligned}f{\text{ and }}g{\text{ are compatible}}:\!&\Leftrightarrow f{\text{ and }}g{\text{ are functions}}\land {\underset {x\in \mathrm {dom} f\cap \mathrm {dom} g}{\forall }}f(x)=g(x)\\&\Leftrightarrow f{\text{ and }}g{\text{ are functions}}\land {\underset {x,\,y,\,z}{\forall }}{\color {CadetBlue}(}(x,y)\in f\land (x,z)\in g\Rightarrow y=z\color {CadetBlue})\end{aligned}}\right)$

${\underset {\mathcal {F}}{\forall }}\color {CadetBlue}\left(\color {black}{\mathcal {F}}{\text{ is a compatible system}}:\Leftrightarrow {\underset {f\in {\mathcal {F}},\,g\in {\mathcal {F}}}{\forall }}f{\text{ and }}g{\text{ are compatible}}\right)$

2.2.9. 练习

${\underset {f,\,g}{\forall }}\color {CadetBlue}\left(\!{\color {black}{\begin{array}{c}f{\text{ and }}g{\text{ are}}\\{\text{functions}}\end{array}}\!\Rightarrow }\!\left(\color {black}{\begin{aligned}&f\cup g{\text{ is a function}}\\\Leftrightarrow \,&{\underset {x,\,y,\,z}{\forall }}{\color {CadetBlue}(}(x,y)\in f\cup g\land (x,z)\in f\cup g\Rightarrow y=z{\color {CadetBlue})}\Leftrightarrow {\underset {x,\,y,\,z}{\forall }}{\color {CadetBlue}(}(x,y)\in f\land (x,z)\in g\Rightarrow y=z\color {CadetBlue})\\\Leftrightarrow \,&f{\text{ and }}g{\text{ are compatible}}\Leftrightarrow {\underset {x\in \mathrm {dom} f\cap \mathrm {dom} g}{\forall }}f(x)=g(x)\\\Leftrightarrow \,&f{\upharpoonright _{\mathrm {dom} g}}=\{(x,f(x))|x\in \mathrm {dom} f\cap \mathrm {dom} g\}=\{(x,g(x))|x\in \mathrm {dom} f\cap \mathrm {dom} g\}=g{\upharpoonright _{\mathrm {dom} f}}\end{aligned}}\!\right)\right)$

2.2.11. 集合到集合的函数的集合的定义；空函数；没有非空集到空集的函数

使用：卡氏积，幂集，函数，分离公理模式

${\underset {X,\,Y}{\forall }}Y^{X}:=\{f|f:X\rightarrow Y\}=\{f\in {\mathcal {P}}(X\times Y)|f:X\rightarrow Y\},\ {\underset {Y}{\forall }}\,Y^{\varnothing }=\{\varnothing \},\ {\underset {X\neq \varnothing }{\forall }}\varnothing ^{X}=\varnothing$

2.3 等价与划分

2.3.1. 自反^w、对称^w、传递^w、等价关系^w的定义

使用：二元关系

${\underset {R,\,X}{\forall }}\color {CadetBlue}{\begin{cases}\color {black}\!{\begin{alignedat}{2}&R{\text{ is reflexive }}&&{\text{on }}X:\Leftrightarrow R\subseteq X^{2}\land {\underset {x\in X}{\forall }}R(x,x)\\&R{\text{ is symmetric }}&&{\text{on }}X:\Leftrightarrow R\subseteq X^{2}\land {\underset {x\in X,\,y\in X}{\forall }}{\color {CadetBlue}(}R(x,y)\Rightarrow R(y,x){\color {CadetBlue})}\Leftrightarrow R\subseteq X^{2}\land {\underset {x\in X,\,y\in X}{\forall }}{\color {CadetBlue}(}R(x,y)\Leftrightarrow R(y,x)\color {CadetBlue})\\&R{\text{ is transitive }}&&{\text{on }}X:\Leftrightarrow R\subseteq X^{2}\land {\underset {x\in X,\,y\in X,\,z\in X}{\forall }}{\color {CadetBlue}(}R(x,y)\land R(y,z)\Rightarrow R(x,z)\color {CadetBlue})\end{alignedat}}\\\color {black}R{\text{ is an equivalence relation on }}X:\Leftrightarrow R{\text{ is reflexive, symmetric and transitive on }}X\end{cases}}$

2.3.3. 练习：理想及其上的等价关系

${\underset {X,\,{\mathcal {I}}}{\forall }}\color {CadetBlue}\left(\color {black}{\mathcal {I}}{\text{ is an ideal on }}X:\Leftrightarrow \varnothing \in {\mathcal {I}}\subseteq {\mathcal {P}}(X)\land {\underset {B\in {\mathcal {I}},\,A\subseteq B}{\forall }}A\in {\mathcal {I}}\land {\underset {A\in {\mathcal {I}},\,B\in {\mathcal {I}}}{\forall }}A\cup B\in {\mathcal {I}}\right)$

2.3.4. 等价类的定义

使用：等价关系，分离公理模式

${\underset {\thicksim ,\,X}{\forall }}\color {CadetBlue}\left(\color {black}\thicksim {\text{is an equivalence relation on }}X\Rightarrow {\underset {x\in X}{\forall }}[x]_{\thicksim }:=\{t\in X|t\thicksim x\}\right)$

2.3.5. 练习：等价类互斥

${\underset {\thicksim ,\,X}{\forall }}\color {CadetBlue}\left({\color {black}{\begin{array}{c}\thicksim {\text{is an equivalence}}\\{\text{relation on }}X\end{array}}\Rightarrow {\underset {x\in X,\,y\in X}{\forall }}}\left(\color {black}{\begin{aligned}{\mathit {true}}&\Leftrightarrow x\thicksim y\lor x\nsim y\Leftrightarrow {\underset {t\in X}{\forall }}{\color {CadetBlue}(}t\thicksim x\Leftrightarrow t\thicksim y{\color {CadetBlue})}\lor {\underset {t\in X}{\nexists }}{\color {CadetBlue}(}t\thicksim x\land t\thicksim y\color {CadetBlue})\\&\Leftrightarrow [x]_{\thicksim }=[y]_{\thicksim }\lor [x]_{\thicksim }\cap [y]_{\thicksim }=\varnothing \end{aligned}}\right)\right)$

2.3.6. 划分的定义

使用：空集，交集，并集

${\underset {S,\,X}{\forall }}\color {CadetBlue}\left(\color {black}S{\text{ is a partition of }}X:\Leftrightarrow \varnothing \notin S\land {\underset {a\in S,\,b\in S,\,a\neq b}{\forall }}a\cap b=\varnothing \land \bigcup S=X\right)$，这里对书上的定义稍作修改。

2.3.7. 商集的定义

使用：等价关系，等价类，替换公理模式

${\underset {\thicksim ,\,X}{\forall }}{\color {CadetBlue}(}\thicksim {\text{is an equivalence relation on }}X\Rightarrow X/\thicksim :=\{[x]_{\thicksim }|x\in X\}\color {CadetBlue})$

2.3.8. 定理：商集是划分

由定义显然成立。

2.3.9. 定理：用划分定义等价关系

$S$ 是 $X$ 的划分，$\thicksim _{S}:=\left\{(x,y)\in X^{2}{\bigg |}{\underset {c\in S}{\exists }}(x\in c\land y\in c)\right\}$，则

（1）显然 $\thicksim _{S}$ 自反、对称；

${\underset {x\in X,\,y\in X,\,z\in X}{\forall }}\left(x\thicksim _{S}y\land y\thicksim _{S}z\Leftrightarrow {\underset {c_{1}\in S,\,c_{2}\in S}{\exists }}(x\in c_{1}\land z\in c_{2}\land y\in c_{1}\cap c_{2}\neq \varnothing )\Rightarrow {\underset {c\in S}{\exists }}(x\in c\land z\in c)\Leftrightarrow x\thicksim _{S}z\right)$

故 $\thicksim _{S}$ 传递，于是 $\thicksim _{S}$ 是等价关系。

若 $\varnothing \notin S$，下证 $X/\thicksim _{S}=S$ ：

${\mathit {true}}\Leftrightarrow \bigcup S=X\Leftrightarrow {\underset {x}{\forall }}\left(x\in X\Leftrightarrow {\underset {c\in S}{\exists }}x\in c\right)\Rightarrow {\underset {c\in S}{\forall }}c\subseteq X$

$\because {\underset {a\in S,\,b\in S,\,a\neq b}{\forall }}a\cap b=\varnothing \ \therefore {\underset {x}{\forall }}\left(x\in X\Leftrightarrow {\underset {c\in S}{\exists !}}(x\in c,\,c=:c_{x})\right)$

${\mathit {true}}\Leftrightarrow {\underset {a\in X/\thicksim _{S}}{\forall }}\ {\underset {x\in X}{\exists }}a=[x]_{\thicksim _{S}}=\left\{t\in X{\bigg |}{\underset {c\in S}{\exists }}(t\in c\land x\in c)\right\}=\{t\in X|t\in c_{x}\}=c_{x}\in S\Rightarrow X/\thicksim _{S}\subseteq S$

${\underset {c\in S}{\forall }}\ {\underset {x\in c}{\forall }}(x\in X\land c=c_{x}=[x]_{\thicksim _{S}}\in X/\thicksim _{S})$

$\because \varnothing \notin S\ \therefore {\underset {c\in S}{\forall }}\ {\underset {x}{\exists }}\,x\in c\ \therefore {\underset {c\in S}{\forall }}c\in X/\thicksim _{S}\ \therefore S\subseteq X/\thicksim _{S}\ \therefore X/\thicksim _{S}=S$

（2）$\thicksim$ 是 $X$ 上的等价关系，则

$S=X/\thicksim \,\Rightarrow {\underset {x\in X,\,y\in X}{\forall }}{\Big (}x\thicksim y\Leftrightarrow {\underset {z\in X}{\exists }}(x\thicksim z\land y\thicksim z)\Leftrightarrow {\underset {z\in X}{\exists }}(x\in [z]_{\thicksim }\land y\in [z]_{\thicksim })\Leftrightarrow {\underset {c\in X/\thicksim }{\exists }}(x\in c\land y\in c)$

$\Leftrightarrow {\underset {c\in S}{\exists }}(x\in c\land y\in c)\Leftrightarrow x\thicksim _{S}y{\Big )}\Rightarrow \,\thicksim _{S}=\thicksim$

2.4 序

2.4.1. 反对称、强连接、偏序（序）、线序（全序）的定义

使用：二元关系，自反，传递

${\underset {\leq ,\,X}{\forall }}\color {CadetBlue}{\begin{cases}\color {black}\!{\begin{alignedat}{2}&\leq {\text{is antisymmetric }}&&{\text{on }}X:\Leftrightarrow (\leq )\subseteq X^{2}\land {\underset {x\in X,\,y\in X}{\forall }}{\color {CadetBlue}(}x\leq y\land y\leq x\Rightarrow x=y\color {CadetBlue})\\&\leq {\text{is strongly connected }}&&{\text{on }}X:\Leftrightarrow (\leq )\subseteq X^{2}\land {\underset {x\in X,\,y\in X}{\forall }}{\color {CadetBlue}(}x\leq y\lor y\leq x\color {CadetBlue})\end{alignedat}}\\\color {black}\!{\begin{alignedat}{5}&(X,\leq ){\text{ is a }}&{\text{poset}}&\Leftrightarrow \,\leq {\text{is a }}&{\text{partial }}&{\text{order on }}X:\Leftrightarrow \,\leq {\text{is reflexive, antisymmetric and transitive on }}X\\&(X,\leq ){\text{ is a }}&{\text{toset}}&\Leftrightarrow \,\leq {\text{is a }}&{\text{total }}&{\text{order on }}X:\Leftrightarrow \!\!{\begin{aligned}\leq {\text{is }}&{\text{reflexive, antisymmetric, transitive}}\\&{\text{and strongly connected on }}X\end{aligned}}\end{alignedat}}\end{cases}}$

2.4.2. 记法

${\underset {X,\,(\leq )\subseteq X^{2},\,x\in X,\,y\in X}{\forall }}\color {CadetBlue}{\begin{cases}\color {black}x\geq y:\Leftrightarrow x\leq ^{-1}y\Leftrightarrow y\leq x\\\color {black}x<y:\Leftrightarrow x\leq y\land x\neq y\\\color {black}x>y:\Leftrightarrow x\geq y\land x\neq y\end{cases}}$

2.4.4. 极小（大）元、最小（大）元、上（下）界、上（下）确界的定义

使用：偏序

${\overset {\hphantom {a_{0},\,X,\,X_{0},\,\leq }}{\underset {a,\,X,\,\leq }{\forall }}}\color {CadetBlue}{\begin{cases}\color {black}\!{\begin{alignedat}{6}a{\text{ is a }}&&{\text{minimal element of }}(X,\leq )&&&:\Leftrightarrow (X,\leq ){\text{ is a poset}}\land a\in X\land {\underset {x\in X}{\forall }}\neg \,&a>x\\a{\text{ is a }}&&{\text{maximal element of }}(X,\leq )&&&:\Leftrightarrow (X,\leq ){\text{ is a poset}}\land a\in X\land {\underset {x\in X}{\forall }}\neg \,&a<x\\a{\text{ is a }}&&{\text{least element of }}(X,\leq )&\Leftrightarrow a=\,&\min(X,\leq )&:\Leftrightarrow (X,\leq ){\text{ is a poset}}\land a\in X\land {\underset {x\in X}{\forall }}&a\leq x\\a{\text{ is a }}&&{\text{greatest element of }}(X,\leq )&\Leftrightarrow a=\,&\max(X,\leq )&:\Leftrightarrow (X,\leq ){\text{ is a poset}}\land a\in X\land {\underset {x\in X}{\forall }}&a\geq x\end{alignedat}}\end{cases}}$

${\overset {\hphantom {a_{0},\,X,\,X_{0},\,\leq }}{\underset {a,\,X,\,X_{0},\,\leq }{\forall }}}\color {CadetBlue}{\begin{cases}\color {black}\!{\begin{alignedat}{2}&a{\text{ is an}}&{\text{ upper bound of }}X_{0}{\text{ in }}(X,\leq )\qquad \,:\Leftrightarrow (X,\leq ){\text{ is a poset}}\land X_{0}\subseteq X\land a\in X\land {\underset {x\in X_{0}}{\forall }}\ \ a\geq x\\&a{\text{ is a}}&{\text{ lower bound of }}X_{0}{\text{ in }}(X,\leq )\qquad \,:\Leftrightarrow (X,\leq ){\text{ is a poset}}\land X_{0}\subseteq X\land a\in X\land {\underset {x\in X_{0}}{\forall }}\ \ a\leq x\end{alignedat}}\end{cases}}$

${\overset {\hphantom {a_{0},\,X,\,X_{0},\,\leq }}{\underset {X,\,X_{0},\,\leq }{\forall }}}\color {CadetBlue}{\begin{cases}\color {black}\!{\begin{alignedat}{2}&X_{0}{\text{ has }}&{\text{upper bounds in }}(X,\leq )\qquad \qquad \,:\Leftrightarrow (X,\leq ){\text{ is a poset}}\land X_{0}\subseteq X\land \qquad {\underset {a\in X}{\exists }}\ {\underset {x\in X_{0}}{\forall }}\ \ a\geq x\\&X_{0}{\text{ has }}&{\text{lower bounds in }}(X,\leq )\qquad \qquad \,:\Leftrightarrow (X,\leq ){\text{ is a poset}}\land X_{0}\subseteq X\land \qquad {\underset {a\in X}{\exists }}\ {\underset {x\in X_{0}}{\forall }}\ \ a\leq x\end{alignedat}}\end{cases}}$

${\underset {a_{0},\,X,\,X_{0},\,\leq }{\forall }}\color {CadetBlue}{\begin{cases}\color {black}\!{\begin{alignedat}{4}&a_{0}{\text{ is a s}}&{\text{upremum of }}X_{0}{\text{ in }}(X,\leq )&\Leftrightarrow a_{0}=\sup(X_{0},X,\leq )\\&&:\!\!&\Leftrightarrow (X,\leq ){\text{ is a poset}}\land X_{0}\subseteq X\land a_{0}=\,&\min \left\{a\in X{\bigg |}{\underset {x\in X_{0}}{\forall }}a\geq x\right\}\\&a_{0}{\text{ is an}}&{\text{infimum of }}X_{0}{\text{ in }}(X,\leq )&\Leftrightarrow a_{0}=\,\,\inf(X_{0},X,\leq )\\&&:\!\!&\Leftrightarrow (X,\leq ){\text{ is a poset}}\land X_{0}\subseteq X\land a_{0}=\,&\max \left\{a\in X{\bigg |}{\underset {x\in X_{0}}{\forall }}a\leq x\right\}\end{alignedat}}\end{cases}}$

第三章 实数的构造

3.1 自然数

见#1.3.10. 后继的定义；自然数。

3.1.1. 归纳集的定义

使用：空集，后继

${\underset {X}{\forall }}\color {CadetBlue}\left(\color {black}X{\text{ is an inductive set}}:\Leftrightarrow \varnothing \in X\land {\underset {x\in X}{\forall }}x^{+}\in X\right)$

无穷公理等价于存在归纳集。

3.1.2. 自然数集的定义

使用：归纳集

$\mathbb {N} :=\left\{n{\bigg |}{\underset {X}{\forall }}\,\color {CadetBlue}({\color {black}X{\text{ is an inductive set}}\Rightarrow n\in X})\right\}$

3.1.3. 定理：自然数集是最小的归纳集

$\mathbb {N}$ 是归纳集，并且是任何归纳集的子集。

证明：见课本。

${\mathit {true}}\Leftrightarrow {\underset {M}{\forall }}\color {CadetBlue}\left(\color {black}\varnothing \in M\land {\underset {x\in M}{\forall }}x^{+}\in M\Rightarrow \mathbb {N} \subseteq M\right){\color {black}\Rightarrow {\underset {M\subseteq \mathbb {N} }{\forall }}}\color {CadetBlue}\left(\color {black}\varnothing \in M\land {\underset {x\in M}{\forall }}x^{+}\in M\Rightarrow \mathbb {N} =M\right)$

3.1.4. 自然数集上的归纳原理

$\varphi (0)\land {\underset {n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}\varphi (n)\Rightarrow \varphi (n+1){\color {CadetBlue})}\Rightarrow {\underset {n\in \mathbb {N} }{\forall }}\varphi (n)$

3.1.5. 引理

${\underset {x,\,y}{\forall }}{\color {CadetBlue}(}x\ {\underline {\in }}\ y:\Leftrightarrow x\in y\lor x=y\Leftrightarrow x\in y\cup \{y\}=y^{+}\color {CadetBlue})$

（1）自然数属于并真包含于其后继

（等价于：自然数及其元素属于其后继）

${\underset {n\in \mathbb {N} }{\forall }}\,n\,{\begin{array}{c}\subset \\\in \end{array}}\,n\cup \{n\}=n+1$

（2）自然数的元素是自然数

（等价于：自然数真包含于自然数集）

使用：归纳原理

${\mathit {true}}\Leftrightarrow {\underset {x\in 0}{\forall }}x\in \mathbb {N} \land {\underset {n\in \mathbb {N} }{\forall }}{\color {CadetBlue}\left({\color {black}{\underset {x\in n}{\forall }}x\in \mathbb {N} \Rightarrow {\underset {x\in n+1}{\forall }}}({\color {black}{\mathit {true}}\Leftrightarrow x\in n\lor x=n\Rightarrow x\in \mathbb {N} })\right)}\Rightarrow {\underset {n\in \mathbb {N} ,\,x\in n}{\forall }}x\in \mathbb {N}$

（3）0 属于其他自然数

使用：归纳原理

${\mathit {true}}\Leftrightarrow 0\ {\underline {\in }}\ 0\land {\underset {n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}0\ {\underline {\in }}\ n\Leftrightarrow 0\in n+1\Rightarrow 0\ {\underline {\in }}\ n+1{\color {CadetBlue})}\Rightarrow {\underset {n\in \mathbb {N} }{\forall }}0\ {\underline {\in }}\ n$

（4）自然数的后继的元素是其元素或自身，反之亦然

${\underset {n\in \mathbb {N} ,\,k\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}k\in n+1\Leftrightarrow k\ {\underline {\in }}\ n\color {CadetBlue})$

（5）自然数的元素的后继是其元素或自身

（等价于：自然数的元素的后继是其后继的元素）

使用：归纳原理，（1）自然数属于并真包含于其后继

${\begin{aligned}{\mathit {true}}&\Leftrightarrow {\underset {m\in 0}{\forall }}m+1\ {\underline {\in }}\ 0\land {\underset {n\in \mathbb {N} }{\forall }}\color {CadetBlue}\!\left({\color {black}{\underset {m\in n}{\forall }}m+1\ {\underline {\in }}\ n\Rightarrow {\underset {m\in n+1}{\forall }}}\left\{\color {black}{\begin{alignedat}{2}&m\ {\underline {\in }}\ n\\&m\in n\Rightarrow m+1\ {\underline {\in }}\ n\,&{\begin{array}{c}\subset \\\in \end{array}}\,n+1\\&m=n\Rightarrow m+1&=n+1\end{alignedat}}\right\}\!\color {black}\Rightarrow {\underset {m\in n+1}{\forall }}m+1\ {\underline {\in }}\ n+1\right)\\&\Rightarrow {\underset {n\in \mathbb {N} ,\,m\in n}{\forall }}m+1\ {\underline {\in }}\ n\end{aligned}}$

（6）自然数上 ∈ 的传递性

使用：归纳原理，（1）自然数真包含于其后继

${\begin{aligned}{\mathit {true}}&\Leftrightarrow {\underset {m\in 0,\,k\in m}{\forall }}k\in 0\land {\underset {n\in \mathbb {N} }{\forall }}\color {CadetBlue}\left({\color {black}{\underset {m\in n,\,k\in m}{\forall }}k\in n\Rightarrow {\underset {m\in n+1,\,k\in m}{\forall }}}({\color {black}{\mathit {true}}\Leftrightarrow k\in m\land m\ {\underline {\in }}\ n\Rightarrow k\in n\subset n+1})\right)\\&\Rightarrow {\underset {n\in \mathbb {N} ,\,m\in n,\,k\in m}{\forall }}k\in n\Leftrightarrow {\underset {k\in \mathbb {N} ,\,m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}k\in m\land m\in n\Rightarrow k\in n{\color {CadetBlue})}\Rightarrow {\underset {k\in \mathbb {N} ,\,m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}k\ {\underline {\in }}\ m\land m\ {\underline {\in }}\ n\Rightarrow k\ {\underline {\in }}\ n\color {CadetBlue})\end{aligned}}$

（7）自然数不属于自身

${\underset {n}{\forall }}\,n\notin n$ ，见#1.3.11. 定理：任何集合不属于自身。

（8）自然数的元素就是其真包含的自然数

使用：归纳原理，（5）自然数的元素的后继是其元素或自身

${\begin{aligned}{\mathit {true}}&\Leftrightarrow \!\color {CadetBlue}{\begin{cases}\!{\color {black}{\underset {n\in \mathbb {N} ,\,m\in n}{\forall }}}\left(\color {black}{\mathit {true}}\Leftrightarrow m\neq n\land {\underset {x\in m}{\forall }}x\in n\Leftrightarrow m\subset n\right)\\\!{\color {black}{\underset {m\in \mathbb {N} }{\forall }}}\,({\color {black}m\subset 0\Rightarrow m\in 0})\\\!{\color {black}{\underset {n\in \mathbb {N} }{\forall }}}\!\left(\!{\begin{aligned}&{\color {black}{\underset {m\in \mathbb {N} }{\forall }}}\,({\color {black}m\subset n\Rightarrow m\in n})\\\color {black}\Rightarrow \,&{\color {black}{\underset {m\in \mathbb {N} }{\forall }}}\!\left(\color {black}m\subset n+1\Rightarrow \!\color {CadetBlue}\left\{\color {black}{\begin{aligned}&{\mathit {true}}\Leftrightarrow m\subset n\cup \{n\}\Rightarrow m\subseteq n\lor n\in m\\&n\in m\Rightarrow n+1\ {\underline {\in }}\ m\Leftrightarrow n+1\in m\Rightarrow n+1\subset m\Leftrightarrow {\mathit {false}}\\&m\subseteq n\Rightarrow m\ {\underline {\in }}\ n\Leftrightarrow m\in n+1\end{aligned}}\!\right\}\!\color {black}\Rightarrow m\in n+1\right)\end{aligned}}\!\!\right)\end{cases}}\\&\Leftrightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}m\in n\Leftrightarrow m\subset n{\color {CadetBlue})}\Leftrightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}m\ {\underline {\in }}\ n\Leftrightarrow m\subseteq n\color {CadetBlue})\end{aligned}}$

3.1.6. 定理：(N,⋸) 是线序集

使用：自然数上 ∈ 的传递性，归纳原理，自然数的元素的后继是其元素或自身

${\begin{aligned}{\mathit {true}}&\Leftrightarrow \!\color {CadetBlue}{\begin{cases}{\color {black}{\underset {n\in \mathbb {N} }{\forall }}n\ {\underline {\in }}\ n\land {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}}({\color {black}m\ {\underline {\in }}\ n\land n\ {\underline {\in }}\ m\Rightarrow m=n\lor m\in m\Leftrightarrow m=n})\,{\color {black}\land {\underset {k\in \mathbb {N} ,\,m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}}({\color {black}k\ {\underline {\in }}\ m\land m\ {\underline {\in }}\ n\Rightarrow k\ {\underline {\in }}\ n})\\\!\color {black}{\begin{aligned}{\mathit {true}}&\Leftrightarrow {\underset {m\in \mathbb {N} }{\forall }}0\ {\underline {\in }}\ m\land {\underset {n\in \mathbb {N} }{\forall }}\color {CadetBlue}\left({\color {black}{\underset {m\in \mathbb {N} }{\forall }}}({\color {black}m\ {\underline {\in }}\ n\lor n\ {\underline {\in }}\ m})\,{\color {black}\Leftrightarrow {\underset {m\in \mathbb {N} }{\forall }}}({\color {black}m\ {\underline {\in }}\ n\lor n\in m})\,{\color {black}\Rightarrow {\underset {m\in \mathbb {N} }{\forall }}}({\color {black}m\in n+1\lor n+1\ {\underline {\in }}\ m})\right)\\&\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}m\ {\underline {\in }}\ n\lor n\ {\underline {\in }}\ m\color {CadetBlue})\end{aligned}}\end{cases}}\\&\Rightarrow (\mathbb {N} ,{\underline {\in }}){\text{ is a toset}}\end{aligned}}$

3.1.7. 自然数大小关系的定义

${\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}m\leq n:\Leftrightarrow m\ {\underline {\in }}\ n{\color {CadetBlue})},\,{\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}{\color {CadetBlue}(}m<n:\Leftrightarrow m\in n\color {CadetBlue})$

3.1.8. 良序的定义

使用：线序，子集，空集，最小元

${\underset {\leq ,\,A}{\forall }}\color {CadetBlue}\left(\color {black}(A,\leq ){\text{ is a woset}}\Leftrightarrow \,\leq {\text{is a well-order on }}A:\Leftrightarrow (A,\leq ){\text{ is a toset}}\land {\underset {X\subseteq A,\,X\neq \varnothing }{\forall }}(X,\leq ){\text{ has a least element}}\right)$

3.1.9. 第二归纳原理

使用：归纳原理

${\underset {n\in \mathbb {N} }{\forall }}\color {CadetBlue}\left(\color {black}{\underset {k<n}{\forall }}\varphi (k)\Rightarrow \varphi (n)\right){\color {black}\Rightarrow }\left\{{\begin{aligned}&\!{\color {black}{\mathit {true}}\Leftrightarrow {\underset {k<0}{\forall }}\varphi (k)\land {\underset {n\in \mathbb {N} }{\forall }}}\left(\color {black}{\underset {k<n}{\forall }}\varphi (k)\Rightarrow {\underset {k<n+1}{\forall }}\varphi (k)\right)\color {black}\Rightarrow {\underset {n\in \mathbb {N} ,\,k<n}{\forall }}\varphi (k)\!\\&\color {black}{\underset {k\in \mathbb {N} }{\forall }}\ {\underset {n\in \mathbb {N} }{\exists }}k<n\end{aligned}}\right\}\color {black}\Rightarrow {\underset {k\in \mathbb {N} }{\forall }}\varphi (k)\Leftrightarrow {\underset {n\in \mathbb {N} }{\forall }}\varphi (n)$

3.1.10. 定理：(N,≤) 是良序集

使用：(N,≤) 是线序集，第二归纳原理

${\mathit {true}}\Leftrightarrow {\color {CadetBlue}\left\{\color {black}{\begin{aligned}&(\mathbb {N} ,\leq ){\text{ is a toset}}\\&\!{\underset {X\subseteq \mathbb {N} }{\forall }}\color {CadetBlue}\left(\!\color {black}{\begin{aligned}X{\text{ has no least element}}&\Rightarrow {\underset {n\in \mathbb {N} }{\forall }}\color {CadetBlue}\left({\color {black}{\underset {k<n}{\forall }}k\notin X\Rightarrow }\,({\color {black}n\in X\Leftrightarrow n=\min X\Leftrightarrow {\mathit {false}}})\right)\\&\Rightarrow {\underset {n\in \mathbb {N} }{\forall }}n\notin X\Leftrightarrow X=\varnothing \end{aligned}}\!\right)\end{aligned}}\!\right\}}\Rightarrow \!{\begin{array}{c}(\mathbb {N} ,\leq ){\text{ is}}\\{\text{a woset}}\end{array}}$

3.2 自然数上的递归定理与运算

3.2.1. 递归定理

${\underset {A,\,a\in A,\,g:A\times \mathbb {N} \rightarrow A}{\forall }}\ {\underset {f:\mathbb {N} \rightarrow A}{\exists !}}\color {CadetBlue}\left(\color {black}f(0)=a\land {\underset {n\in \mathbb {N} }{\forall }}f(n+1)=g(f(n),n)\right)$

3.2.2. 序列、有穷序列、空序列、无穷序列的定义

使用：函数，定义域，自然数集

${\underset {s}{\forall }}\,\color {CadetBlue}{\begin{cases}\!\color {black}{\begin{alignedat}{3}&s{\text{ is a}}&{\text{sequence}}&:\Leftrightarrow s{\text{ is a function}}\land \mathrm {dom} s\ {\underline {\in }}\ \mathbb {N} \\&s{\text{ is a}}&{\text{finite sequence}}&:\Leftrightarrow s{\text{ is a function}}\land \mathrm {dom} s\in \mathbb {N} \\&s{\text{ is an}}&{\text{empty sequence}}&:\Leftrightarrow s{\text{ is a function}}\land \mathrm {dom} s=0\\&s{\text{ is an }}&{\text{infinite sequence}}&:\Leftrightarrow s{\text{ is a function}}\land \mathrm {dom} s=\mathbb {N} \end{alignedat}}\end{cases}}$

递归定理的证明

存在性：

${\underset {A}{\forall }}\ {\underset {a\in A,\,g:A\times \mathbb {N} \rightarrow A}{\forall }}\ {\underset {m\in \mathbb {N} }{\forall }}\ {\underset {t}{\forall }}{\Big (}t$ 是（$A$ 上基于 $a$ 和 $g$ 的）$m$-近似 $:\Leftrightarrow t:m+1\rightarrow A\land t_{0}=a\land {\underset {k<m}{\forall }}t_{k+1}=g(t_{k},k){\Big )}$

${\underset {A}{\forall }}\ {\underset {a\in A,\,g:A\times \mathbb {N} \rightarrow A}{\forall }}{\bigg (}{\mathcal {F}}:={\Big \{}t\in {\mathcal {P}}(\mathbb {N} \times A){\Big |}{\underset {m\in \mathbb {N} }{\exists }}t$ 是 $m$-近似${\Big \}},\,{\mathit {true}}\Leftrightarrow {\underset {t\in {\mathcal {F}},\,u\in {\mathcal {F}},\,\mathrm {dom} t\leq \mathrm {dom} u}{\forall }}$

$\left({\mathit {true}}\Leftrightarrow t_{0}=u_{0}=a\land {\underset {k\in \mathbb {N} }{\forall }}(k+1<\mathrm {dom} t\land t_{k}=u_{k}\Rightarrow t_{k+1}=g(t_{k},k)=g(u_{k},k)=u_{k+1})\Rightarrow {\underset {k<\mathrm {dom} t}{\forall }}t_{k}=u_{k}\right)$

$\Rightarrow {\mathcal {F}}$ 是相容的函数系统 $\Rightarrow \bigcup {\mathcal {F}}$ 是函数${\bigg )}$

${\underset {A}{\forall }}\ {\underset {a\in A,\,g:A\times \mathbb {N} \rightarrow A}{\forall }}{\Big (}{\mathit {true}}\Leftrightarrow \{(0,a)\}$ 是 $0$-近似 $\land \,{\underset {n\in \mathbb {N} ,\,t}{\forall }}(t$ 是 $n$-近似 $\Rightarrow t\cup \{(n+1,g(t_{n},n))\}$ 是 $n+1$-近似$)$

$\Rightarrow {\underset {n\in \mathbb {N} }{\forall }}\ {\underset {t\in {\mathcal {F}}}{\exists }}n\in \mathrm {dom} t\Rightarrow {\underset {n\in \mathbb {N} }{\forall }}n\in {\underset {t\in {\mathcal {F}}}{\cup }}\mathrm {dom} t=\mathrm {dom} \bigcup {\mathcal {F}}\Rightarrow \mathbb {N} \subseteq \mathrm {dom} \bigcup {\mathcal {F}}{\Big )}$

${\underset {A}{\forall }}\ {\underset {a\in A,\,g:A\times \mathbb {N} \rightarrow A}{\forall }}{\Big (}{\mathit {true}}\Leftrightarrow \bigcup {\mathcal {F}}$ 是函数 $\land \,\mathrm {dom} \bigcup {\mathcal {F}}\subseteq \mathbb {N} \land \mathrm {ran} \bigcup {\mathcal {F}}\subseteq A\land \mathbb {N} \subseteq \mathrm {dom} \bigcup {\mathcal {F}}\Leftrightarrow \bigcup {\mathcal {F}}:\mathbb {N} \rightarrow A{\Big )}$

${\underset {A}{\forall }}\ {\underset {a\in A,\,g:A\times \mathbb {N} \rightarrow A}{\forall }}{\bigg (}{\mathit {true}}\Leftrightarrow \bigcup {\mathcal {F}}:\mathbb {N} \rightarrow A\land \left({\mathit {true}}\Leftrightarrow {\underset {t\in {\mathcal {F}}}{\forall }}t_{0}=a\Rightarrow \left(\bigcup {\mathcal {F}}\right)(0)=a\right)$

$\land \,{\underset {n\in \mathbb {N} }{\forall }}{\Big (}{\mathit {true}}\Leftrightarrow {\underset {t\in {\mathcal {F}}}{\exists }}t$ 是 $n+1$-近似 $\Rightarrow {\underset {t\in {\mathcal {F}}}{\exists }}t_{n+1}=g(t_{n},n)\Rightarrow \left(\bigcup {\mathcal {F}}\right)(n+1)=g\left(\left(\bigcup {\mathcal {F}}\right)(n),n\right)$

$\Rightarrow {\underset {f:\mathbb {N} \rightarrow A}{\exists }}\left(f(0)=a\land {\underset {n\in \mathbb {N} }{\forall }}f(n+1)=g(f(n),n)\right){\bigg )}$

唯一性：

${\underset {A}{\forall }}\ {\underset {a\in A,\,g:A\times \mathbb {N} \rightarrow A}{\forall }}\ {\underset {f:\mathbb {N} \rightarrow A,\,h:\mathbb {N} \rightarrow A}{\forall }}{\Big (}f(0)=h(0)=a\land {\underset {n\in \mathbb {N} }{\forall }}f(n+1)=g(f(n),n)\land {\underset {n\in \mathbb {N} }{\forall }}h(n+1)=g(h(n),n)$

$\Rightarrow f(0)=h(0)\land {\underset {n\in \mathbb {N} }{\forall }}(f(n)=h(n)\Rightarrow f(n+1)=g(f(n),n)=g(h(n),n)=h(n+1))\Rightarrow {\underset {n\in \mathbb {N} }{\forall }}g(n)=h(n)\Leftrightarrow f=h{\Big )}$

$\therefore {\underset {A}{\forall }}\ {\underset {a\in A,\,g:A\times \mathbb {N} \rightarrow A}{\forall }}\ {\underset {f:\mathbb {N} \rightarrow A}{\exists !}}\left(f(0)=a\land {\underset {n\in \mathbb {N} }{\forall }}f(n+1)=g(f(n),n)\right)$

3.2.3. 带参数的递归定理

${\underset {P,\,A}{\forall }}\ {\underset {g:P\times A\times \mathbb {N} \rightarrow A}{\forall }}\ {\underset {t\in A^{P},\,n\in \mathbb {N} }{\forall }}\ {\underset {h\in A^{P}}{\exists !}}\ {\underset {p\in P}{\forall }}h(p)=g(p,t(p),n)$

${\underset {P,\,A}{\forall }}\ {\underset {g:P\times A\times \mathbb {N} \rightarrow A}{\forall }}\ {\underset {G:A^{P}\times \mathbb {N} \rightarrow A^{P}}{\exists !}}\ {\underset {t\in A^{P},\,n\in \mathbb {N} }{\forall }}\ {\underset {p\in P}{\forall }}G(t,n)(p)=g(p,t(p),n)$

根据递归定理，${\underset {P,\,A}{\forall }}\ {\underset {a\in A^{P},\,G:A^{P}\times \mathbb {N} \rightarrow A^{P}}{\forall }}\ {\underset {F:\mathbb {N} \rightarrow A^{P}}{\exists !}}\left(F(0)=a\land {\underset {n\in \mathbb {N} }{\forall }}F(n+1)=G(F(n),n)\right)$

$\therefore {\underset {P,\,A}{\forall }}\ {\underset {a:P\rightarrow A,\,g:P\times A\times \mathbb {N} \rightarrow A}{\forall }}\ {\underset {F:\mathbb {N} \rightarrow A^{P}}{\exists !}}\ {\underset {p\in P}{\forall }}\left(F(0)(p)=a(p)\land {\underset {n\in \mathbb {N} }{\forall }}F(n+1)(p)=g(p,F(n)(p),n)\right)$

$\therefore {\underset {P,\,A}{\forall }}\ {\underset {a:P\rightarrow A,\,g:P\times A\times \mathbb {N} \rightarrow A}{\forall }}\ {\underset {f:P\times \mathbb {N} \rightarrow A}{\exists !}}\ {\underset {p\in P}{\forall }}\left(f(p,0)=a(p)\land {\underset {n\in \mathbb {N} }{\forall }}f(p,n+1)=g(p,f(p,n),n)\right)$

3.2.4. 定理：自然数上加法的定义

使用：带参数的递归定理

${\underset {+:\mathbb {N} \times \mathbb {N} \rightarrow \mathbb {N} }{\exists !}}\color {CadetBlue}\left({\color {black}{\underset {m\in \mathbb {N} }{\forall }}}\left(\color {black}+(m,0)=m\land {\underset {n\in \mathbb {N} }{\forall }}+(m,n+1)=+(m,n)+1\right)\color {black},\,{\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}+(m,n)=:m+n\right)$

3.2.5. 定理：自然数上乘法的定义

使用：带参数的递归定理，自然数上的加法

${\underset {\cdot :\mathbb {N} \times \mathbb {N} \rightarrow \mathbb {N} }{\exists !}}\color {CadetBlue}\left({\color {black}{\underset {m\in \mathbb {N} }{\forall }}}\left(\color {black}\cdot (m,0)=0\land {\underset {n\in \mathbb {N} }{\forall }}\cdot (m,n+1)=\cdot (m,n)+m\right)\color {black},\,{\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}\cdot (m,n)=:m\cdot n=mn\right)$

3.2.7. 引理：自然数上加法和乘法的运算定律

（1）加法交换律

使用：归纳原理，加法的定义

${\begin{aligned}{\mathit {true}}&\Leftrightarrow \!\color {CadetBlue}{\begin{cases}{\color {black}{\mathit {true}}\Leftrightarrow 0+0=0\land {\underset {m\in \mathbb {N} }{\forall }}}({\color {black}0+m=m\Rightarrow 0+(m+1)=(0+m)+1=m+1})\color {black}\Rightarrow {\underset {m\in \mathbb {N} }{\forall }}0+m=m=m+0\\\!{\color {black}{\underset {n\in \mathbb {N} }{\forall }}}\left(\color {black}{\begin{aligned}&{\underset {m\in \mathbb {N} }{\forall }}m+n=n+m\\\Rightarrow \,&\color {CadetBlue}{\begin{cases}\color {black}0+(n+1)=(n+1)+0\\\!{\color {black}{\underset {m\in \mathbb {N} }{\forall }}}\left(\!\color {black}{\begin{aligned}&m+(n+1)=(n+1)+m\\\Rightarrow \,&(m+1)+(n+1)=((m+1)+n)+1=(n+(m+1))+1=((n+m)+1)+1\\&{\phantom {(m+1)+(n+1)}}=((m+n)+1)+1=(m+(n+1))+1=((n+1)+m)+1\\&{\phantom {(m+1)+(n+1)}}=(n+1)+(m+1)\end{aligned}}\!\right)\end{cases}}\\\Rightarrow \,&{\underset {m\in \mathbb {N} }{\forall }}m+(n+1)=(n+1)+m\end{aligned}}\!\!\!\right)\end{cases}}\\&\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}m+n=n+m\end{aligned}}$

（2）加法结合律

使用：归纳原理，加法的定义，加法交换律

${\begin{aligned}{\mathit {true}}&\Leftrightarrow \!\color {CadetBlue}{\begin{cases}\color {black}{\underset {m\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m+0)+p=m+(0+p)\\\!{\color {black}{\underset {n\in \mathbb {N} }{\forall }}}\left(\!\color {black}{\begin{aligned}&{\phantom {\Rightarrow }}\ {\underset {m\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m+n)+p=m+(n+p)\\&\!{\begin{aligned}\Rightarrow {\underset {m\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m+(n+1))+p&=((m+n)+1)+p=p+((m+n)+1)=(p+(m+n))+1\\{\vphantom {\underset {}{}}}&=(p+(n+m))+1=((p+n)+m)+1=(m+(p+n))+1\\&=m+((p+n)+1)=m+(p+(n+1))=m+((n+1)+p)\end{aligned}}\end{aligned}}\!\right)\end{cases}}\\&\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m+n)+p=m+(n+p)\end{aligned}}$

（3）乘法交换律

${\mathit {true}}\Leftrightarrow \left({\mathit {true}}\Leftrightarrow 0\cdot 0=0\cdot 0\land {\underset {m\in \mathbb {N} }{\forall }}(0m=m\Rightarrow 0(m+1)=0m+0=0)\Rightarrow {\underset {m\in \mathbb {N} }{\forall }}0m=0=m0\right)$

$\land {\underset {n\in \mathbb {N} }{\forall }}{\Big (}{\underset {m\in \mathbb {N} }{\forall }}mn=nm\Rightarrow 0(n+1)=(0+n)0\land {\underset {m\in \mathbb {N} }{\forall }}{\big (}m(n+1)=(n+1)m$

$\Rightarrow (m+1)(n+1)=(m+1)n+m+1=n(m+1)+m+1=nm+n+m+1=mn+m+n+1$

$=m(n+1)+n+1=(n+1)m+n+1=(n+1)(m+1){\big )}\Rightarrow {\underset {m\in \mathbb {N} }{\forall }}m(n+1)=(n+1)m{\Big )}\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}mn=nm$

（5）乘法对加法的分配律

${\mathit {true}}\Leftrightarrow {\underset {n\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}0(n+p)=0=0n+0p\land {\underset {m\in \mathbb {N} }{\forall }}{\Big (}{\underset {n\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}m(n+p)=mn+mp$

$\Rightarrow {\underset {n\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m+1)(n+p)=(n+p)(m+1)=(n+p)m+(n+p)=m(n+p)+(n+p)=(mn+mp)+(p+n)$

$=((mn+mp)+p)+n=n+((mn+mp)+p)=n+(mn+(mp+p))=(n+mn)+(mp+p)$

$=(nm+n)+(pm+p)=n(m+1)+p(m+1)=(m+1)n+(m+1)p{\Big )}\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}m(n+p)=mn+mp$

（4）乘法结合律

${\mathit {true}}\Leftrightarrow {\underset {m\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m0)p=0=m(0p)\land {\underset {n\in \mathbb {N} }{\forall }}{\Big (}{\underset {m\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(mn)p=m(np)\Rightarrow {\underset {m\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m(n+1))p=(mn+m)p$

$=p(nm+m)=p(nm)+pm=(pn)m+pm=m(pn)+mp=m(pn+p)=m(p(n+1))=m((n+1)p){\Big )}$

$\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(mn)p=m(np)$

3.4 整数与有理数

3.4.1. 整数集的定义

${\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} }{\forall }}(m_{1},n_{1})\thicksim (m_{2},n_{2}):\Leftrightarrow m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}=m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1},\ \mathbb {Z} :=\mathbb {N} \times \mathbb {N} /\thicksim$

3.4.2. 练习

${\mathit {true}}\Leftrightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m=n\Rightarrow m+1=n+1\Leftrightarrow m\cup \{m\}=n\cup \{n\}\Rightarrow m=n\lor (m\in n\land n\in m)\Leftrightarrow m=n)$

$\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m=n\Leftrightarrow m+1=n+1)$

${\mathit {true}}\Leftrightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m+0=n+0\Leftrightarrow m=n)\land {\underset {p\in \mathbb {N} }{\forall }}{\Big (}{\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m+p=n+p\Leftrightarrow m=n)$

$\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m+(p+1)=n+(p+1)\Leftrightarrow (m+p)+1=(n+p)+1\Leftrightarrow m+p=n+p\Leftrightarrow m=n){\Big )}$

$\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m+p=n+p\Leftrightarrow m=n)$

${\mathit {true}}\Leftrightarrow {\underset {(m,n)\in \mathbb {N} \times \mathbb {N} }{\forall }}({\mathit {true}}\Leftrightarrow m+n=m+n\Leftrightarrow (m,n)\thicksim (m,n))\,\land$

${\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} }{\forall }}((m_{1},n_{1})\thicksim (m_{2},n_{2})\Leftrightarrow m_{1}+n_{2}=m_{2}+n_{1}\Leftrightarrow m_{2}+n_{1}=m_{1}+n_{2}\Leftrightarrow (m_{2},n_{2})\thicksim (m_{1},n_{1}))$

$\land {\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} ,\,(m_{3},n_{3})\in \mathbb {N} \times \mathbb {N} }{\forall }}((m_{1},n_{1})\thicksim (m_{2},n_{2})\land (m_{2},n_{2})\thicksim (m_{3},n_{3})$

$\Leftrightarrow m_{1}+n_{2}=m_{2}+n_{1}\land m_{2}+n_{3}=m_{3}+n_{2}\Rightarrow (m_{1}+n_{2})+(m_{2}+n_{3})=(m_{2}+n_{1})+(m_{3}+n_{2})$

$\Leftrightarrow (m_{1}+n_{3})+(m_{2}+n_{2})=(m_{3}+n_{1})+(m_{2}+n_{2})\Leftrightarrow m_{1}+n_{3}=m_{3}+n_{1}\Leftrightarrow (m_{1},n_{1})\thicksim (m_{3},n_{3}))$

$\Rightarrow \,\thicksim$ 是 $\mathbb {N} \times \mathbb {N}$ 上的等价关系

3.4.3. 整数集上的线序、加法和乘法、整数零的定义

${\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} }{\forall }}\left([(m_{1},n_{1})]\,{\underset {\mathbb {Z} }{\leq }}\,[(m_{2},n_{2})]:\Leftrightarrow m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\,{\underset {\mathbb {N} }{\leq }}\,m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\right)$

${\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} }{\forall }}[(m_{1},n_{1})]\,{\underset {\mathbb {Z} }{+}}\,[(m_{2},n_{2})]:=\left[\left(m_{1}\,{\underset {\mathbb {N} }{+}}\,m_{2},n_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\right)\right]$

${\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} }{\forall }}[(m_{1},n_{1})]\,{\underset {\mathbb {Z} }{\cdot }}\,[(m_{2},n_{2})]:=\left[\left(m_{1}\,{\underset {\mathbb {N} }{\cdot }}\,m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\,{\underset {\mathbb {N} }{\cdot }}\,n_{2},\,m_{1}\,{\underset {\mathbb {N} }{\cdot }}\,n_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\,{\underset {\mathbb {N} }{\cdot }}\,m_{2}\right)\right]$

${\underset {\mathbb {Z} }{0}}:=[(0,0)],\ {\underset {n\in \mathbb {N} }{\forall }}\ {\underset {\mathbb {Z} }{0}}=[(n,n)]$

整数集上的线序

${\mathit {true}}\Leftrightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m\leq n\Leftrightarrow m<n+1\Rightarrow m+1\leq n+1\Rightarrow m<n+1\Leftrightarrow m\leq n)$

$\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m\leq n\Leftrightarrow m+1\leq n+1)$

${\mathit {true}}\Leftrightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m+0\leq n+0\Leftrightarrow m\leq n)\land {\underset {p\in \mathbb {N} }{\forall }}{\Big (}{\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m+p\leq n+p\Leftrightarrow m\leq n)$

$\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} }{\forall }}(m+(p+1)\leq n+(p+1)\Leftrightarrow (m+p)+1\leq (n+p)+1\Leftrightarrow m+p\leq n+p\Leftrightarrow m\leq n){\Big )}$

$\Rightarrow {\underset {m\in \mathbb {N} ,\,n\in \mathbb {N} ,\,p\in \mathbb {N} }{\forall }}(m+p\leq n+p\Leftrightarrow m\leq n)$

$\Rightarrow {\underset {m_{1}\in \mathbb {N} ,\,n_{1}\in \mathbb {N} ,\,m_{2}\in \mathbb {N} ,\,n_{2}\in \mathbb {N} }{\forall }}(m_{1}\leq m_{2}\land n_{1}\leq n_{2}\Rightarrow m_{1}+n_{1}\leq m_{2}+n_{1}\leq m_{2}+n_{2})$

${\mathit {true}}\Leftrightarrow {\underset {(m,n)\in \mathbb {N} \times \mathbb {N} }{\forall }}\left({\mathit {true}}\Leftrightarrow m\,{\underset {\mathbb {N} }{+}}\,n\,{\underset {\mathbb {N} }{\leq }}\,m\,{\underset {\mathbb {N} }{+}}\,n\Leftrightarrow [(m,n)]\,{\underset {\mathbb {Z} }{\leq }}\,[(m,n)]\right)$

$\land {\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} }{\forall }}{\Big (}[(m_{1},n_{1})]\,{\underset {\mathbb {Z} }{\leq }}\,[(m_{2},n_{2})]\land [(m_{2},n_{2})]\,{\underset {\mathbb {Z} }{\leq }}\,[(m_{1},n_{1})]\Leftrightarrow m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\,{\underset {\mathbb {N} }{\leq }}\,m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\land m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\,{\underset {\mathbb {N} }{\leq }}\,m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}$

$\Leftrightarrow m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}=m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\Leftrightarrow (m_{1},n_{1})\thicksim (m_{2},n_{2})\Leftrightarrow [(m_{1},n_{1})]=[(m_{2},n_{2})]{\Big )}$

$\land {\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} ,\,(m_{3},n_{3})\in \mathbb {N} \times \mathbb {N} }{\forall }}{\Big (}[(m_{1},n_{1})]\,{\underset {\mathbb {Z} }{\leq }}\,[(m_{2},n_{2})]\land [(m_{2},n_{2})]\,{\underset {\mathbb {Z} }{\leq }}\,[(m_{3},n_{3})]$

$\Leftrightarrow m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\,{\underset {\mathbb {N} }{\leq }}\,m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\land m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{3}\,{\underset {\mathbb {N} }{\leq }}\,m_{3}\,{\underset {\mathbb {N} }{+}}\,n_{2}\Rightarrow \left(m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\right){\underset {\mathbb {N} }{+}}\left(m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{3}\right){\underset {\mathbb {N} }{\leq }}\left(m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\right){\underset {\mathbb {N} }{+}}\left(m_{3}\,{\underset {\mathbb {N} }{+}}\,n_{2}\right)$

$\Leftrightarrow \left(m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{3}\right){\underset {\mathbb {N} }{+}}\left(m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{2}\right){\underset {\mathbb {N} }{\leq }}\left(m_{3}\,{\underset {\mathbb {N} }{+}}\,n_{1}\right){\underset {\mathbb {N} }{+}}\left(m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{2}\right)\Leftrightarrow m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{3}\,{\underset {\mathbb {N} }{\leq }}\,m_{3}\,{\underset {\mathbb {N} }{+}}\,n_{1}\Leftrightarrow [(m_{1},n_{1})]\,{\underset {\mathbb {Z} }{\leq }}\,[(m_{3},n_{3})]{\Big )}$

$\land {\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} }{\forall }}{\Big (}{\mathit {true}}\Leftrightarrow m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\,{\underset {\mathbb {N} }{\leq }}\,m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\lor m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{1}\,{\underset {\mathbb {N} }{\leq }}\,m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}$

$\Leftrightarrow [(m_{1},n_{1})]\,{\underset {\mathbb {Z} }{\leq }}\,[(m_{2},n_{2})]\lor [(m_{2},n_{2})]\,{\underset {\mathbb {Z} }{\leq }}\,[(m_{1},n_{1})]{\Big )}\Rightarrow \left(\mathbb {Z} ,{\underset {\mathbb {Z} }{\leq }}\right)$是线序集

整数加法是函数

${\underset {(m_{1},n_{1})\in \mathbb {N} \times \mathbb {N} ,\,(m_{2},n_{2})\in \mathbb {N} \times \mathbb {N} ,\,(m_{1}',n_{1}')\in \mathbb {N} \times \mathbb {N} ,\,(m_{2}',n_{2}')\in \mathbb {N} \times \mathbb {N} }{\forall }}{\bigg (}[(m_{1},n_{1})]=[(m_{1}',n_{1}')]\land [(m_{2},n_{2})]=[(m_{2}',n_{2}')]$

$\Leftrightarrow (m_{1},n_{1})\thicksim (m_{1}',n_{1}')\land (m_{2},n_{2})\thicksim (m_{2}',n_{2}')\Leftrightarrow m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{1}'=m_{1}'\,{\underset {\mathbb {N} }{+}}\,n_{1}\land m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{2}'=m_{2}'\,{\underset {\mathbb {N} }{+}}\,n_{2}$

$\Rightarrow \left(m_{1}\,{\underset {\mathbb {N} }{+}}\,n_{1}'\right){\underset {\mathbb {N} }{+}}\left(m_{2}\,{\underset {\mathbb {N} }{+}}\,n_{2}'\right)=\left(m_{1}'\,{\underset {\mathbb {N} }{+}}\,n_{1}\right){\underset {\mathbb {N} }{+}}\left(m_{2}'\,{\underset {\mathbb {N} }{+}}\,n_{2}\right)\Leftrightarrow \left(m_{1}\,{\underset {\mathbb {N} }{+}}\,m_{2}\right){\underset {\mathbb {N} }{+}}\left(n_{1}'\,{\underset {\mathbb {N} }{+}}\,n_{2}'\right)=\left(m_{1}'\,{\underset {\mathbb {N} }{+}}\,m_{2}'\right){\underset {\mathbb {N} }{+}}\left(n_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\right)$

$\Leftrightarrow \left(m_{1}\,{\underset {\mathbb {N} }{+}}\,m_{2},n_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\right)\thicksim \left(m_{1}'\,{\underset {\mathbb {N} }{+}}\,m_{2}',n_{1}'\,{\underset {\mathbb {N} }{+}}\,n_{2}'\right)\Leftrightarrow \left[\left(m_{1}\,{\underset {\mathbb {N} }{+}}\,m_{2},n_{1}\,{\underset {\mathbb {N} }{+}}\,n_{2}\right)\right]=\left[\left(m_{1}'\,{\underset {\mathbb {N} }{+}}\,m_{2}',n_{1}'\,{\underset {\mathbb {N} }{+}}\,n_{2}'\right)\right]{\bigg )}$

3.4.4. 命题：整数有唯一加法逆元；整数减法的定义

${\underset {(m,n)\in \mathbb {N} \times \mathbb {N} }{\forall }}\ {\underset {(m',n')\in \mathbb {N} \times \mathbb {N} }{\forall }}{\bigg (}[(m,n)]\,{\underset {\mathbb {Z} }{+}}\,[(m',n')]={\underset {\mathbb {Z} }{0}}\Leftrightarrow \left(m\,{\underset {\mathbb {N} }{+}}\,m',n\,{\underset {\mathbb {N} }{+}}\,n'\right)\thicksim (0,0)\Leftrightarrow m\,{\underset {\mathbb {N} }{+}}\,m'=n\,{\underset {\mathbb {N} }{+}}\,n'$

$\Leftrightarrow m'\,{\underset {\mathbb {N} }{+}}\,m=n\,{\underset {\mathbb {N} }{+}}\,n'\Leftrightarrow (m',n')\thicksim (n,m)\Leftrightarrow [(m',n')]=[(n,m)]{\bigg )}$

${\underset {a\in \mathbb {Z} }{\forall }}\ {\underset {a'\in \mathbb {Z} }{\exists !}}\left(a\,{\underset {\mathbb {Z} }{+}}\,a'={\underset {\mathbb {Z} }{0}},\,a'=:-a\right),\ {\underset {a\in \mathbb {Z} ,\,b\in \mathbb {Z} }{\forall }}a-b:=a\,{\underset {\mathbb {Z} }{+}}\,(-b)$

3.4.5. 整数的绝对值的定义

${\underset {a\in \mathbb {Z} }{\forall }}|a|:={\begin{cases}a,&a\,{\underset {\mathbb {Z} }{\geq }}\,{\underset {\mathbb {Z} }{0}}\\-a,&a\,{\underset {\mathbb {Z} }{<}}\,{\underset {\mathbb {Z} }{0}}\end{cases}}$

${\mathit {true}}\Leftrightarrow {\underset {a{\underset {\mathbb {Z} }{\geq }}{\underset {\mathbb {Z} }{0}}}{\forall }}|a|=a\,{\underset {\mathbb {Z} }{\geq }}\,{\underset {\mathbb {Z} }{0}}\land {\underset {(m,n)\in \mathbb {N} \times \mathbb {N} }{\forall }}\left([(m,n)]\,{\underset {\mathbb {Z} }{<}}\,{\underset {\mathbb {Z} }{0}}\Leftrightarrow m\,{\underset {\mathbb {Z} }{<}}\,n\Leftrightarrow n\,{\underset {\mathbb {N} }{>}}\,m\Rightarrow |[(m,n)]|=-[(m,n)]=[(n,m)]\,{\underset {\mathbb {Z} }{>}}\,{\underset {\mathbb {Z} }{0}}\right)$

$\Rightarrow {\underset {a\in \mathbb {Z} }{\forall }}|a|\,{\underset {\mathbb {Z} }{\geq }}\,{\underset {\mathbb {Z} }{0}}$