1 自然数

1.1 代数の言葉

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],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 … \(:\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 )\)

1.2 自然数の記号、加法

0以上の自然数\({\tt n}\)に対し
word(,s) … \({\tt n}\)
word(,s) … \(\mathbb{M}\)  \(\mathbb{N}\)
ℕ. … \(\mathbb{N} = \{ n \in \mathbb{M} \mid n \neq 0 \}\)

word(ss,s) … \(+\)  \(+\)  \(+\)  \(+\)
*^+. … \([+] \stackrel{\star\!\star}{=} \; [\stackrel{\text{*^}}{+}]\)
^*+. … \([+] \stackrel{\star\!\star}{=} \; [\stackrel{\text{^*}}{+}]\)
^^+. … \([+] \stackrel{\star\!\star}{=} \; [\stackrel{\text{^^}}{+}]\)

1以上の自然数\({\tt n}\)に対し
\({\tt n}\). … \({\tt n} = ( {\tt n\,{\text -}\,1} ) + 1\)
Peano1 … \(n \in \mathbb{M} \Longrightarrow n + 1 \in \mathbb{N}\)
Peano2 … \(m , n \in \mathbb{M} , m + 1 = n + 1 \Longrightarrow m = n\)
INDC … \(0 \in D , \forall m \in \mathbb{M} . ( m \in D \Longrightarrow m + 1 \in D ) \Longrightarrow \mathbb{M} \subset D\)
+𝕄 … \(\begin{cases} m \in \mathbb{M} \Longrightarrow m + 0 = m \\ m , n \in \mathbb{M} \Longrightarrow m + ( n + 1 ) = ( m + n ) + 1 \end{cases}\)
Ax+𝕄 … Peano1 ，Peano2 ，INDC ，+𝕄 ，\(0 \in \mathbb{M}\)
\({\tt n} \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄

1.3 加法の性質

+𝕄:2 … \(( \mathbb{M} , [+] ) :\underline{2}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄
\(0 \in \text{unit} ( \mathbb{M} , [+] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄
+𝕄:C … \(( \mathbb{M} , [+] ) :\mathsf{C}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄
+𝕄:A … \(( \mathbb{M} , [+] ) :\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄
\(\mathbb{N} = \mathbb{M} + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄

1.4 乗法

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}\)
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} , [\cdot] ) :\underline{2}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
⋅𝕄:C … \(( \mathbb{M} , [\cdot] ) :\mathsf{C}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
⋅𝕄+ … \(( \mathbb{M} , [+] , [\cdot] ) :\mathsf{D}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
⋅𝕄:A … \(( \mathbb{M} , [\cdot] ) :\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
⋅𝕄:1 … \(1 \in \text{unit} ( \mathbb{M} , [\cdot] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄

1.5 三分律

Lz0 … \(x , y \in \mathbb{M} , x + y = 0 \Longrightarrow x = 0 , y = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄
Ltri … \(m , n \in \mathbb{M} \Longrightarrow \exists k \in \mathbb{M} . m = n + k \mathbin{\rm o\!r} \exists k \in \mathbb{M} . n = m + k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄