x+0=xは定義されていますが、逆バージョン0+x=xは証明定義されていませんのて証明していきます。
0+x=x
証明
1.0+0(仮定)
1.0(加法定義)
3.0+0⇔0…1
4.0+1(仮定)
5.S(0+0)(加法定義)
6.S(0)(1より)
7.1
8.0+1⇔1…2
9.0+2(仮定)
10.0+S(S(0))
11.S(0+S(0))(加法定義)
12.S(0+1)
13.S(1)(2より)
14.0+2⇔2
(1)(2)(3)より前の式の証明が後の式の正しさを証明する数学的帰納法が成立します。
コメント