証明するということ

しばらく前に買って積読されていたので再度読み始めました

ゲーデルの定理を大学時代に知ったときは「結論はわかる。でもどうして証明可能であるという概念が実際に算術上の命題として表現できるのか？」を理解することができなませんでした。論文ではこの部分を丁寧に大量の中間概念を導入しながら証明していくのですが、個々が抽象的すぎてすぐに眠くなってしまうからです。

100年前にヒルベルトが目指した数学の完全な形式化、そしてその無矛盾性の証明は当時は高度に抽象的なものであったと思います。

しかし現在プログラミングを生業にしているとこの概念は極めて具体的で明瞭です。

なんせコンピュータとは形式的な記号の羅列をルールに従って操作しているだけなのですから。

ゲーデル数の概念はアセンブリ（プログラミング言語）そのものがビットの羅列で表現できることと同値だし、定理や推論規則の算術的操作への置き換えはCPUがそのビット列に対してビット操作（演算だ）するだけで動いていることと同値です。

そう、今回は違います。ゲーデルの証明を一つずつプログラム言語で記述してしまえばいい！

そういうことならHaskellでしょう。だってHaskellのプログラムってそのまま数学の証明みたいだもんね！

まあそんな野望を抱いて最初の1章を読み終え、さてそろそろプログラムを書くか…とHaskellに詳しい同僚に相談してみました

「無理っすよ、Haskellは述語論理（∀とか∃とか）を表現できないですから！Haskellに述語論理をのっけたAgdaってのがあります」

うーんなるほどね。世の中には大抵先を行く人がいるもんだな。

すげぇと感心しつつ、Haskellさえちゃんとやったことのない身としては恐怖を覚えたのでした。

まあ今回は本当に証明したいわけではなく、ゲーデルの証明をプログラミング言語で表現したいだけなのでExistとかForAllとかの関数を書けば済みそうではあります。とさっそく言い訳を…