飯田隆編「知の教科書 論理の哲学」
選書メチエは選書にしてはハードなものが多いんだけど、本書も相当にハードだ。
論理トレーニング的なものではなく、どちらかというと数学よりな内容になっている。なので論理的思考をはぐくむために、ちょいと選書でも読んでみるかという気持ちで手を伸ばすのは危険だ。
また８つの章が別々の執筆者によるためか、内容とレベルにかなりの差があるので、章ごとに頭を切り替えて読む必要がある。
一章は簡単なまとめ。
二章はクレタ人のパラドックスを、三章はソリテス・パラドックス（砂山から一粒取り除いても砂山である、ゆえにいくら取り除いても砂山であり続ける）を扱っている。どちらも、わりと初歩的なパラドックスなので、あなどって読み始めたところ、特にソリテス・パラドックスについては幾重にも深い解説がなされていて驚かされた。
ひとことで論理学といっても、哲学的立場により、これだけの解釈があるというのは面白い。
で、このあたりまでは比較的簡単なんだけど、四章以降はとてもじゃないが入門書とはいえない内容になってゆく。
例えば四章では不完全性定理について説明してるんだけど、もともと知ってるひとじゃないと絶対に理解できない内容なのだ。想像するに、30ページくらいでそれなりに厳密に不完全性定理を説明してほしいんだけど、という要望に素直にこたえてしまったのだろう。
それでも五章は対話篇になっているので、読みやすい。ただ扱っている内容は、古典論理と背理法を許さない直観主義論理についてなので、やっぱり難しい。それでも、なんとなくわかった気にさせられたので、お得な感じである。
六章はフレーゲが提唱した論理主義がどのような展開をしていったのかという話。ラッセルのタイプ理論の説明もあったりする。これに関しては三浦俊彦「ラッセルのパラドクス」 - モナドの方へを読むと、わかりやすい。（読書案内になかったので紹介しておく）
個人的には七章がヒット。直観主義論理の自然演繹と型付きラムダ計算が同型である、というカリー＝ハワード同型対応を取り扱っている。ひらたく言ってしまうと、論理とプログラムが同型だから、プログラムを実行するのと論理的証明を行うことは同じことなんだよ、ということである。
ただしこの対応は背理法が使えない直観主義論理の枠組みの中の話である。では古典論理には対応しないのかというと、そうでもない。実は型付きラムダ計算に継続呼び出しを加えることが、直観主義論理に背理法を加えて古典論理になることと対応しているのである。具体的に言うと、型付きラムダ計算であるLISPに、継続呼び出しcall/ccを加えてSchemeになると、直観主義論理が古典論理になることと同じ意味であるということのようだ。
また、これは最後にちらっと書かれていることだが、人間の脳から生まれた論理体系とコンピュータ上で実行されるプログラムが対応しているということは非常に興味深い事実だ。もちろんコンピュータ（チューリングマシン）だって人間が生み出したんだから、当然だという指摘もあるかもしれないが……
いずれにせよこの対応関係には、まだまだ深遠な謎が横たわっているらしい。
八章は論理的に自然言語を扱いましょうというテーマで、一般述語論理やカテゴリー文法が紹介されている。またも最終的には言語構造がラムダ計算で扱えるという話になってゆくのが見所だ。
さて本書とは直接関係ないのだが、読んでいて考えてしまったのが論理学と時間との関係性である。まだ思いつき程度でまとまってないんだけど、忘れないうちに書いておく。
証明するプロセスや、ラムダ計算におけるβ簡約は、概念上は瞬時に適応されるということになっている。つまり計算が無時間で行われ、ウィトゲンシュタインの言ったように「すべての推論はア・プリオリに行われる」わけだ。
しかし現実には計算には時間がかかる。だから計算量の問題なんてのが重要な学問として成立しているわけである。
では、不死の存在を仮定したらどうだろう。時間を無限に消費してよいということは、計算が無時間で行われるのと等価である。無限ループにならない限り、必ず計算は終了する。これならば論理学の計算論議にはなんの問題もない。
逆に言うと、論理学はこのような不死の存在を措定しているということになる。残念ながら人間は、時間・空間ともに有限な存在だ。だから人間の時間感という枠組みで時間を考えてしまうと「時間は実在するか」にも書いてある通り、恐ろしく厄介な問題が噴出してくるのではないだろうか。
余談
フレーゲの著作の大部分が自国語の翻訳で読めるのは、世界の中でも日本だけ！だそうだ。
