5 自然数と2項演算

5.1 2項演算

word+(s[ss,s],p)R … \(:\underline{2}\)  \(:\mathsf{C}\)  \(:\mathsf{A}\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\underline{2}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y \in X\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\mathsf{C}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y = y \mathbin{{\sf f}} x\)
lower … \(( X , [\mathbin{{\sf f}}] ) :\mathsf{A}\) ≃ \(\forall x , y , z \in X . x \mathbin{{\sf f}} \, ( y \mathbin{{\sf f}} z ) = ( x \mathbin{{\sf f}} y ) \mathbin{{\sf f}} z\)
word+(s[ss,s][ss,s],p)R … \(:\underline{2}_2\)  \(:\mathsf{C}_2\)  \(:\mathsf{A}_2\)  \(:\mathsf{D}\)
lower … \(( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) :\underline{2}_2\) ≃ \(( X , [\mathbin{{\sf f}}] ) :\underline{2} , ( X , [\mathbin{{\sf g}}] ) :\underline{2}\)
lower … \(( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) :\mathsf{C}_2\) ≃ \(( X , [\mathbin{{\sf f}}] ) :\mathsf{C} , ( X , [\mathbin{{\sf g}}] ) :\mathsf{C}\)
lower … \(( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) :\mathsf{A}_2\) ≃ \(( X , [\mathbin{{\sf f}}] ) :\mathsf{A} , ( X , [\mathbin{{\sf g}}] ) :\mathsf{A}\)
lower … \(( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) :\mathsf{D}\) ≃ \(\forall x , y , z \in X . x \mathbin{{\sf g}} \, ( y \mathbin{{\sf f}} z ) = ( x \mathbin{{\sf g}} y ) \mathbin{{\sf f}} \, ( x \mathbin{{\sf g}} z )\)
word+(s[ss,s],c) … \(\text{unit}\)
lower … \(\text{unit} ( X , [\mathbin{{\sf f}}] )\) ≃ \(\{ e \in X \mid \forall x \in X . e \mathbin{{\sf f}} x = x = x \mathbin{{\sf f}} e \}\)
word+(s[ss,s][ss,s],p)R … \(\text{csemiring}\)
lower … \(( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) \text{csemiring}\) ≃ \(( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) :\underline{2}_2 , ( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) :\mathsf{C}_2 , ( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) :\mathsf{A}_2 , 0 \in X , 1 \in X , 0 \in \text{unit} ( X , [\mathbin{{\sf f}}] ) , 1 \in \text{unit} ( X , [\mathbin{{\sf g}}] ) , ( X , [\mathbin{{\sf f}}] , [\mathbin{{\sf g}}] ) :\mathsf{D} , \forall x \in X . 0 \mathbin{{\sf g}} x = 0\)

5.2 自然数の加法

加法は次の漸化式を仮定として置きます。
+𝕄 … \(\begin{cases} m \in \mathbb{M} \Longrightarrow m + 0 = m \\ m , n \in \mathbb{M} \Longrightarrow m + ( n + 1 ) = ( m + n ) + 1 \end{cases}\)
+𝕄:2 … \(( \mathbb{M} , [+] ) :\underline{2}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
交わらない \(m\) 個と \(k\) 個を合わせると \(m + k\) 個（\(k\) についての帰納法）。
∪=#+ … \(X \cap Y = \emptyset , X \stackrel{\#}= m \in \mathbb{M} , Y \stackrel{\#}= k \in \mathbb{M} \Longrightarrow X \cup Y \stackrel{\#}= m + k \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L×1 … \(X \times \{ c \} \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
Lmn … \(m , n \in \mathbb{M} \Longrightarrow \exists M , N \, M \stackrel{\#}= m , N \stackrel{\#}= n , M \cap N = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s
+𝕄:C … \(( \mathbb{M} , [+] ) :\mathsf{C}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
+𝕄:A … \(( \mathbb{M} , [+] ) :\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄

5.3 自然数の乗法

word(ss,s) … \(\cdot\)
⋅𝕄 … \(\begin{cases} m \in \mathbb{M} \Longrightarrow m \cdot 0 = 0 \\ m , n \in \mathbb{M} \Longrightarrow m \cdot ( n + 1 ) = m \cdot n + m \end{cases}\)
⋅𝕄:2 … \(( \mathbb{M} , [\cdot] ) :\underline{2}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
⋅=# … \(m , n \in \mathbb{M} \Longrightarrow m \cdot n \stackrel{\#}= m \times n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
各 \(s \in S\) の \(c\) での値が \(Y\) の元で、値が \(a\) のもの全体がどの \(a \in Y\) でも \(q\) 個なら、\(S\) は \(q \cdot k\) 個（\(Y\) は \(k\) 個）。
LΣ … \(Y \stackrel{\#}= k \in \mathbb{M} , q \in \mathbb{M} , \forall s \in S . \exists a \in Y . \langle c , a \rangle \in s , \forall s \in S . \forall a , b \, ( \langle c , a \rangle \in s , \langle c , b \rangle \in s \Longrightarrow a = b ) , \forall a \in Y . \forall F \, ( \forall s \, ( s \in F \Longleftrightarrow s \in S , \langle c , a \rangle \in s ) \Longrightarrow F \stackrel{\#}= q ) \Longrightarrow S \stackrel{\#}= q \cdot k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
⋅𝕄+ … \(( \mathbb{M} , [+] , [\cdot] ) :\mathsf{D}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
0⋅ … \(m \in \mathbb{M} \Longrightarrow 0 \cdot m = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
+1⋅ … \(m , n \in \mathbb{M} \Longrightarrow ( m + 1 ) \cdot n = m \cdot n + n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
⋅𝕄:C … \(( \mathbb{M} , [\cdot] ) :\mathsf{C}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
⋅𝕄:A … \(( \mathbb{M} , [\cdot] ) :\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
L⋅1 … \(m \in \mathbb{M} \Longrightarrow m \cdot 1 = m , 1 \cdot m = m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
\(1 \in \text{unit} ( \mathbb{M} , [\cdot] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
\(0 \in \text{unit} ( \mathbb{M} , [+] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
𝕄 は加法を +、乗法を ⋅ とする可換半環（csemiring）。
\(( \mathbb{M} , [+] , [\cdot] ) \text{csemiring}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

5.4 自然数のべき

word(ss,s) … ↑
word+(ss,s) … \(\uparrow\) ≃ ↑
↑𝕄 … \(\begin{cases} m ^ 0 = 1 \\ n \in \mathbb{M} \Longrightarrow m ^ { n + 1 } = m ^ n \cdot m \end{cases}\)
↑𝕄:2 … \(( \mathbb{M} , [\uparrow] ) :\underline{2}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄
2乗は、単位元をもつ集合 \(S\) の上でならその積（底が 𝕄 でなくてよい）。
↑2 … \(m \in S , 1 \in \text{unit} ( S , [\cdot] ) \Longrightarrow m ^ 2 = m \cdot m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，↑𝕄
自然数の2乗は積。
↑2𝕄 … \(m \in \mathbb{M} \Longrightarrow m ^ 2 = m \cdot m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄
自然数の3乗は積。
↑3𝕄 … \(m \in \mathbb{M} \Longrightarrow m ^ 3 = m \cdot ( m \cdot m )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄
乗法で閉じていて 1 を含む集合 \(S\) の元のべきは \(S\) の元。
↑∈S … \(( S , [\cdot] ) :\underline{2} , 1 \in S , r \in S , n \in \mathbb{M} \Longrightarrow r ^ n \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，↑𝕄
0・1 を含み加法で閉じている集合は、自然数をすべて含む（+ と ⋅ は全体で共通なので、自然数の S への埋め込みは要らない）。
𝕄⊂S … \(( S , [+] ) :\underline{2} , 0 \in S , 1 \in S , n \in \mathbb{M} \Longrightarrow n \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
可換半環では右分配も成り立つ。
Rdist-S … \(( S , [+] , [\cdot] ) \text{csemiring} , x , y , z \in S \Longrightarrow ( x + y ) \cdot z = x \cdot z + y \cdot z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
可換半環の元 \(x\) について \(2x = x + x\)、自然数 \(m\) について \((m+1)x = mx + x\)。
L2⋅S … \(( S , [+] , [\cdot] ) \text{csemiring} , x \in S \Longrightarrow 2 \cdot x = x + x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
+1⋅S … \(( S , [+] , [\cdot] ) \text{csemiring} , m \in \mathbb{M} , n \in S \Longrightarrow ( m + 1 ) \cdot n = m \cdot n + n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄

5.5 自然数の階乗

word(s,s) … \(!\)
階乗は次の漸化式を仮定として置きます。
!𝕄 … \(\begin{cases} 0 ! = 1 \\ n \in \mathbb{M} \Longrightarrow ( n + 1 ) ! = n ! \cdot ( n + 1 ) \end{cases}\)
!∈𝕄 … \(n \in \mathbb{M} \Longrightarrow n ! \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄