論理学

もう，正月からずいぶん過ぎてしまったわけだが．．．

実は『群論』から『ロジック』方向へ少々興味が移ってしまい，かなり長い間，記事を書いていないような気がする．
有限群ファンの日記というタイトルでロジックの話題を書くことには，あまり抵抗ないのだが，ネタがさっぱりない．
まあ，今は教科書を読んでるような段階ではあるが，有限群論のようにちょこっとしたネタのようなものがロジックではちょっと思いつかない（←不勉強）．また，証明も非構成的なものが多くて（イライラするし），計算機の有限な世界とはかけ離れて．．．と言いたいところであるが，実はそうではないらしい．

知の教科書　論理の哲学 (講談社選書メチエ)

の206ページあたりに　『ゆえに古典論理と直観主義論理の違いは、プログラミングの言葉でいえば、大域脱出ができるかできないかの違いだということになる。』という衝撃的な文章がある．きっとこの文にシビレタのは私だけではあるまい．この結果は1990年と紹介されているのでもう20年も前になるわけだが，まったく知らなかった（←不勉強なだけ）．
この結果の何が面白いかというと，プログラムの構文の一つであるGoto文の使用に疑問を呈する内容で，Dijkstra（ダイクストラ）というコンピュータ学者が1968年に発表した論文に端を発したGoto文論争というものが’70年代にかけて起こっていたのである，当時は論理学とはまったく違う次元の論争で，簡単に言うと『（Goto文不使用による）形式の美しさか？（Goto文使用による）効率重視か？』が論点となっていた．その論争が実は『直観論理か？古典論理か？』という議論であったというのが愉快なところである．
しかし，論理学としても不毛な議論であったのではないような気がする．（なんらかの意味での）効率性ということと排中律は関連性があるように思うのである．それは，『細かい確認手続きはわからなくてもいいから，AかAでないかどっちか成り立っているのだから先へ進めるでしょう？』というような効率性である．