ごとけんです

In message "[ruby-math:00021] Re: Why is '**' not abelian"
    on 00/01/12, Toyofuku <toyofuku / juice.or.jp> writes:

>> 上の等号をもし証明ぽく示すなら、
>>   succ**n(m) => succ**n(succ**m(0))
>  ...
>>              => succ(succ(...(succ(succ(succ(...succ(0)...))))...))
>>                 |<-- succがn個 -->|<-- succがm個 -->|
>
>    succ**m(n) => succ(succ(...(succ(succ(succ(...succ(0)...))))...))
>                  |<-- succがm個 -->|<-- succがn個 -->|
>
>  これだと「n個の後にm個」と「m個の後にn個」が
>等しいかということになって n+m == m+n かという
>問題に戻ってしまいませんか。
>証明っぽくするには数学的帰納法かな。
     ======

いや、それだと証明になってしまいます :-)

ちなみに、ペアノの公理系は、可換かつ結合律をみたす加法を使っ
ても同値な公理系を作れるようです。詳しくは数学辞典の「数」の
項に載っています。

-- gotoken