1 - c　自然数、有限・無限 - test2.atp-research.com

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} \, \stackrel{\star}{=} \stackrel{\text{^}}{\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 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\)
\(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. … \(+ \stackrel{\star\!\star}{=} \stackrel{｛l｝}{+}\) 　+r. … \(+ \stackrel{\star\!\star}{=} \stackrel{｛r｝}{+}\) 　+_. … \(+ \stackrel{\star\!\star}{=} \stackrel{\text{^^}}{+}\)
\(\{ 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 \stackrel{\star\!\star}{=} \stackrel{\text{^*}}{\cdot}\) 　*r. … \(\cdot \stackrel{\star\!\star}{=} \stackrel{\text{*^}}{\cdot}\) 　*_. … \(\cdot \stackrel{\star\!\star}{=} \stackrel{\text{^^}}{\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 \text{cls} 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

自然数

帰納法