1 自然数の演算

1.1 準備

2.book の隠し補題のうち、この Book で使うものを写しました（隠し補題は import で引き継がれないため）。

1.2 加法

2.book では加法と乗法を定義せず、再帰の等式 +𝕄・*𝕄 を仮定として使います。この Book はその別案として、途中経過の列 \(h\) を使って \(+\)・\(\cdot\) を定義し、+𝕄・*𝕄 を定理として示したものです（2026-09-29 作成・2.book から移動）。
\(m + n\) は \(m\) から始めて \({\rm suc}\) を \(n\) 回施したものです。途中経過の列 \(h\)（\(h\) は \(k+1\) 上の写像で \(h(0)=m\)、\(h(i+1)=h(i)+1\)）を使って定義します。
+. … \(\exists! w \exists k , h \, \begin{cases} k \in \mathbb{M} \\ h \in k \textit{+1} \to \mathbb{M} \\ \langle 0 , m \rangle \in h \\ \forall i \in k . \forall u ( \langle i , u \rangle \in h \Longrightarrow \langle i \textit{+1} , u \textit{+1} \rangle \in h ) \\ \langle n , w \rangle \in h \end{cases} \Longrightarrow ( m + n = y \Leftrightarrow \exists k , h \, \begin{cases} k \in \mathbb{M} \\ h \in k \textit{+1} \to \mathbb{M} \\ \langle 0 , m \rangle \in h \\ \forall i \in k . \forall u ( \langle i , u \rangle \in h \Longrightarrow \langle i \textit{+1} , u \textit{+1} \rangle \in h ) \\ \langle n , y \rangle \in h \end{cases} )\)
+𝕄 … \(\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}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
+∈𝕄 … \(m , n \in \mathbb{M} \Longrightarrow m + n \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

1.3 乗法

\(m \cdot n\) は \(0\) から始めて \(m\) を \(n\) 回足したものです。加法と同じく途中経過の列 \(h\)（\(h(0)=0\)、\(h(i+1)=h(i)+m\)）で定義します。
⋅. … \(\exists! w \exists k , h \, \begin{cases} k \in \mathbb{M} \\ h \in k \textit{+1} \to \mathbb{M} \\ \langle 0 , 0 \rangle \in h \\ \forall i \in k . \forall u ( \langle i , u \rangle \in h \Longrightarrow \langle i \textit{+1} , u + m \rangle \in h ) \\ \langle n , w \rangle \in h \end{cases} \Longrightarrow ( m \cdot n = y \Leftrightarrow \exists k , h \, \begin{cases} k \in \mathbb{M} \\ h \in k \textit{+1} \to \mathbb{M} \\ \langle 0 , 0 \rangle \in h \\ \forall i \in k . \forall u ( \langle i , u \rangle \in h \Longrightarrow \langle i \textit{+1} , u + m \rangle \in h ) \\ \langle n , y \rangle \in h \end{cases} )\)
*𝕄 … \(\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}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
⋅∈𝕄 … \(m , n \in \mathbb{M} \Longrightarrow m \cdot n \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s