余談

ちなみにゲーデルさんが定義した最初の関数は

y|x ⇔ yをxで割った余りは0である

だぜ。2番目は「xは素数である」という関数だぜ。
どっちも中学レベルだぜ。
ここから46番目の

Provable(x) ⇔ ゲーデル数xを持つ式は証明可能である

まで「具体的に構築」
してしまうのがゲーデルさんの本当に恐ろしいところだぜ