整数の定義が納得いかないので自然な定義を作った

$$ \begin{flalign*} 1+1 &= 1+S(0)\\ &= S(1+0) \\ &= S(1) \\ &= 2 \end{flalign*} $$

$(a,b)\sim'(c,d) :⇔ a+d=b+c$とする．

• $\sim'$が同値関係であることを示す．
  1. $a+b = b+a$より、$(a,b)\sim'(a,b)$
  2. $a+d=b+c ⇔ c+b=d+a$より、$(a,b)\sim'(c,d) ⇔ (c,d)\sim'(a,b)$
  3. $(a,b)\sim'(c,d) \land (c,d)\sim'(e,f)$と仮定すると、
     $a+d=b+c \land c+f=d+e$
     $\Rightarrow (a+d)+(c+f)=(b+c)+(d+e)$
     $\Rightarrow a+f+(c+d)=b+e+(c+d)$
     $\Rightarrow a+f=b+e$
     $\Rightarrow (a,b)\sim'(e,f)$
     よって、$(a,b)\sim'(c,d) \land (c,d)\sim'(e,f) \Rightarrow (a,b)\sim'(e,f)$

　$\therefore\ \sim'$は同値関係

• $\sim'$が定義9.1を満たすことを示す．
  $a+b=b+a$
  $\Rightarrow S(a+b) = S(b+a)$
  $\Rightarrow a+S(b) = b+S(a)$
  $\Rightarrow (a,b)\sim'(S(a),S(b))$
  よって，$\sim'$は定義9.1を満たす．

• $\sim'$が定義9.2を満たすことを示す．
  $R\in Eq(\mathbb{N}^2) \land (\forall a,b\in \mathbb{N},\ (a,b)R(S(a),S(b)))$を満たす$R$を一つ取る．
  ☆ $\forall a,b,c\in\mathbb{N},\ (a,b)R(a+c,b+c)$を示す．

1. $c=0$のとき，
   $(a,b)=(a+0,b+0)$より$(a,b)R(a+0,b+0)$
2. $c=k$のとき，$(a,b)R(a+k,b+k)$と仮定すると，
   \begin{align} (a+k,b+k)R&(S(a+k),S(b+k)) \\ =&(a+S(k),b+S(k))\ \text{から} \\ (a+k,b+k)R&(a+S(k),b+S(k)) \end{align}
   推移律より，$(a,b)R(a+S(k),b+S(k))$
   よって、$c=S(k)$ のとき成り立つ．

　$\therefore \forall a,b,c\in\mathbb{N},\ (a,b)R(a+c,b+c)$

　$(a,b)\sim'(c,d)$と仮定すると、
　$a+d = b+c$
　☆より，
　$(a,b)R(a+d,b+d)$
　$(c,d)R(c+b,d+b)$
　また，$(a+d,b+d)=(c+b,d+b)$
　よって推移律により，$(a,b)R(c,d)$が言えるので，
　$\sim'\subseteq R$
　従って，$\sim'$は定義9.2を満たす．

• 定義9を満たす同値関係が一意であることを示す．
  同値関係$\sim_1,\sim_2$がともに定義9を満たすと仮定すると，定義9.2の最小性より
  $\sim_1\subseteq\sim_2\ \land\ \sim_2\subseteq\sim_1$
  $\Rightarrow\ \sim_1 = \sim_2$
  よって、定義9を満たす同値関係は一意である．

以上より、定義9を満たす同値関係はただ一つ存在し，$\sim=\sim'$
即ち，$(a,b)\sim(c,d) ⇔ a+d=b+c$

\begin{align} 0+a=0+a &⇔ [0,0]=[a,a] \\ &⇔ 0_\mathbb Z = [a,a] \end{align}
$\therefore 0_\mathbb Z := [a,a]$

$[a,b]=[c,d]$とする．
定理12より $a+d=b+c$
よって，
\begin{align} S(a)+d&= S(a+d) \\ &= S(b+c) \\ &= b+S(c) \end{align}
より，$[S(a),b]=[S(c),d]$から，
\begin{align} S_\mathbb{Z}([a,b])&=[S(a),b] \\ &= [S(c),d] \\ &= S_\mathbb{Z}([c,d]) \end{align}
$\therefore S_\mathbb{Z}$は$\text{well-defined}$

$P([a,b]) := [a,S(b)]$ とする．
($Pが\text{well-defined}$であることは$S_\mathbb{Z}$と同様に証明できる)
\begin{align} S_\mathbb{Z}(P([a,b])) &= S_\mathbb{Z}([a,S(b)]) \\ &= [S(a),S(b)] \\ &= [a,b] \end{align}
\begin{align} P(S_\mathbb{Z}([a,b])) &= P([S(a),b]) \\ &= [S(a),S(b)] \\ &= [a,b] \end{align}
よって$S_\mathbb{Z}$は全単射で ${S_\mathbb{Z}}^{-1}=P$
即ち， ${S_\mathbb{Z}}^{-1}([a,b]) = [a,S(b)]$

1. $f$の存在性を示す．
   自然数の再帰定理より，以下を満たす写像$h:\mathbb N\rightarrow X$が一意に存在する．
   $h(0)=x,\ h(S(b))=g^{-1}(h(b))$
   同様に自然数の再帰定理より，以下を満たす写像$k_b:\mathbb N\rightarrow X$が一意に存在する．
   $k_b(0)=h(b),\ k_b(S(a))=g(k_b(a))$
   
   写像$f':\mathbb Z\rightarrow X$を$f'([a,b]):=k_b(a)$とする．
   $f'が\text{well-defined}$であることを示す．

   $[a,b]=[c,d]⇒k_b(a)=k_d(c)$を示せばよい．
   ☆$k_{S(b)}(a)=g^{-1}(k_b(a))$を示す．
   (i) $a=0$のとき，
   \begin{align} k_{S(b)}(0)&=h(S(b)) \\ &= g^{-1}(h(b))\\ &= g^{-1}(k_b(0)) \end{align}
   より成り立つ．
   (ii) $a=l$のとき，$k_{S(b)}(l)=g^{-1}(k_b(l))$と仮定すると，
   \begin{align} k_{S(b)}(S(l)) &= g(k_{S(b)}(l)) \\ &= g(g^{-1}(k_b(l))) \\ &= k_b(l) \\ &= g^{-1}(g(k_b(l))) \\ &= g^{-1}(k_b(S(l))) \end{align}
   より$a=S(l)$のとき成り立つ．
   $\therefore k_{S(b)}(a)=g^{-1}(k_b(a))$
   
   ☆$k_{b+l}(a+l)=k_b(a)$を示す．
   (i) $l=0$のとき，
   $k_{b+0}(a+0)=k_b(a)$より成り立つ．
   (ii) $l=i$のとき，$k_{b+i}(a+i)=k_b(a)$と仮定すると，
   \begin{align} k_{b+S(i)}(a+S(i)) &= k_{S(b+i)}(S(a+i)) \\ &= g(k_{S(b+i)}(a+i)) \\ &= g(g^{-1}(k_{b+i}(a+i))) & (\because k_{S(b)}(a)=g^{-1}(k_b(a))) \\ &= k_{b+i}(a+i) \\ &= k_b(a) \end{align}
   より$a=S(i)$のとき成り立つ．
   $\therefore k_{b+l}(a+l)=k_b(a)$
   
   ☆$[a,b]=[c,d]⇒k_b(a)=k_d(c)$を示す．
   $[a,b]=[c,d]$とすると，
   $a+d=b+c$
   \begin{align} k_b(a) &= k_{b+d}(a+d) \\ &= k_{b+d}(b+c) \\ &= k_{d+b}(c+b) \\ &= k_{d}(c) \end{align}
   $\therefore [a,b]=[c,d]⇒k_b(a)=k_d(c)$
   
   
   \begin{align} f'(0_\mathbb Z) &= f'([0,0]) \\ &= k_0(0) \\ &= h(0) \\ &= x \end{align}
   \begin{align} f'(S_\mathbb Z([a,b])) &= f'([S(a),b]) \\ &= k_b(S(a)) \\ &= g(k_b(a)) \\ &= g(f'([a,b])) \end{align}
   から，$f'$は$f$の条件を満たす．
   よってこのような$f$が存在することが示された．
2. fの一意性を示す．
   定理12のようなfを一つとる．
   $\forall n\in\mathbb Z,\ f(S_\mathbb Z(n))=g(f(n))$であり，
   $S_\mathbb Z$は全単射なので，$m=S_\mathbb Z(n)$として，
   $\forall m\in\mathbb Z,\ f(m)=g(f({S_\mathbb Z}^{-1}(m)))$
   また$g$は全単射なので，
   $\forall m\in\mathbb Z,\ g^{-1}(f(m))=f({S_\mathbb Z}^{-1}(m))$
   
   写像$h:\mathbb N\rightarrow X$を$h(b):=f([0,b])$とする．
   \begin{align} h(0)&=f([0,0]) \\ &= f(0_\mathbb Z) \\ &= x \end{align}
   \begin{align} h(S_\mathbb N(b)) &= f([0,S(b)]) \\ &= f({S_\mathbb Z}^{-1}([0,b])) \\ &= g^{-1}(f([0,b])) \\ &= g^{-1}(h(b)) \end{align}
   より，自然数の再帰定理から，$h$は一意．
   
   写像$k_b:\mathbb N\rightarrow X$を$k_b(a):=f([a,b])$とする．
   \begin{align} k_b(0)&=f([0,b]) \\ &= h(b) \end{align}
   より，$k_b(0)$は一意．
   \begin{align} k_b(S(a)) &= f([S(a),b]) \\ &= f(S_\mathbb Z([a,b])) \\ &= g(f([a,b])) \\ &= g(k_b(a)) \end{align}
   より，自然数の再帰定理から，$k_b$は一意．
   よって、$f$は一意．

$\therefore f$は一意に存在する

二項演算$+':\mathbb{Z}\times\mathbb{Z}→\mathbb{Z}$を
$[a,b]+'[c,d]:=[a+c,b+d]$
とする．

• $+'$が$\text{well-defined}$であることを示す．
  $[a,b]=[a',b']，[c,d]=[c',d']$とすると，
  $a+b'=b+a'，c+d'=d+c'$
  よって，
  \begin{align} &(a+b')+(c+d')=(b+a')+(d+c') \\ ⇔\ &(a+c)+(b'+d')=(b+d)+(a'+c') \\ ⇔\ &[a+c,b+d]=[a'+c',b'+d'] \end{align}
  から，
  \begin{align} [a,b]+[c,d] &= [a+c,b+d] \\ &= [a'+c',b'+d'] \\ &= [a',b']+[c',d'] \end{align}
  より，$+'$は$\text{well-defined}$

• $n+'0_\mathbb Z = n$を示す．
  $n=[a,b]$とすると，
  \begin{align} n+'0_\mathbb Z &= [a,b]+'[0,0] \\ &= [a+0,b+0] \\ &= [a,b] \\ &= n \end{align}

• $n+'S_\mathbb{Z}(m) = S_\mathbb{Z}(n+'m)$を示す．
  $n=[a,b],\ m=[c,d]$とすると，
  \begin{align} n+'S_\mathbb{Z}(m) &= [a,b]+'S_\mathbb{Z}([c,d]) \\ &= [a,b]+'[S(c),d] \\ &= [a+S(c),b+d] \\ &= [S(a+c),b+d] \\ &= S_\mathbb{Z}([a+c,b+d]) \\ &= S_\mathbb{Z}([a,b]+'[c,d]) \\ &= S_\mathbb{Z}(n+'m) \end{align}

よって$+'$は定義12の条件を満たす．

• 定義12を満たす二項演算は一意であることを示す．
  定義12を満たす$+$を一つとる.
  写像$f_n:\mathbb Z\rightarrow\mathbb Z$を$f_n(m):=n+m$とし，
  写像$g:=S_\mathbb{Z}$とする．
  $g$が全単射なことに注意すると，このとき，
  \begin{align} f_n(0_\mathbb Z) &= n+0_\mathbb Z \\ &= n \end{align}
  \begin{align} f_n(S_\mathbb{Z}(m)) &= n+S_\mathbb{Z}(m) \\ &= S_\mathbb{Z}(n+m) \\ &= S_\mathbb{Z}(f_n(m)) \\ &= g(f_n(m)) \end{align}
  より，整数の再帰定理から，$f_n$は一意．
  よって，$+$は一意．

以上より、定義12を満たす二項演算はただ一つ存在し，$+=+'$
即ち，$[a,b]+[c,d]=[a+c,b+d]$

$n=[a,b]$とし，$m'=[b,a]$とする．
\begin{align} n+m'&=[a,b]+[b,a] \\ &=[a+b,b+a] \\ &=[a+b,a+b]\\ &=0_\mathbb Z \end{align}
よって$m'$は$n$の逆元．

ここで、逆元が一意であることを示す．
$m_1,m_2$が$n+m_1=0_\mathbb Z,n+m_2=0_\mathbb Z$を満たすとする．
このとき，
\begin{align} m_1 &= m_1+0_\mathbb Z \\ &= m_1+(n+m_2) \\ &= (m_1+n)+m_2 \\ &= (n+m_1)+m_2 \\ &= 0_\mathbb Z+m_2 \\ &= m_2 \end{align}

よって、逆元は一意

以上より、逆元はただ一つ存在し，$m=m'$
即ち，$m=[b,a]$

二項演算$-':\mathbb{Z}\times\mathbb{Z}→\mathbb{Z}$を
$n-'m:=n+(-m)$
とし，
$n:=[a,b],\ m:=[c,d]$とする．

\begin{align} [a,b]-'[c,d]&=[a,b]+(-[c,d])\\ &=[a,b]+[d,c]\\ &=[a+d,b+c] \end{align}
に注意して，

• $n-'0_\mathbb Z = n$を示す．
  \begin{align} n-'0_\mathbb Z &= [a,b]-'[0,0] \\ &= [a+0,b+0] \\ &= [a,b] \\ &= n \end{align}
• $S_\mathbb{Z}(n-'S_\mathbb{Z}(m)) = n-'m$を示す．
  \begin{align} S_\mathbb{Z}(n-'S_\mathbb{Z}(m)) &= S_\mathbb{Z}([a,b]-'S_\mathbb{Z}([c,d])) \\ &= S_\mathbb{Z}([a,b]-'[S(c),d]) \\ &= S_\mathbb{Z}([a+d,b+S(c)]) \\ &= [S(a+d),S(b+c)] \\ &= [a+d,b+c] \\ &= [a,b]-'[c,d]\\ &= n-'m \end{align}

よって$-'$は定義14の条件を満たす．

• 定義14を満たす二項演算は一意であることを示す．
  定義14を満たす$-$を一つとる.
  写像$f_n:\mathbb Z\rightarrow\mathbb Z$を$f_n(m):=n-m$とし，
  写像$g:={S_\mathbb{Z}}^{-1}$とする．
  $g$が全単射なことに注意すると，このとき，
  \begin{align} f_n(0_\mathbb Z) &= n-0_\mathbb Z \\ &= n \end{align}
  \begin{align} f_n(S_\mathbb{Z}(m)) &= n-S_\mathbb{Z}(m) \\ &= {S_\mathbb{Z}}^{-1}(S_\mathbb{Z}(n-S_\mathbb{Z}(m))) \\ &= {S_\mathbb{Z}}^{-1}(n-m) \\ &= {S_\mathbb{Z}}^{-1}(f_n(m)) \\ &= g(f_n(m)) \end{align}
  より，整数の再帰定理から，$f_n$は一意．
  よって，$-$は一意．

以上より、定義14を満たす二項演算はただ一つ存在し，$-=-'$
即ち，$n-m=n+(-m)$

二項演算$\cdot':\mathbb{Z}\times\mathbb{Z}→\mathbb{Z}$を
$[a,b]\cdot'[c,d]:=[ac+bd,ad+bc]$
とし，
$n:=[a,b],\ m:=[c,d]$とする．

• $\cdot'$が$\text{well-defined}$であることを示す．
  $[a,b]=[a',b']，[c,d]=[c',d']$とすると，
  $a+b'=b+a'，c+d'=d+c'$
  \begin{align} (a+b')(c+d')&=(a'+b)(c'+d) \\ (b+b')(c'+d)&=(b+b')(c+d') \\ (a'+b)(d+d')&=(a+b')(d+d') \end{align}
  これらの辺々を足すと，
  \begin{align} &(a+b')(c+d')+(b+b')(c'+d)+(a'+b)(d+d')\\ &=(a'+b)(c'+d)+(b+b')(c+d')+(a+b')(d+d') \end{align}
  展開すると，
  \begin{align} &ac + ad' + b'c + b'd' \\ &+ bc' + bd + b'c' + b'd \\ &+ a'd + a'd' + bd + bd' \\ =&\ a'c' + a'd + bc' + bd \\ &+ bc + bd' + b'c + b'd' \\ &+ ad + ad' + b'd + b'd' \\ \end{align}
  共通項を整理すると，
  \begin{align} &(ac+bd+a'd'+b'c') \\ &+(ad' + a'd + bc' + bd + bd' + b'c + b'd + b'd') \\ =\ &(ad+bc+a'c'+b'd') \\ &+(ad' + a'd + bc' + bd + bd' + b'c + b'd + b'd') \end{align}
  
  よって，
  \begin{align} &ac+bd+a'd'+b'c'=ad+bc+a'c'+b'd' \\ ⇔\ &(ac+bd)+(a'd'+b'c')=(ad+bc)+(a'c'+b'd') \\ ⇔\ &[ac+bd,ad+bc]=[a'c'+b'd',a'd'+b'c'] \end{align}
  から，
  \begin{align} [a,b]\cdot[c,d] &= [ac+bd,ad+bc] \\ &= [a'c'+b'd',a'd'+b'c'] \\ &= [a',b']\cdot[c',d'] \end{align}
  より，$\cdot'$は$\text{well-defined}$

• $n\cdot' 0_\mathbb Z = 0_\mathbb Z$を示す．
  \begin{align} n\cdot' 0_\mathbb Z &= [a,b]\cdot'[0,0] \\ &= [a\cdot 0+b\cdot 0,a\cdot 0+b\cdot 0] \\ &= [0,0] \\ &= 0_\mathbb Z \end{align}

• $n\cdot' S_\mathbb{Z}(m) = n\cdot' m + n$を示す．
  \begin{align} n\cdot' S_\mathbb{Z}(m) &= [a,b]\cdot'S_\mathbb{Z}([c,d]) \\ &= [a,b]\cdot'[S(c),d] \\ &= [a\cdot S(c)+bd,ad+b\cdot S(c)] \\ &= [ac+a+bd,ad+bc+b] \\ &= [(ac+bd)+a,(ad+bc)+b] \\ &= [ac+bd,ad+bc]+[a,b] \\ &= [a,b]\cdot'[c,d]+[a,b] \\ &= n\cdot' m+n \end{align}

• 定義15を満たす二項演算は一意であることを示す．
  定義15を満たす$\cdot $を一つとる.
  写像$f_n:\mathbb Z\rightarrow\mathbb Z$を$f_n(m):=n\cdot m$とし，
  写像$g_n(k):=k+n$とする．
  また，$h_n(k):=k+(-n)$とすると，
  \begin{align} g_n(h_n(k)) &= h_n(k)+n \\ &= (k+(-n))+n \\ &= k+((-n)+n) \\ &= k+0_\mathbb Z \\ &= k \end{align}
  \begin{align} h_n(g_n(k)) &= g_n(k)+(-n) \\ &= (k+n)+(-n) \\ &= k+(n+(-n)) \\ &= k+0_\mathbb Z \\ &= k \end{align}
  より，${g_n}^{-1}(k) = h_n(k)$から，$g_n$は全単射．
  このとき，
  \begin{align} f_n(0_\mathbb Z) &= n\cdot 0_\mathbb Z \\ &= 0_\mathbb Z \end{align}
  \begin{align} f_n(S_\mathbb{Z}(m)) &= n\cdot S_\mathbb{Z}(m) \\ &= n\cdot m+n \\ &= g_n(n\cdot m) \\ &= g_n(f_n(m)) \end{align}
  より，整数の再帰定理から，$f_n$は一意．
  よって，$\cdot$は一意．

以上より、定義15を満たす二項演算はただ一つ存在し，$\cdot=\cdot'$
即ち，$[a,b]\cdot[c,d]=[ac+bd,ad+bc]$