1 - c　自然数、有限・無限

c1

自然数を作ります。帰納法が強力な道具になりますが、メタの帰納法も使われます。

自然数

word(,s) … 0
0.'【\(0 = \emptyset\)】

0以上の自然数全体を作ってしまいます。
word(,s) … \(\mathbb{M}\)
【\(0 \in \mathbb{M}\)】は公理になります。

後置される後続関数を準備します。
word(s,s) … \(\textit{+1}\) \(\textit{+1}\)
suc.'【\(n \textit{+1} = n \cup \{ n \}\)】
suc_.【\(\textit{+1} \, \,^\star{=}\; {\textit{+1}}\)】

帰納法

word(,c) … \(\text{Ind}\)
Ind.'【\(\text{Ind} = \{ M \mid 0 \in M , M \textit{+1} \subset M \}\)】
帰納法を使うときは \Mi ≅ \M を使用します。
\Mi.【\(\mathbb{M} = \bigcap \text{Ind}\)】
\Mi1'【\(\mathbb{M} \textit{+1} \subset \mathbb{M}\)】\(\blacktriangleleft\)
【\(\bigcup \mathbb{M} = \mathbb{M}\)】\(\blacktriangleleft\)

<\M0【\( m , n \in \mathbb{M} \Longrightarrow m \in n \Leftrightarrow m \subsetneq n\)】\(\blacktriangleleft\)
<\M1【\( m , n \in \mathbb{M} \Longrightarrow m \subsetneq n \textit{+1} \Leftrightarrow m \subset n\)】\(\blacktriangleleft\)
【\(\mathbb{M} \subset \mathbb{V}_1\)】\(\blacktriangleleft\)
\(\bigcup\) が先行関数になります。
Cup\M【\(m \in \mathbb{M} \Longrightarrow \bigcup ( m \textit{+1} ) = m\)】\(\blacktriangleleft\)
\(\mathbb{M}\)は全順序になります。
<\M_T【\( m , n \in \mathbb{M} \Longrightarrow m \subset n \mathbin{\rm o\!r} n \subset m\)】\(\blacktriangleleft\)

メタからの自然数の作成

1以上の自然数 \({\tt n}\) に対し word(,s) … \({\tt n}\)
私たちは十進法を使用するので、「1以上の自然数」とは [1-9][0-9]* です。

自然数を集合と思う時にはvon Neumann流の定義を採用します。
\({\tt n}\).'【\({\tt n} = \{ 0 , 1 , \cdots , {\tt n\,{\text -}\,1} \}\)】
\({\tt n}\)..【\({\tt n} = {\tt n\,{\text -}\,1} \textit{+1}\)】\(\blacktriangleleft\)
次のThmは \({\tt n}\geq0\) のメタ帰納法で示されます。
【\({\tt n} \in \mathbb{M}\)】\(\blacktriangleleft\)

2以上の自然数 \({\tt n}\) に対しては、次の長いFormを準備します。
in\({\tt n}\)【\(0 \in 1 \in \cdots \in {\tt n\,{\text -}\,1}\)】\(\blacktriangleleft\)
subn\({\tt n}\)【\(0 \subsetneq 1 \subsetneq \cdots \subsetneq {\tt n\,{\text -}\,1}\)】\(\blacktriangleleft\)
neq\({\tt n}\)【\(0 \neq 1 , 0 \neq 2 , \cdots , {\tt n\,{\text -}\,2} \neq {\tt n\,{\text -}\,1}\)】

c2

列を作ります。\({\tt n}\)=2 だと順序対と同じ表記になります。

列

1以上の自然数 \({\tt n}\) に対して
word(s\(^{\tt n}\),s)F … \(\text{ary}_{{\tt n}}\)
abbr …【\(\langle x_{1} , \cdots , x_{\tt n} \rangle\)】≈【\(\text{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}\)!【\(\langle x_{1} , \cdots , x_{\tt n} \rangle \in \text{mapon} ( {\tt n} )\)】\(\blacktriangleleft\)
ary\({\tt n}\)!!【\(f \in \text{mapon} ( {\tt n} ) \Longrightarrow f = \langle f ( 0 ) , \cdots , f ( {\tt n\,{\text -}\,1} ) \rangle\)】\(\blacktriangleleft\)

1以上の自然数 \({\tt n}\) に対して
word(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} )\)】
times\({\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} \}\)】
times\({\tt n}\)..【\(X_{1} \times \cdots \times X_{\tt n} = \{ f \in \text{mapon} ( {\tt n} ) \mid f ( 0 ) \in X_{1} , \cdots , f ( {\tt n\,{\text -}\,1} ) \in X_{\tt n} \}\)】\(\blacktriangleleft\)
times\({\tt n}\)!【\(\times_{{\tt n}} ( X , \cdots , X ) = {\tt n} \to X\)】

列の性質

ary1IS【\(\langle x \rangle \in 1 \stackrel{\rm IS}\to \{ x \}\)】\(\blacktriangleleft\)
2以上の自然数 \({\tt n}\) に対して
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\)
ary\({\tt n}\)IS【\(x_{1} \neq x_{2} , \cdots \Longleftrightarrow \langle x_{1} , \cdots , x_{\tt n} \rangle \in {\tt n} \stackrel{\rm IS}\to \{ x_{1} , \cdots , x_{\tt n} \}\)】\(\blacktriangleleft\)
n=4でも30秒以上かかっちゃう…

=#1【\(X \stackrel{\#}= 1 \Longleftrightarrow \exists x \, X = \{ x \}\)】\(\blacktriangleleft\)
=#\({\tt n}\)【\(X \stackrel{\#}= {\tt n} \Longleftrightarrow \exists^* x_{1} , \cdots , x_{\tt n} \, X = \{ x_{1} , \cdots , x_{\tt n} \}\)】\(\blacktriangleleft\)
未
`f in n ->S X => X =s {set f ap (0) ; f ap (1) ; … ; f ap (n-1)}` / ->S.. / ->.. // W. ＜ n.
Le / ->S.. / ->.. // W. ＜ n. ;; Le := `f in n ->S X => X =s {set f ap (0) ; f ap (1) ; … ; f ap (n-1)}`

neq2 が必要なハズ。<=ではaryも

有限の補題

word(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} \Rightarrow \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 im (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\)
【\(n \in \mathbb{M} \Longrightarrow n \stackrel{\rm I}\to n = n \stackrel{\rm IS}\to n\)】\(\blacktriangleleft\)
【\(n \in \mathbb{M} \Longrightarrow n \stackrel{\rm S}\to n = n \stackrel{\rm IS}\to n\)】\(\blacktriangleleft\)

有限、無限

集合を有限と無限に分けます。
word(,c) … \(\mathbb{V}_{\not\infty}\) \(\mathbb{V}_\infty\)
cvt …【\(\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\)
cvt …【\(\mathbb{V}_\infty\)】≃【\(\mathop\setminus \mathbb{V}_{\not\infty}\)】

c3

自然数の加法

word(ss,s) … \(+\) \(+\) \(+\) \(+\)
+l.【\(+ \,^{\star\!\star}{=}\; {+}\)】　+r.【\(+ \,^{\star\!\star}{=}\; {+}\)】　+_.【\(+ \,^{\star\!\star}{=}\; {+}\)】
\(\{ 0 , 1 \} + 2 = \{ 2 , 3 \}\) となるべきです。

+\M【\(\begin{cases} m \in \mathbb{M} \Longrightarrow m + 0 = m \\ m , n \in \mathbb{M} \Longrightarrow m + ( n \textit{+1} ) = ( m + n ) \textit{+1} \end{cases}\)】
【\(m \in \mathbb{M} \Longrightarrow m + 1 = m \textit{+1}\)】\(\blacktriangleleft\)
+\M0'【\(\mathbb{M} + \mathbb{M} \subset \mathbb{M}\)】\(\blacktriangleleft\)

【\(n \in \mathbb{M} \Longrightarrow 0 + n = n\)】\(\blacktriangleleft\)
【\( m , n \in \mathbb{M} \Longrightarrow m + n = n + m\)】
【\( m , n , k \in \mathbb{M} \Longrightarrow m + ( n + k ) = ( n + m ) + k\)】

0+n=n、可換則、結合則なんかは濃度を使って証明した方が良い？

自然数の乗法

word(ss,s) … \(\cdot\) \(\cdot\) \(\cdot\) \(\cdot\)
*l.【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】　*r.【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】　*_.【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】
\(\{ 0 , 1 \} \cdot 2 = \{ 0 , 2 \}\) となるべきです。

*\M【\(\begin{cases} m \in \mathbb{M} \Longrightarrow m \cdot 0 = 0 \\ m , n \in \mathbb{M} \Longrightarrow m \cdot ( n \textit{+1} ) = ( m \cdot n ) + m \end{cases}\)】
*\M0'【\(\mathbb{M} \cdot \mathbb{M} \subset \mathbb{M}\)】\(\blacktriangleleft\)

【\(n \in \mathbb{M} \Longrightarrow 0 \cdot n = 0\)】\(\blacktriangleleft\)

加法・乗法の諸法則は1-dで証明されます。

自然数の順序

大小は加法を使って作ることもできる
【\(i \in \mathbb{M} \Rightarrow \{ n \in \mathbb{M} \mid i \subset n \} = i + \mathbb{M}\)】
`i in \M => {cls n in \M | i sub n } =_ i +r \M` / +r. => ＜ Le1 ,, M_i. ,, \Mi. ;; Le1 / W.!!sub. ＜ `0 in \M` ,, \Mi1 ,, +\M ,, Le2 ,, <\M1 / subn.. ;; Le2 // W. ＜ O ;; Le1 := `i in \M => M_i(i) in_ Ind` ;; Le2 := `x sub 0 => x =s 0`
準備　M_i.【\(M_i ( i ) = \{ n \in \mathbb{M} \mid i \subset n \Rightarrow \exists m \in \mathbb{M} . n = i + m \}\)】
`i in \M => {cls n in \M | i sub n } =_ i +r \M` / W. ＜ \Mi. ,, Le2 ,, M_i. ;; Le1 := `i in \M => M_i(i) in_ Ind`ダメ

有限の計算

直和の濃度
【\( m , n \in \mathbb{M} \Longrightarrow ( 1 \times m ) \cup ( n \times 1 ) \stackrel{\#}= m + n\)】\(\blacktriangleleft\)

集合の直和作る？
\(m+n = \{0\}\times m \cup \{1\}\times n\)

1 - c 自然数、有限・無限

c1

自然数

帰納法