大西琢朗先生の以下のブログ記事が面白かった。
タフコ先生の論理的実在論に関する論文を批判している。形而上学の議論を論理学に当て嵌めただけで、論理学そのもののおもしろさを見逃しているのではないか、というような内容。
特に以下がなるほどである。
たとえば、論理学の基本的な定理である完全性定理は「任意の推論に対して、その妥当性を示す証明か、その非妥当性を示す反例モデルのいずれかが存在する」という定理です。「証明」はもちろん言語的な構成物です。他方、ここでの「反例モデル」はしばしば、論理式の集合からなる「カノニカルモデル」として与えられます。つまり、こちらも言語的な構成物です。完全性定理は、言語的な構成物を大々的に用いて証明される定理です。
完全性定理は「 ならば
」というような風に書かれるが、引用のように表現することも出来るなあ。完全性定理を証明する際によくあるパターンは以下である。まず、対偶の
から
を導くことを考える。
は
を含意するので、無矛盾な理論がモデルを持つことが示されれば、
を真にするモデル、すなわち
を全て真にして
を偽にするモデルが得られる。無矛盾な理論に対してモデルを作る操作は論理式の集合を使って行うと上手くいきがちなのである。これは古典論理の命題論理や述語論理でもそうだし、様相論理なんかでクリプキ・モデルを作る際もそうなんである。
ここから大西先生は以下のように書いている。
比喩的に言うと、ここには、言語それ自体が、自身の論理的正しさを支えうるような「客観的事実」を構成しているという驚きがあります (わりとみんなに共有されている驚きだと思うんですが、どうでしょう)。論理にかかわる実在論を論じるなら、こういう驚きが出発点になると思うんですが、残念ながら、(IND)にはそういう驚きのカケラも見いだせないんですよね。
（(IND)というのはタフコ先生の論文に出てくる命題）完全性定理の証明を勉強すると確かにここに感心するのだが、ちゃんと考えたことはなかった。我流で勉強してきたからかも。いまゼミでCTL（計算木論理）というやつの完全性定理がらみのことをやっているので先生や他の人の意見を頂戴したいところ。「わりとみんなに共有されている」のかどうか。
大西先生は証明論的意味論(以下PTS)の研究で博士論文を書いておられる。PTSの精神はこういうところにあるのかもしれない。先日PTSを研究している先輩の発表を聴いた感じでは、証明という言語的な営み・構成物から真理のような客観的っぽいものを定義しようとする研究という印象を受けた。
