例とか例えではなく、以下の「ペアノの公理による1+1=2の証明」と同じくらい厳密な証明をお願いいたします。
http://d.hatena.ne.jp/tomo31415926563/20090110/1272413984
ペアノの公理
自然数は以下を満たす。
(1)自然数 0 が存在する。
(2)任意の自然数 a にはその後者 (successor)、suc(a) が存在する（suc(a) は a +
1 の "意味"）。
(3)0 はいかなる自然数の後者でもない（0 より前の自然数は存在しない）。
(4)異なる自然数は異なる後者を持つ。つまり a ≠ b のとき suc(a) ≠ suc(b) となる。
(5) 0 がある性質を満たし、a がある性質を満たせばその後者 suc(a) もその性質を満たすとき、すべての自然数はその性質を満たす。
ペアノの公理を満たす集合に対して加法が以下のように定義される。
すべての自然数 a に対して、a + 0 = a
すべての自然数 a, b に対して、a + suc(b) = suc(a + b)
ここで、
suc(0) := 1
suc(suc(0)):=2と定義すると。
加法の定義の二番目にa=suc(0) ,b=0を代入して
suc(0)+suc(0)=suc(suc(0)+0)
=suc(suc(0)) (加法の定義一番目の定義より)
ゆえに1+1=2
No.5
>この場合はλ式の使えるプログラム言語で「四則演算等、自分で定義していない演算子は一切使わず」「（－１）、（１）、（×：乗法）、（＝：等号）」をプログラミング（定義）して「 -1×-1=1」を出力できればいいのかな？
Scheme(Gauche)で作ってみた。
その前に、
>難しそうなのは匿名回答4号さんの定義だとある整数を表す表現は無限(x =(x+k,k):kは自然数)にあるので、等号をどうやって定義するかというのがありそうです。
(k,l) = (m,n) ⇒ k + n = l + m
とする。
(岩波数学辞典第四版p587参照)
さらに、掛け算の定義を以下の様に修正。
a * 0 = 0
a * succ(b) = a + (a * b)
;; 0を空リスト定義 (define zero '()) ;; 0の判定関数 (define (zero? x) (null? x)) ;; 後者写像succ (define (succ x) (cons x x)) ;; 後者写像の逆写像desucc ;; desucc(succ(x)) = x (define (desucc x) (car x)) ;; 足し算plus (define (plus a b) (let loop ((result a) (b b)) (cond ((zero? b) result) (else (loop (succ result) (desucc b)))))) ;; 掛け算mult (define (mult a b) (let loop ((result zero) (b b)) (cond ((zero? b) result) (else (loop (plus a result) (desucc b)))))) ;; 自然数→整数 (define (N-to-Z a) (cons a zero)) ;; 整数の同値 (define (Z= a b) (equal? (plus (car a) (cdr b)) (plus (cdr a) (car b)))) ;; 整数の掛け算 (define (Z-mult a b) (cons (plus (mult (car a) (car b)) (mult (cdr a) (cdr b))) (plus (mult (car a) (cdr b)) (mult (cdr a) (car b)))))
N-to-Zでは-1を作ることができない。
N-to-Zは自然数を整数に変換するものなので、そもそも自然数でない負数は対応していない。
だから、-1は手で作らないといけない。
具体的には、
(cons zero (succ zero))
とすれば良い。
Z-multは負数に対しても通用するので、
(Z= (N-to-Z (succ zero) (Z-mult (cons zero (succ zero)) (cons zero (succ zero))))
が#tを返せば良く、実際にそうなっている。
No.1
No.2
(-1)*(-1)=1を、整数Z上の単位元の逆元を2回かけると単位元になる、と言う意味で捉えると、環の定義から証明できる。
整数全体Zは環である。つまり、Zに対して、以下のことが成り立つ。
(1)加法が定義され、a in Z, b in Z => a + b in Z。このとき、
{1}交換法則が成り立つ a,b in Zに対して、a + b = b + a
{2}結合法則が成り立つ a,b,c in Zに対して、(a + b) + c = a + (b + c)
{3}零元0 in Zが存在し任意のaに対して、a + 0 = 0 + a = a
{4}任意のa in Zに対して、逆元-aが存在し、a + (-a) = (-a) + a = 0
(2)乗法が定義され、a in Z, b in Z => a*b in Z。このとき、
{1}結合法則が成り立つ a,b in Zに対して、(a*b)*c=a*(b*c)
(3)分配法則が成り立つ a,b,c in Zに対して、a*(b + c) = a*b + a*c , (a + b)*c = a*c + b*c
とくに、整数Zについては、次も成り立つ。(一般の環では成り立たない)
(4)整数Zには単位元1が存在して、任意のa in Z に対して、a*1 = 1*a = a
あと、
等式の性質 a,b,c in Z a=b,b=c => a=c
a,b,c in Z, a=b => a+c=b+c, c+a=b+a, a*c=b*c, c*a=c*b
以上を用いて、(-1)*(-1)=1を証明する。
[1]a*0=0
(1){3}より0+0=0なので、左からaをかけて、a*(0+0)=a*0
(3)より a*0 + a*0 = a*0
a*0 の逆元を右から加えて、(a*0 + a*0) + (-(a*0)) = a*0 + (-(a*0))
(1){2}よりa*0 + (a*0 + (-(a*0))) = a*0 + (-(a*0))
(1){4}よりa*0+0=0
(1){3}よりa*0=0
[2]-(-a)=a
(1){4}より、a+(-a)=(-a)+a=0より、-aの逆元はa、すなわち-(-a)=a
[3]a*(-1)=-a
1の逆元は-1なので、(1){4}より、1 + (-1)=0
任意のaを左からかけて、a*(1+(-1))=a*0
(3)と[1]より、a*1+a*(-1)=0
(4)より、a+a*(-1)=0
(1){3}より、aの逆元はa*(-1)、すなわち、a*(-1)=-a
[4](-1)*(-1)=1
[3]より、(-1)*(-1)=-(-1)
[2]より、-(-1)=1
したがって、(-1)*(-1)=1
(2){1}はたぶんいらない。Zは乗法について可換じゃなくても成り立つぽい。
No.3
整数を自然数のペアを使って以下の様に定義する。
z：(k+z,k)
0：(k,k)
-z：(k,k+z)
但し、kは任意の自然数。
加法は、
(k,l) + (m,n) = (k+m,l+n)
乗法は、
(k,l) * (m,n) = (k*m + l*n,k*n + l*m)
と定義する。
(岩波数学辞典第四版p587参照)
ここで、-1は(k,k+1)だから、
-1 * -1 = (k,k+1) * (k,k+1)
=(k^2 + (k+1)^2,2k*(k+1))
=(2k^2 + 2k + 1,2k^2 + 2k)
=1
No.4
既にいくつか回答が出ていますが、ちょっと補足的なことを。
「厳密な証明」をするためには、まず始めに「何を仮定するか」を"厳密に"決める必要があります。その仮定次第でこの質問には色々な回答が考えられます。
匿名回答3号さんの回答にあるように、「整数（とその上の加算・乗算）が（単位元を持つ）環の公理を満たす」ことを仮定すると、-1×-1=1が証明できます。これは整数に限らず、任意の（単位元を持つ）環について成り立つ性質です。匿名回答1号さんの回答にあるサイトでの説明も、環という言葉を使ってないだけで本質的に同じです。
「整数が環の公理を満たす」ことを仮定するなんてズルい、と思うかもしれません。しかし、質問者さんが例として挙げた「ペアノの公理による1+1=2の証明」においても、
「自然数がペアノの公理を満たす」こと及び「加法をどう定義するか」を仮定しているわけです。数学ではいつも何かを仮定しなければ始まりません。
別の回答としては、整数よりもっと基本的なものを仮定した上で、整数を「構成」して、その構成した整数の上に加算・乗算を「定義」し、-1×-1=1が成り立つことを証明する、というものが考えられます。匿名回答4号さんの回答がこれで、自然数は知っているものとして整数を構成し、その上の加算・乗算を定義して証明しています。
ただしこの回答でも、何故その構成が正しく整数を与えているのか、また何故その加算・乗算の定義が正しいと言えるのか、という点は自明ではありません。結局のところ、整数の性質を仮定するにしても、整数を構成するにしても、人間の直観（「整数」が何であるか知っている）が最終的には必要になるわけです。
ちなみに、「自然数はこういう性質を満たす」とか「環はこういう性質（公理）を満たす」といった仮定を置いてそこから出発するというのは現代的な数学における基本的な考え方ですが、これを突き詰めたのが公理的集合論で、集合が満たす性質を仮定するところから出発して、自然数も整数も実数も（実質的に「全ての数学」を）構成することができます。ひょっとしたら、「公理的集合論における整数の構成」こそが質問者さんの求める回答かもしれません。しかし、数学者であっても普通は、整数や実数が公理的集合論の中で構成されたものだと考えるよりは、単に、直観的に知っている（ある性質を満たす）数の集まりだと考えていると思います（そのような性質を満たす数の集まりが存在する（構成できる）という事実は重要ですが）。環の公理から-1×-1=1が導出できるように、満たす性質さえわかっていれば実際の構成はそれほど重要ではないからです。
整数に拡張した場合、このような証明になるのでしょう。
「整数の公理」
http://aozoragakuen.sakura.ne.jp/kaisekikiso/node10.html
こんな感じの回答を希望してます。（というかこれが回答そのものかな）
なるほど、自然数を仮定せずに整数を定義する流儀もあるわけですね。確かに、上で匿名回答4号さんが書いた式は負の数を含めても演算を一意に定めるので、それを整数上の乗算の定義とすることができます。一旦定義を与えてしまえば-1×-1=1であることを証明するのは難しくなりません（そのページではより一般に(-x)*(-y)=xyが示されていますね）。
ただし一つ注意する必要があるのは、「環の公理」は「整数の公理」よりも「弱い」ということです。つまり、「整数の公理」を満たす集合が環であることは証明できますが、「環の公理」を満たす集合は必ずしも整数ではありません。実際、整数は環の中でもすごく特別なものです。
つまり、見かけ上は環の公理は沢山あるようでも、実はより少ない仮定（公理）から証明をしているとも言えるということです。
そもそもなんで証明が必要？
https://twitter.com/HaraKazuo/status/513355620011888641
-1×-1=1(あるいは(-x)×(-y)=xy)を公理（定義：ルール)として認めてしまうという方法もあるのですよ。
中学校の「正の数・負の数」では証明することもなく「そういう規則（ルール）だから」で終わっています。
ーーーーーーーーーーーーーーーーーーーーーーーーーーーー
二つの数の積の符号と絶対値
二つの数が同符号なら、積の符号は正、積の絶対値は二つの数の絶対値の積
二つの数が異符号なら、積の符号は負、積の絶対値は二つの数の絶対値の積
ーーーーーーーーーーーーーーーーーーーーーーーーーーーー
しかし、いかなる整数においても成立するわけですから、そこには何か理由があると考えるのが自然だと思います。
-1×-1=1を証明しようと思えば、「（-1)とは何か」「×(乗法)とは何か」というのを定義するなり、他の定義（公理）から定理として証明する必要があるわけです。
ちゃんと証明しておかないと、誰かに聞かれた時に説明できませんから。
それが「そもそもなんで証明が必要？」に対する答えです。
ああ、後
「質問者が回答を理解できたかが気になる。」
http://b.hatena.ne.jp/entry/226736493/comment/homarara
これまで書いたコメント等で判断してみてくれ。
・・・
誰かλ式を使って証明してくれる人はいないかな。
λ式を使った自然数、加法、乗法の定義は良く見かけます。
匿名回答4号さんの定義を使えば、自然数から整数への拡張が出来るでしょう。
難しそうなのは匿名回答4号さんの定義だとある整数を表す表現は無限(x =(x+k,k):kは自然数)にあるので、等号をどうやって定義するかというのがありそうです。
この場合はλ式の使えるプログラム言語で「四則演算等、自分で定義していない演算子は一切使わず」「（－１）、（１）、（×：乗法）、（＝：等号）」をプログラミング（定義）して「 -1×-1=1」を出力できればいいのかな？
No.5
ここでベストアンサー
>この場合はλ式の使えるプログラム言語で「四則演算等、自分で定義していない演算子は一切使わず」「（－１）、（１）、（×：乗法）、（＝：等号）」をプログラミング（定義）して「 -1×-1=1」を出力できればいいのかな？
Scheme(Gauche)で作ってみた。
その前に、
>難しそうなのは匿名回答4号さんの定義だとある整数を表す表現は無限(x =(x+k,k):kは自然数)にあるので、等号をどうやって定義するかというのがありそうです。
(k,l) = (m,n) ⇒ k + n = l + m
とする。
(岩波数学辞典第四版p587参照)
さらに、掛け算の定義を以下の様に修正。
a * 0 = 0
a * succ(b) = a + (a * b)
;; 0を空リスト定義 (define zero '()) ;; 0の判定関数 (define (zero? x) (null? x)) ;; 後者写像succ (define (succ x) (cons x x)) ;; 後者写像の逆写像desucc ;; desucc(succ(x)) = x (define (desucc x) (car x)) ;; 足し算plus (define (plus a b) (let loop ((result a) (b b)) (cond ((zero? b) result) (else (loop (succ result) (desucc b)))))) ;; 掛け算mult (define (mult a b) (let loop ((result zero) (b b)) (cond ((zero? b) result) (else (loop (plus a result) (desucc b)))))) ;; 自然数→整数 (define (N-to-Z a) (cons a zero)) ;; 整数の同値 (define (Z= a b) (equal? (plus (car a) (cdr b)) (plus (cdr a) (car b)))) ;; 整数の掛け算 (define (Z-mult a b) (cons (plus (mult (car a) (car b)) (mult (cdr a) (cdr b))) (plus (mult (car a) (cdr b)) (mult (cdr a) (car b)))))
N-to-Zでは-1を作ることができない。
N-to-Zは自然数を整数に変換するものなので、そもそも自然数でない負数は対応していない。
だから、-1は手で作らないといけない。
具体的には、
(cons zero (succ zero))
とすれば良い。
Z-multは負数に対しても通用するので、
(Z= (N-to-Z (succ zero) (Z-mult (cons zero (succ zero)) (cons zero (succ zero))))
が#tを返せば良く、実際にそうなっている。
No.6
(-1)×(-1)＝a とすると、
{x -(x+1)}{x -(x+1)}=a
x^2-2x(x+1)+(-1)×(-1)×(x+1)^2=a
x^2 - 2x^2- 2x +a(x^2+2x+1)=a
x(x+2)(a-1)=0
これが任意のxで成り立つならばa=1
故に(-1)×(-1)＝1
失礼。これはネタ回答だと思ってました。
2
2
1
これだと整数の定義や、それが加算や乗算に対して群となることは前提としてるので、質問者さんの要望には足りてないんじゃないでしょうか。
2014/09/17 20:09:44そうですね。もう少し詳しい証明をお願いいたします。
2014/09/18 08:14:56