>任意の文字列に対して、それが何らかの定理の証明になっているかを
>判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
>あるかどうかの判定をするアルゴリズムも書ける。

ええ、うそでしょ？
ならそのアルゴリズムがすでに定理の証明になっちゃってるじゃん。