from constant domain model to hyperdoctrinal model

後でやろうと思っていた hyperdoctrinal model による Kripke model の再構成をやってみました。少しは理解が進んだと思いたい。

元になる意味論

constant domain model $(W, R, D, I)$ が与えられたとき、 $g, w {\mid\hspace{-5}=} \phi$ が定義される。ここで

W は集合、R はその上の関係
D は集合
I は各述語変数 P に $I(P) : W {\;\rightarrow\;} 2^{D^n}$ を割り当てる (n は P の arity)
$w \in W, g : Var {\;\rightarrow\;} D$ . (Var は個体変数の集合)

w を隠す

このように定義された関係から、次のような集合を定義する:

$\llbracket \phi \rrbracket^g := \{ w \;\mid\; g, w {\mid\hspace{-5}=} \phi \} \subseteq 2^W$ .

そうすると

$g, w {\mid\hspace{-5}=} \phi {\;\Longleftrightarrow\;} w \in \llbracket \phi \rrbracket^g$

であると考えることができる。このとき、 $A = 2^W$ とおいて $I(P) : D^n {\;\rightarrow\;} A$ とみなすと、意味論の定義から W, R を消すことができる。

そのようにして意味論を再定義すると、与えられた $(D, I, A)$ から $\llbracket \phi \rrbracket^g \in A$ が定義されることになる。ここで A は任意の BAO となり、先の定義はその特別な場合 (complex algebra) とみなせる。

g を隠す

さらに抽象化を推し進めてみる。さきほどの $\llbracket \phi \rrbracket^g$ を g の関数だと考える。そうすると

$\llbracket \phi \rrbracket : D^{Var} {\;\rightarrow\;} A$

である。

いま $\mathcal{A}(X) := A^X$ と定義すると $\mathcal{A} : Set {\;\rightarrow\;} BAO^{op}$ は hyperdoctrine であり、論理式の interpretant は $\mathcal{A} (D^{Var})$ である。実際には assignment のうち使われるのは有限個 (解釈しようとする論理式の自由変数の個数) だけなので、そのあたりを調整すると hyperdoctrinal model として定式化できる。