日々の流転

λ. 直観主義命題論理の意味論

直観主義命題論理のモデルって以下の三種類くらいあるのだけど、その関係を私はちゃんと考えたことがなかったので、ちょっとだけ考えてみた。

1. クリプキ・モデル
2. 位相空間の開集合系によるモデル
3. ハイティング代数によるモデル

クリプキ・モデルである論理式が真になる世界の集合は上に閉じた集合なのでAlexandrov位相の開集合になり、したがって位相空間によるモデルを得られる。〚A→B〛 は ∪{X∈O | X∩〚A〛⊆〚B〛} = int(〚A〛^c ∪ 〚B〛) となる。

一般に、位相空間の開集合系はフレームという代数をなすが、フレームは a→b = ∨{x | x∧a≦b} と定義することでハイティング代数になるので、位相空間によるモデルからハイティング代数によるモデルが得られる。 ので、位相空間によるモデルはハイティング代数によるモデルの特殊例。

次に、ハイティング代数 K によるモデルが与えられたとき、そのスペクトラムであるコヒーレント空間 Spec K を考えれば位相空間によるモデルが得られる*1。

最後に、位相空間によるモデルが与えられたとき、specialization (pre)order によって順序を入れれば、クリプキ・モデルを得られる。ただ、元の位相空間がT₀でない場合には、得られたクリプキ・モデルの到達可能性関係は半順序ではなくて前順序になってしまうので、半順序になるように商集合をとる必要がある(T₀化)。 半順序になるよう商集合をとる必要があるのは、多くの文献ではクリプキ・モデルの到達可能性関係に半順序という条件を付けているからなのだけど、実際にはこれは前順序に弱めてしまっても特に不都合はないはずで、なんで多くの文献では半順序として定義してるんだろうなぁ。