北田 発見への道 9章

9章 証明の数値的表現

これまでの議論において、「xは公理である⇔Axiom(x)」や「xは証明列である⇔Proof(x)」といった、ゲーデル数を引数にとる述語を、自然数論の体系 N において再帰的に構成できると述べてきた。それを示している。

なお、「xは証明可能である⇔Pr(x)」、「xは反証可能である⇔Re(x)」もNにおいて表現できるが、それは再帰的ではない。

コンピュータ言語みたいっすなー。一つ一つはきちんと見ていないが実際にできるだろうということは納得がいく。