Greg Restall, "Truth values and proof theory"

sequent calculus から truth value を構築する話。技術的には既知なのだけど、この論文の焦点はそれをどう解釈するかにある。らしい。

やってることは普通の sequent calculus から canonical model を作る標準的なやり方。Γ=>Δ が証明できない対 (Γ,Δ) で極大なものを考えるということです。

技術的な部分で知らなかった点が二つ。直観主義の場合に single conclusion にするか multiple conclusion (で →-R を使うときだけ single conclusion) にするかで、出てくるモデルが違う (single conclusion なら Beth semantics で multiple conclusion なら Kripke semantics) というのが一つ目。それから二つ目は、(古典)様相論理 S5 が hypersequent で定式化できて、それに対しても同様の構成ができるということ。この場合は、各々の極大無矛盾集合(的なもの)が Kripke frame になります。可能世界は hypersequent に属している個々の sequent 。

これだけだと論文の中身を紹介したことにはほとんどならないのですが、それ以外でどこに感動すればいいのかがいまいちわからなかったのです。まず inference ありきで、そこから truth value がどうやって説明できるかという話だと思うのですが、極大無矛盾集合をとるみたいな超越的なことをしてるあたりでなんかもやもやしています。