自然数や濃度の基本を整備します。(dagger)
0. … \(x \in 0 \Longleftrightarrow {\perp}\)
0.' … \(0 = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(s,s) … \(\textit{+1}\) \(\textit{+1}\)
suc. … \(x \in n \textit{+1} \Longleftrightarrow x \in n \mathbin{\rm o\!r} x = n\)
suc.' … \(n \textit{+1} = n \cup \{ n \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
suc_. … \({\textit{+1}} \, \stackrel{\star}{=} {\stackrel{\text{^}}{\textit{+1}}}\)
Ind. … \(\text{Ind} = \{ M \mid 0 \in M , \forall m \in M . m \textit{+1} \in M \}\)
Ind.' … \(\text{Ind} = \{ M \mid 0 \in M , M \textit{+1} \subset M \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(,s) … \(\mathbb{M}\)
ax_m … \(0 \in \mathbb{M}\)
\M. … \(\mathbb{M} = \bigcap \text{Ind}\)
\M1 … \(\forall n \in \mathbb{M} . n \textit{+1} \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\M1' … \(\mathbb{M} \textit{+1} \subset \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
<\M:i … \(n \in \mathbb{M} \Longrightarrow n \subset \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
省略形（須田作）\(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
\(\bigcup \mathbb{M} = \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
<\M:l … \(m \in n \in \mathbb{M} \Longrightarrow m \subsetneq n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
<\M:r … \(m , n \in \mathbb{M} , m \subsetneq n \Longrightarrow m \in n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
<\M:0 … \(m , n \in \mathbb{M} \Longrightarrow m \in n \Leftrightarrow m \subsetneq n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
<\M:1 … \(m , n \in \mathbb{M} \Longrightarrow m \subsetneq n \textit{+1} \Leftrightarrow m \subset n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
\(\mathbb{M} \subset \mathbb{V}_0\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
Cup\M … \(m \in \mathbb{M} \Longrightarrow \bigcup ( m \textit{+1} ) = m\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
<\M:T … \(m , n \in \mathbb{M} \Longrightarrow m \subset n \mathbin{\rm o\!r} n \subset m\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
\({\tt n}\). … \(x \in {\tt n} \Longleftrightarrow x = 0 \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = {\tt n\,{\text -}\,1}\)
\({\tt n}\).' … \({\tt n} = \{ 0 , \cdots , {\tt n\,{\text -}\,1} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\({\tt n}\).. … \({\tt n} = ( {\tt n\,{\text -}\,1} ) \textit{+1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\({\tt n} \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m
2以上の自然数 \({\tt n}\) に対し
in\({\tt n}\) … \(0 \in 1 \in \cdots \in {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
neq\({\tt n}\) … \(0 \neq 1 , \cdots\!\cdots , {\tt n\,{\text -}\,2} \neq {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
subn\({\tt n}\) … \(0 \subsetneq 1 \subsetneq \cdots \subsetneq {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
subn\({\tt n}\)\(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
\(\mathbb{W}_0\)(s\(^{\tt n}\),s)F … \(\mathsf{ary}_{\tt n}\)
abbr … \(\langle X_{1} , \cdots , X_{\tt n} \rangle\) ≈ \(\mathsf{ary}_{\tt n} ( X_{1} , \cdots , X_{\tt n} )\)
ary\({\tt n}\). … \(\langle x_{1} , \cdots , x_{\tt n} \rangle = \{ \langle 0 , x_{1} \rangle , \cdots , \langle {\tt n\,{\text -}\,1} , x_{\tt n} \rangle \}\)
ary\({\tt n}\)R … \(\langle x_{1} , \cdots , x_{\tt n} \rangle \in {\tt n} \to \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ary\({\tt n}\)L … \(f \in {\tt n} \to \mathbb{V} \Rightarrow f = \langle f ( 0 ) , \cdots , f ( {\tt n\,{\text -}\,1} ) \rangle\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ary\({\tt n}\)> … \(\triangleright ( \langle x_{1} , \cdots , x_{\tt n} \rangle ) = \{ x_{1} , \cdots , x_{\tt n} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ary\({\tt n}\)S … \(\langle x_{1} , \cdots , x_{\tt n} \rangle \in {\tt n} \stackrel{\rm S}\to \{ x_{1} , \cdots , x_{\tt n} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ary1IS … \(\langle x \rangle \in 1 \stackrel{\rm IS}\to \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
2以上の自然数 \({\tt n}\) に対して
ary\({\tt n}\)IS … \(x_{0} \neq x_{1} , \cdots\!\cdots , x_{\tt n\,{\text -}\,2} \neq x_{\tt n\,{\text -}\,1} \Longleftrightarrow \langle x_{0} , \cdots , x_{\tt n\,{\text -}\,1} \rangle \in {\tt n} \stackrel{\rm IS}\to \{ x_{0} , \cdots , x_{\tt n\,{\text -}\,1} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=#. … \(X \stackrel{\#}= Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm IS}\to Y\)
=#.' … \(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
le#. … \(X \stackrel{\#}\le Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm I}\to Y\)
le#.' … \(X \stackrel{\#}\le Y \Longleftrightarrow X \stackrel{\rm I}\to Y \neq \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
<#. … \(X \stackrel{\#}< Y \Longleftrightarrow X \stackrel{\#}\le Y , X \stackrel{{\tt /}}{\stackrel{\#}=} Y\)
=:RTX … \({\stackrel{\#}=} :\mathsf{R}\&\mathsf{T}\&\mathsf{X}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=:C … \(X \stackrel{\#}= Y \Longleftrightarrow Y \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
le:RT … \({\stackrel{\#}\le} :\mathsf{R}\&\mathsf{T}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
Schröder-Bernsteinの定理
<:T … \(X \stackrel{\#}< Y \stackrel{\#}\le Z \mathbin{\rm o\!r} X \stackrel{\#}\le Y \stackrel{\#}< Z \Longrightarrow X \stackrel{\#}< Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=#0 … \(X \stackrel{\#}= \emptyset \Longleftrightarrow X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=#1 … \(X \stackrel{\#}= 1 \Longleftrightarrow \exists x \, X = \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\({\tt n}\) が2以上の自然数のとき
=#\({\tt n}\) … \(X \stackrel{\#}= {\tt n} \Longleftrightarrow \exists^* x_{1} , \cdots , x_{\tt n} ( X = \{ x_{1} , \cdots , x_{\tt n} \} )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \stackrel{\#}\le \wp X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，Ax_s
Cantorの定理
\(X \stackrel{\rm S}\to \wp X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，Ax_s
inj. … \(\text{inj} _ ( n , k ) = [ \bullet ] | k \cup [ \bullet \textit{+1} ] | ( n \mathop\setminus k )\)
inj! … \(k \subset n \in \mathbb{M} \Longrightarrow \text{inj} _ ( n , k ) \in n \stackrel{\rm IS}\to n \textit{+1} \mathop\setminus \{ k \}\)
鳩の巣原理（部屋割り論法）
Le_le# … \(m , n \in \mathbb{M} , m \stackrel{\#}\le n \Longrightarrow m \subset n\) \(\blacktriangleleft\)
\(m \in \mathbb{M} , n \in \mathbb{M} , m \stackrel{\#}\le n \Longrightarrow m \subset n\) \(\blacktriangleleft\)
なぜか上のものダメ
n in |A and m in \M and f in m ->I n suc and n {/}in ^pr> (f) => m sub n
n in |A and m in \M and f in m ->I n suc and n = f (k) => m-1 sub n-1
\(m , n \in \mathbb{M} , m \subsetneq n \Longrightarrow \not\exists f f \in m \stackrel{\rm S}\to n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(n \in \mathbb{M} \Longrightarrow n \stackrel{\rm I}\to n = n \stackrel{\rm IS}\to n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(n \in \mathbb{M} \Longrightarrow n \stackrel{\rm S}\to n = n \stackrel{\rm IS}\to n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_1\)(,c) … \(\mathbb{V}_{\not\infty}\) \(\mathbb{V}_\infty\)
\Vf. … \(\mathbb{V}_{\not\infty} = \{ X \mid \exists n \in \mathbb{M} . X \stackrel{\#}= n \}\)
\(\mathbb{V}_{\not\infty} = \{ X \mid X \stackrel{\#}\le \mathbb{M} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\Vi. … \(\mathbb{V}_\infty = \mathop\setminus \mathbb{V}_{\not\infty}\)
wp_f. … \(\wp_{\not\infty} ( X ) = \wp ( X ) \cap \mathbb{V}_{\not\infty}\)
\(\wp_{\not\infty} ( \mathbb{M} ) \stackrel{\#}= \mathbb{M}\)
choice. … \(\text{choice} ( \mathcal{X} ) = \{ f \in \mathcal{X} \to \bigcup \mathcal{X} \mid \forall X , x \, ( \langle X , x \rangle \in f \Rightarrow x \in X ) \}\)
choice.' … \(\text{choice} ( \mathcal{X} ) = \{ f \in \mathcal{X} \to \mathbb{V} \mid \forall X \in \mathcal{X} . f ( X ) \in X \}\)
\(X = \{ x \} \Longrightarrow \text{choice} ( \{ X \} ) = \{ X \mathop{{\cdot}{\to}} x \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\emptyset \in \mathcal{X} \Longrightarrow \text{choice} ( \mathcal{X} ) = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ax_c … \(\emptyset \notin \mathcal{X} \Longrightarrow \text{choice} ( \mathcal{X} ) \neq \emptyset\)
\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \exists g \in Y \to X . f \circ g = \text{id} _ Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_c
ax_c -|
Dp. … \(x \in \Pi X \Longleftrightarrow \begin{cases} X \in \text{Map} \Longrightarrow x \in \triangleleft ( X ) \to \mathbb{V} , \forall \lambda \in \triangleleft ( X ) . x _ \lambda \in X _ \lambda \\ X \notin \text{Map} \Longrightarrow x \in \Pi X \end{cases}\)
Dp.' … \(X \in \Lambda \to \mathbb{V} \Longrightarrow \Pi X = \{ x \in \Lambda \to \mathbb{V} \mid \forall \lambda \in \Lambda . x _ \lambda \in X _ \lambda \}\)
\(X \in \Lambda \to \mathbb{V} , \emptyset \in \triangleright ( X ) \Longrightarrow \Pi X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
Dp_c … \(X \in \Lambda \to \mathbb{V} , \emptyset \notin \triangleright ( X ) \Longrightarrow \Pi X \neq \emptyset\)
abbr … \(X_{1} \times \cdots \times X_{\tt n}\) ≈ \(\times_{{\tt n}} ( X_{1} , \cdots , X_{\tt n} )\)
dp\({\tt n}\). … \(X_{1} \times \cdots \times X_{\tt n} = \{ \langle x_{1} , \cdots , x_{\tt n} \rangle \mid x_{1} \in X_{1} , \cdots , x_{\tt n} \in X_{\tt n} \}\)
dp\({\tt n}\).. … \(X_{1} \times \cdots \times X_{\tt n} = \{ f \in {\tt n} \to \mathbb{V} \mid f ( 0 ) \in X_{1} , \cdots , f ( {\tt n\,{\text -}\,1} ) \in X_{\tt n} \}\) \(\blacktriangleleft\)
dp\({\tt n}\)! … \(\times_{{\tt n}} ( X , \cdots , X ) = {\tt n} \to X\)
\(X \times Y \stackrel{\#}= Y \times X\) \(\blacktriangleleft\)
\(X \to ( Y \to Z ) \stackrel{\#}= X \times Y \to Z\) \(\blacktriangleleft\)
自然数についての議論では帰納法が良く使われます。証明ではメタの帰納法も使われます。
c1
0と後続関数
\(\mathbb{W}_0\)(,s) … \(0\)0. … \(x \in 0 \Longleftrightarrow {\perp}\)
0.' … \(0 = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(s,s) … \(\textit{+1}\) \(\textit{+1}\)
suc. … \(x \in n \textit{+1} \Longleftrightarrow x \in n \mathbin{\rm o\!r} x = n\)
suc.' … \(n \textit{+1} = n \cup \{ n \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
suc_. … \({\textit{+1}} \, \stackrel{\star}{=} {\stackrel{\text{^}}{\textit{+1}}}\)
帰納法
\(\mathbb{W}_1\)(,c) … \(\text{Ind}\)Ind. … \(\text{Ind} = \{ M \mid 0 \in M , \forall m \in M . m \textit{+1} \in M \}\)
Ind.' … \(\text{Ind} = \{ M \mid 0 \in M , M \textit{+1} \subset M \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(,s) … \(\mathbb{M}\)
ax_m … \(0 \in \mathbb{M}\)
\M. … \(\mathbb{M} = \bigcap \text{Ind}\)
\M1 … \(\forall n \in \mathbb{M} . n \textit{+1} \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\M1' … \(\mathbb{M} \textit{+1} \subset \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
<\M:i … \(n \in \mathbb{M} \Longrightarrow n \subset \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
省略形（須田作）\(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
\(\bigcup \mathbb{M} = \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
<\M:l … \(m \in n \in \mathbb{M} \Longrightarrow m \subsetneq n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
<\M:r … \(m , n \in \mathbb{M} , m \subsetneq n \Longrightarrow m \in n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
<\M:0 … \(m , n \in \mathbb{M} \Longrightarrow m \in n \Leftrightarrow m \subsetneq n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
<\M:1 … \(m , n \in \mathbb{M} \Longrightarrow m \subsetneq n \textit{+1} \Leftrightarrow m \subset n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
\(\mathbb{M} \subset \mathbb{V}_0\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
Cup\M … \(m \in \mathbb{M} \Longrightarrow \bigcup ( m \textit{+1} ) = m\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
<\M:T … \(m , n \in \mathbb{M} \Longrightarrow m \subset n \mathbin{\rm o\!r} n \subset m\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
自然数
1以上の自然数 \({\tt n}\) に対し word(,s) … \({\tt n}\)\({\tt n}\). … \(x \in {\tt n} \Longleftrightarrow x = 0 \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = {\tt n\,{\text -}\,1}\)
\({\tt n}\).' … \({\tt n} = \{ 0 , \cdots , {\tt n\,{\text -}\,1} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\({\tt n}\).. … \({\tt n} = ( {\tt n\,{\text -}\,1} ) \textit{+1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\({\tt n} \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m
2以上の自然数 \({\tt n}\) に対し
in\({\tt n}\) … \(0 \in 1 \in \cdots \in {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
neq\({\tt n}\) … \(0 \neq 1 , \cdots\!\cdots , {\tt n\,{\text -}\,2} \neq {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
subn\({\tt n}\) … \(0 \subsetneq 1 \subsetneq \cdots \subsetneq {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
subn\({\tt n}\)\(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_m ，Ax_s
neq壊れとる
列
1以上の自然数 \({\tt n}\) に対して\(\mathbb{W}_0\)(s\(^{\tt n}\),s)F … \(\mathsf{ary}_{\tt n}\)
abbr … \(\langle X_{1} , \cdots , X_{\tt n} \rangle\) ≈ \(\mathsf{ary}_{\tt n} ( X_{1} , \cdots , X_{\tt n} )\)
ary\({\tt n}\). … \(\langle x_{1} , \cdots , x_{\tt n} \rangle = \{ \langle 0 , x_{1} \rangle , \cdots , \langle {\tt n\,{\text -}\,1} , x_{\tt n} \rangle \}\)
ary\({\tt n}\)R … \(\langle x_{1} , \cdots , x_{\tt n} \rangle \in {\tt n} \to \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ary\({\tt n}\)L … \(f \in {\tt n} \to \mathbb{V} \Rightarrow f = \langle f ( 0 ) , \cdots , f ( {\tt n\,{\text -}\,1} ) \rangle\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ary\({\tt n}\)> … \(\triangleright ( \langle x_{1} , \cdots , x_{\tt n} \rangle ) = \{ x_{1} , \cdots , x_{\tt n} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ary\({\tt n}\)S … \(\langle x_{1} , \cdots , x_{\tt n} \rangle \in {\tt n} \stackrel{\rm S}\to \{ x_{1} , \cdots , x_{\tt n} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ary1IS … \(\langle x \rangle \in 1 \stackrel{\rm IS}\to \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
2以上の自然数 \({\tt n}\) に対して
ary\({\tt n}\)IS … \(x_{0} \neq x_{1} , \cdots\!\cdots , x_{\tt n\,{\text -}\,2} \neq x_{\tt n\,{\text -}\,1} \Longleftrightarrow \langle x_{0} , \cdots , x_{\tt n\,{\text -}\,1} \rangle \in {\tt n} \stackrel{\rm IS}\to \{ x_{0} , \cdots , x_{\tt n\,{\text -}\,1} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
c2
濃度①
\(\mathbb{W}_0\)(ss,p) … \(\stackrel{\#}=\) \(\stackrel{\#}\le\) \(\stackrel{\#}<\)=#. … \(X \stackrel{\#}= Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm IS}\to Y\)
=#.' … \(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
le#. … \(X \stackrel{\#}\le Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm I}\to Y\)
le#.' … \(X \stackrel{\#}\le Y \Longleftrightarrow X \stackrel{\rm I}\to Y \neq \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
<#. … \(X \stackrel{\#}< Y \Longleftrightarrow X \stackrel{\#}\le Y , X \stackrel{{\tt /}}{\stackrel{\#}=} Y\)
=:RTX … \({\stackrel{\#}=} :\mathsf{R}\&\mathsf{T}\&\mathsf{X}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=:C … \(X \stackrel{\#}= Y \Longleftrightarrow Y \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
le:RT … \({\stackrel{\#}\le} :\mathsf{R}\&\mathsf{T}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
濃度②
sub_le# … \(X \subset Y \Longrightarrow X \stackrel{\#}\le Y\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)Schröder-Bernsteinの定理
<:T … \(X \stackrel{\#}< Y \stackrel{\#}\le Z \mathbin{\rm o\!r} X \stackrel{\#}\le Y \stackrel{\#}< Z \Longrightarrow X \stackrel{\#}< Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=#0 … \(X \stackrel{\#}= \emptyset \Longleftrightarrow X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=#1 … \(X \stackrel{\#}= 1 \Longleftrightarrow \exists x \, X = \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\({\tt n}\) が2以上の自然数のとき
=#\({\tt n}\) … \(X \stackrel{\#}= {\tt n} \Longleftrightarrow \exists^* x_{1} , \cdots , x_{\tt n} ( X = \{ x_{1} , \cdots , x_{\tt n} \} )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
べき集合の濃度
=#wp … \(\wp X \stackrel{\#}= X \to 2\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，Ax_s\(X \stackrel{\#}\le \wp X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，Ax_s
Cantorの定理
\(X \stackrel{\rm S}\to \wp X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，Ax_s
c3
有限の補題
\(\mathbb{W}_0\)(ss,s) … \(\text{inj}\)inj. … \(\text{inj} _ ( n , k ) = [ \bullet ] | k \cup [ \bullet \textit{+1} ] | ( n \mathop\setminus k )\)
inj! … \(k \subset n \in \mathbb{M} \Longrightarrow \text{inj} _ ( n , k ) \in n \stackrel{\rm IS}\to n \textit{+1} \mathop\setminus \{ k \}\)
鳩の巣原理（部屋割り論法）
Le_le# … \(m , n \in \mathbb{M} , m \stackrel{\#}\le n \Longrightarrow m \subset n\) \(\blacktriangleleft\)
\(m \in \mathbb{M} , n \in \mathbb{M} , m \stackrel{\#}\le n \Longrightarrow m \subset n\) \(\blacktriangleleft\)
なぜか上のものダメ
n in |A and m in \M and f in m ->I n suc and n {/}in ^pr> (f) => m sub n
n in |A and m in \M and f in m ->I n suc and n = f (k) => m-1 sub n-1
\(m , n \in \mathbb{M} , m \subsetneq n \Longrightarrow \not\exists f f \in m \stackrel{\rm S}\to n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(n \in \mathbb{M} \Longrightarrow n \stackrel{\rm I}\to n = n \stackrel{\rm IS}\to n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(n \in \mathbb{M} \Longrightarrow n \stackrel{\rm S}\to n = n \stackrel{\rm IS}\to n\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
有限、無限
集合を有限と無限に分けます。\(\mathbb{W}_1\)(,c) … \(\mathbb{V}_{\not\infty}\) \(\mathbb{V}_\infty\)
\Vf. … \(\mathbb{V}_{\not\infty} = \{ X \mid \exists n \in \mathbb{M} . X \stackrel{\#}= n \}\)
\(\mathbb{V}_{\not\infty} = \{ X \mid X \stackrel{\#}\le \mathbb{M} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\Vi. … \(\mathbb{V}_\infty = \mathop\setminus \mathbb{V}_{\not\infty}\)
有限部分集合の全体
\(\mathbb{W}_0\)(s,s) … \(\wp_{\not\infty}\)wp_f. … \(\wp_{\not\infty} ( X ) = \wp ( X ) \cap \mathbb{V}_{\not\infty}\)
\(\wp_{\not\infty} ( \mathbb{M} ) \stackrel{\#}= \mathbb{M}\)
c4
選択写像
\(\mathbb{W}_0\)(s,s)F … \(\text{choice}\)choice. … \(\text{choice} ( \mathcal{X} ) = \{ f \in \mathcal{X} \to \bigcup \mathcal{X} \mid \forall X , x \, ( \langle X , x \rangle \in f \Rightarrow x \in X ) \}\)
choice.' … \(\text{choice} ( \mathcal{X} ) = \{ f \in \mathcal{X} \to \mathbb{V} \mid \forall X \in \mathcal{X} . f ( X ) \in X \}\)
\(X = \{ x \} \Longrightarrow \text{choice} ( \{ X \} ) = \{ X \mathop{{\cdot}{\to}} x \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\emptyset \in \mathcal{X} \Longrightarrow \text{choice} ( \mathcal{X} ) = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
ax_c … \(\emptyset \notin \mathcal{X} \Longrightarrow \text{choice} ( \mathcal{X} ) \neq \emptyset\)
\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \exists g \in Y \to X . f \circ g = \text{id} _ Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax_c
ax_c -|
直積
\(\mathbb{W}_0\)(s,s) … \(\Pi\)Dp. … \(x \in \Pi X \Longleftrightarrow \begin{cases} X \in \text{Map} \Longrightarrow x \in \triangleleft ( X ) \to \mathbb{V} , \forall \lambda \in \triangleleft ( X ) . x _ \lambda \in X _ \lambda \\ X \notin \text{Map} \Longrightarrow x \in \Pi X \end{cases}\)
Dp.' … \(X \in \Lambda \to \mathbb{V} \Longrightarrow \Pi X = \{ x \in \Lambda \to \mathbb{V} \mid \forall \lambda \in \Lambda . x _ \lambda \in X _ \lambda \}\)
\(X \in \Lambda \to \mathbb{V} , \emptyset \in \triangleright ( X ) \Longrightarrow \Pi X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
Dp_c … \(X \in \Lambda \to \mathbb{V} , \emptyset \notin \triangleright ( X ) \Longrightarrow \Pi X \neq \emptyset\)
有限直積
\(\mathbb{W}_0\)(s\(^{\tt n}\),s)F … \(\times_{{\tt n}}\)abbr … \(X_{1} \times \cdots \times X_{\tt n}\) ≈ \(\times_{{\tt n}} ( X_{1} , \cdots , X_{\tt n} )\)
dp\({\tt n}\). … \(X_{1} \times \cdots \times X_{\tt n} = \{ \langle x_{1} , \cdots , x_{\tt n} \rangle \mid x_{1} \in X_{1} , \cdots , x_{\tt n} \in X_{\tt n} \}\)
dp\({\tt n}\).. … \(X_{1} \times \cdots \times X_{\tt n} = \{ f \in {\tt n} \to \mathbb{V} \mid f ( 0 ) \in X_{1} , \cdots , f ( {\tt n\,{\text -}\,1} ) \in X_{\tt n} \}\) \(\blacktriangleleft\)
dp\({\tt n}\)! … \(\times_{{\tt n}} ( X , \cdots , X ) = {\tt n} \to X\)
\(X \times Y \stackrel{\#}= Y \times X\) \(\blacktriangleleft\)
\(X \to ( Y \to Z ) \stackrel{\#}= X \times Y \to Z\) \(\blacktriangleleft\)