13/12/05 20:45:18.86
自然数論の形式的な論理式がどういうものかご存知ですか？
これは案外不自由なもので、まずこれを知らないと、
そもそも「標準的自然数」とは何なのかも理解できません。
ここでやらないといけないのは与えられた数から1ずつ引いていくプログラムじゃなくて
「"いずれ"0に到達できる」ということを表現した形式的な論理式です。
342は、「"いずれ"0に到達できる」、ということを表現できていないように思います。
「有限回の操作後いずれ0になる」の意味なんて明らかだ、というのは
「標準的自然数」の定義なんて明らかだ、誰でも知ってるから敢えて書く必要ない、
というのと似たようなことです。
＞再帰的定義のところが間違いなのでしょうか
仰るとおりです。「案外難しい」というか、実際やってみるとできません。
不完全性定理周りでは「明らかに」できそうなことが実はできないことがわかる、
というようなことは良くあります。だから不完全性定理の証明では、
自明臭いことを延々と実際に書いて確かめたりします。