エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

エレファントな整数論(6)

 \mathbb{N} (自然数全体の集合)と数学的帰納法の関係を考察したので、ここからは数学的帰納法の原理が成り立つ  \mathbb{N} が存在するとして進めます。

整数の加法

 a \in \mathbb{N} に対して  -a

  •  -0 = 0
  •  -(a + 1) = (-a) + s^{-1}

と定義します。 s^{-1} = -1 となります。

 \begin{eqnarray*}
& & (-a) + (-1) = (-1) + (-a) \\
& \Leftarrow & (-(a-1)) + (-1) + (-1) = (-1) + (-(a-1)) + (-1) \\
& \Leftarrow & (-(a-1)) + (-1) = (-1) + (-(a-1)) \\
& \Leftarrow & (-(a-2)) + (-1) = (-1) + (-(a-2)) \\
& \Leftarrow & \cdots \Leftarrow (-(a-a)) + (-1) = (-1) + (-(a-a)) \Leftarrow -1 = -1
\end{eqnarray*}

  • 任意の  a \in \mathbb{N} に対して  (-a) + (-1) = (-1) + (-a)

 (-a) + 1 = 1 + (-1) + (-a) + 1 = 1 + (-a) + (-1) + 1 = 1 + (-a)

  • 任意の  a \in \mathbb{N} に対して  (-a) + 1 = 1 + (-a)

 a + (-b) = (a - 1) + 1 + (-b) = (a - 1) + (-b) + 1 = (a - 2) + (-b) + 2 \\ = \cdots = (a - a) + (-b) + a = (-b) + a

  • (Z5) 任意の  a, b \in \mathbb{N} に対して  a + (-b) = (-b) + a

 a + (-a) = (a - 1) + 1 + (-(a - 1)) + (-1) = (a - 1) + (-(a - 1)) \\ = (a - 2) + (-(a - 2)) = \cdots = (a - a) + (-(a - a)) = 0

  • (Z4) 任意の  a \in \mathbb{N} に対して  a + (-a) = (-a) + a = 0

 -(a + b) = (-(a + b - 1)) + (-1) = (-(a + b - 2)) + (-2) \\ = \cdots = = (-(a + b - b)) + (-b) = (-a) + (-b)

  • (Z1) 任意の  a, b \in \mathbb{N} に対して  -(a + b) = (-a) + (-b)
  • (Z6) 任意の  a, b \in \mathbb{N} に対して  (-a) + (-b) = (-b) + (-a)

 a \ge b のとき  a = b + c となる  c \in \mathbb{N} が存在します。 c = a \setminus b と書くと

  • (Z2) 任意の  a, b \in \mathbb{N} に対して  a + (-b) = b + c + (-b) = c = a \setminus b
  • (Z3) 任意の  a, b \in \mathbb{N} に対して  (-a) + b = (-(b + c)) + b = (-c) + (-b) + b = -c = -(a \setminus b)

となります。

 \mathbb{N} は可換なモノイドなので、 \mathbb{N}^- = \{ -a \mid a \in \mathbb{N} \} \mathbb{Z} = \mathbb{N} \cup \mathbb{N}^- とおくと(Z1)、(Z2)、(Z3)より  \mathbb{Z} + (写像の合成)に関して閉じています。(Z4)より逆元が存在するので  \mathbb{Z} は群となります。 \mathbb{Z} 1 を含む最小の(全単射全体の群の)部分群となります。(Z5)、(Z6)より  \mathbb{Z} はアーベル群となります。

 a, b \in \mathbb{Z} に対して  a - b = a + (-b) と定義します。(Z2)より  a, b \in \mathbb{N} a \ge b のとき  a - b = a \setminus b となります。