Kripke frame
Kripke 意味論 (Kripke semantics)。可能世界意味論
クリプキ・モデル - Wikipedia
Kripke semantics - Wikipedia
Kripke frame in nLab
Kripke frame とは$ Wを集合として、二項關係$ R\subseteq W\times Wとの組$ (W,R)を言ふ
Kripke model
Kripke model とは Kripke frame に、集合$ Wの要素と命題との以下の條件を滿たす二項關係$ \Vdashを足した組$ (W,R,\Vdash)である
$ w\Vdash\neg A\iff w\cancel\Vdash A.
$ w\Vdash A\to B\iff w\cancel\Vdash A\lor w\Vdash B.
$ w\Vdash\square A\iff\forall u_{\in W}(wRu\land u\Vdash A).
命題文$ Aが Kripke model$ M=(W,R,\Vdash)に於いて妥當であるとは$ \forall w_{\in W}(w\Vdash A)である事を言ひ、$ M\vDash Aと書く
命題文$ Aが Kripke frame$ F上の任意の Kripke model で妥當であれば、$ Aは$ F上で妥當であると言ひ、$ F\vDash Aと書く
命題文$ Aが Kripke frame の類 (class)$ {\bf C}_Fに屬する任意の Kripke model 上で妥當であれば、$ Aが$ \bf C_Fで妥當であると言ひ、$ {\bf C_F}\vDash Aと書く
集合$ Wの要素は「世界」より「場所」と呼ぶのが穩當ではないか
bounded morphism (p-morphism (pseudo-epimorphism))
Kripke frame$ (W,R)と$ (W',R')が有り、寫像$ f:W\to W'は以下を滿たす時、$ (W,R)から$ (W',R')への bounded morphism と呼ぶ
$ \forall u,w_{\in W}(uRw\to f(u)R'f(w))關係を保存する
$ \forall u_{\in W},w'_{\in W'}(f(u)R'w'\to\exist w_{\in W}(uRw\land f(w)=w'))關係を考慮した全射
Kripke model 閒の bounded morphism は更に、全ての命題變數$ pに就いて$ w\Vdash p\iff f(w)\Vdash'pを滿たす
bounded morphism は Kripke frame 閒の雙模倣の一種である
? 有界型空閒との關係は?
有界型空閒
雙模倣 (bisimulation)
Kripke frame$ (W,R)と$ (W',R')が在る時、二項關係$ B\subseteq W\times W'が雙模倣であるとは以下の zig-zag property が滿たされる事を言ふ
$ uBu'\land uRw\to\exist w'_{\in W'}(wBw'\land u'R'w').
$ uBu'\land u'R'w'\to\exist w_{\in W}(wBw'\land uRw).
Kripke model 閒の雙模倣は更に、全ての命題變數$ pに就いて$ wBw'\to (w\Vdash p\iff w'\Vdash'p)を滿たす
反射律$ wRwと推移律$ uRv\land vRw\to uRwを滿たす Kripke frame は圈である
反射律は公理 T$ \square A\to A
推移律は公理 4$ \square A\to\square\square A
S4 樣相論理 (半順序 (poset))
IL frame とも呼び$ (W,\le)と書く
Kripke frame は集合$ Wからその冪集合$ 2^Wへの自己函手$ {\cal P}:W\to 2^Wの$ \cal P-餘代數 (圈)である
y.「Coalgebra としての Kripke フレーム」2018
Kripke frame は bounded morphism を射として圈を成し、この圈は$ \cal P-餘代數の圈$ {\bf Coalg}({\cal P})と圈同型である
擴張
general frame$ (W,R_{\subseteq W\times W},A_{\subseteq 2^W})
Kripke 層
Routley-Meyer frame$ (W,R_{\subseteq W\times W\times W},^*_{:W\to W},0_{\in W})
近傍 frame$ (W,N_{:W\to2^{2^W}})