述語論理によるペアノ公理

質問

(a) 0 + x = x
(b) x + y = Z → (x + 1) + y = Z + 1
であるから
(1)Plus(0,x,x)
(2)Plus(x,y,z)→Plus(s(x),y,s(x))とする。
この定義で任意の加算が実行できる。

このとき2+3=5を証明せよ。
∃(xPlus(s(s(0)),x,s(s(s(s(s(0)))))
のx=s(s(s(0)))
となるのを証明せよという問題なのですが導出とか単一化と言われたのですが全く意味が分からないのでどんな風になるか教えていただければ幸いです。

似た意味の投稿がありましたが若干ずれたやり取りになっておりましたので投稿させて頂きますm()m

回答No.2

grothendieck

「まず(1)より
　Plus( 0, s(s(s(0))), s(s(s(0))) )
これに(2)を2回用いると
　Plus( s(s(0)), s(s(s(0))), s(s(s(s(s(0))))) )
これは2+3=5であることを示している。」
で良いのではないでしょうか。

回答No.1

grothendieck

まず、
(2)Plus(x,y,z)→Plus(s(x),y,s(x))とする。
は
(2)Plus(x,y,z)→Plus(s(x),y,s(z))とする。
に修正する必要があると思われます。そうすればできると思いますのでやってみて下さい。

お礼

grothendieckさん、早速有難う御座います。
見直してみたところご指摘の通り、間違っていました。
確認不足で投稿してしまい申し訳御座いませんm()m
-------------------------------------------------
(a) 0 + x = x
(b) x + y = Z → (x + 1) + y = Z + 1
であるから
(1)Plus(0,x,x)
(2)Plus(x,y,z)→Plus(s(x),y,s(z))とする。
この定義で任意の加算が実行できる。

このとき2+3=5を証明せよ。
∃(xPlus(s(s(0)),x,s(s(s(s(s(0)))))
のx=s(s(s(0)))
となるのを証明せよ
----------------------------------------------
↑で引き続きお願い致します。