>>216
決定可能だったら有限個の公理のセットを知っていればそれで良いけど
決定不能だったらそうはいかないでしょ。

「Th(<N, S(・), ＋, ×>)については読者はよく知っていると仮定する」
とか言われても、実際この中にRiemann予想（の自然数論上の同値命題）
とか双子予想とかが入ってるかどうかなんて分からないんだから
ちょっと真面目に考えると途方に暮れるしかない訳で。

まあ原理的には決定可能な命題の中にも、
IMOの実不等式の証明問題になるようなnon-trivialな命題は存在するけどね。

あとこういう話題にはTuring還元の話とかとも関係すると思う。