>>750
ゲーデルの結果だね。これがあるから、今日では successor を使わず、
加法乗法を定義ではなく関数記号として与える現在の流儀になった。
>>751
スマリヤンは読んでないから知らない。評判が悪い本なのは確かだが。
successor 使わないのが一般的だが、使う流儀もないわけじゃないし、
そういうのがあっても、まあいいんじゃないの？