birelational semantics for IK without distributivity
distributivity のない可能様相をもつ直観主義様相論理の完全性はどうやって証明するものだったかなと思って "Categorical and Kripke semantics for constructive S4 modal logic" (Alechina et al. '01) を読み返しました。
気づいたこと: completeness for IK
読んでいるうちに、別に CS4 でなくても IK でほとんど同じことができると気がつきました。やり方は
- W = {(Γ, Θ) | Γ: a (not necessarily proper) prime filter, Θ: an ideal or empty set, Γ∩Θ={} }
- (Γ, Θ) ≦ (Γ', Θ') iff Γ⊂Γ'
- (Γ, Θ) R (Γ', Θ') iff (if □A ∈ Γ then A ∈Γ') and (if ◇A ∈ Θ then A ∈Θ')
でよさそう。*1
対応する公理系は
- intuitionistic tautologies
- K□: □(A ⊃ B) ⊃ □A ⊃ □B
- K◇: □(A ⊃ B) ⊃ ◇A ⊃ ◇B
- modus ponens: if A and A ⊃ B then B
- necessitation: if A then □A
疑問
この frame の作り方、前に読んだときはそんなに気にならなかったのですが、何か不思議なことをしているように感じられます。Θの部分はどうして intuitionistic accessibility に関係しないのでしょう。確かに証明を読めば、そうする必要があったことは理解できます。しかし Θ の存在が結局何を意味しているのかよくわからないのです。
Θ は、直感的には "negative information" を表す、と書いてありました。R の定義からも読み取れますが、Θ はある種の制約になっています。Γ が「成立していることがら」の集まりであるのに対し Θ は「成立していないことがら」の集まりといえそうです。*2
そうであるならば、その説明を素直に読むと Θ が増えることも知識の増加であるようにも思えたり、A ∈Θ と ¬A∈Γ は同じなんじゃないかという気がして Θ が何のために存在するのかよくわからなくなったりします。
結局のところ、このモデルの構成がうまくいくということをどのように理解したらいいのでしょうか。
lax modality and constraint
そうこうしているうちに思いついたのが lax logic で、Θ を制約だと考えると「ある制約のもとで成り立つ」という意味の lax modality と関係があるのではないかと考えられます。そこで "Propositional lax logic" (Fairtlough, Mendler '97) を見てみたところ、表現は違いますが実はほとんど同じことをしているように見えました。Γ が増えるときに (Θ とは関係なく) intuitionistically accessible で、特に Θ も増える場合には modally accessible とすると lax logic の completeness の証明へつながるようです。
ということは、Θ の関わる部分をうまく切り出し lax modality によって制約の存在を論理のレベルで明示してやれば、もう少し理解が進むのかもしれません。
しかしとりあえず今のところは「Θ が何を意味していてその大小が intuitionistic な部分に関係しないのがどうしてなのか」という最初の疑問については解決していません。状態に制約を課したり、課された制約を解除したりできるってどういうことだろう。
