>>502
をを！すまんかった。今は反省している。どうも>>498を読んだときバカにされた気が
して感情的になってしまったようだ。

おわびに、ゲーデル数化をしても、定理の自動証明にはあまり実用的でないということ
を例えで説明しよう。まず、使用する文字を決める。例えば、ひらがな全てでも良い。
カタカナを含めてもよい。いずれにしても使う文字は有限個に決める。例えばN個だと
しよう。文字を2つだけ並べた文字列は有限個しかない。今の例ならN×N個だ。文字を
3つだけ並べた文字列も有限個。4つ並べても有限個。．．．と行くと、いずれは例えば

ふるいけやかわずとびこむみずのおと

というような文字列も現れるし、ピタゴラスの定理の証明として読める文章も現れる。
それに、以上の手続きは簡単なアルゴリズムで書ける。もっと詳しく論理式とか、証明
を定義すれば、任意の文字列に対して、それが何らかの定理の証明になっているかを
判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
あるかどうかの判定をするアルゴリズムも書ける。