Kripke submodel

Let $ℱ=(W,R)$ be a Kripke frame. A subframe of $ℱ$ is a pair ${ℱ}^{\prime }=(W^{\prime },R^{\prime })$ such that $W^{\prime }$ is a subset of $W$ and $R^{\prime }=R\cap (W^{\prime }\times W^{\prime })$. A submodel of a Kripke model $M=(W,R,V)$ of a modal propositional logic PL${}_M$ is a triple $(W^{\prime },R^{\prime },V^{\prime })$ where $(W^{\prime },R^{\prime })$ is a subframe of $(W,R)$, and $V^{\prime }(p)=V(p)\cap W^{\prime }$ for each propositional variable $p$ in PL${}_M$.

The most common submodel of a Kripke model $M=(W,R,V)$ is constructed by taking $W_w:=\{u\mid w{R}^{*}u\}$, where $R^{*}$ is the reflexive transitive closure of $R$, for any $w\in W$. The submodel $M_w:=(W_w,R_w,V_w)$ is called the submodel of $M$ generated by the world $w$, and ${ℱ}_w$ the subframe of $ℱ$ generated by $w$. A submodel of $M$ is called a generated submodel if it is generated by some world $w$ in $M$.

Proposition 1.

For any wff $A$ and any $u\mathrm{\in }{W}_w$, $M{\mathrm{\vDash }}_{u}A$ iff $M_w{\mathrm{\vDash }}_{u}A$.

Proof.

We do induction on the number $n$ of connectives in $A$.

If $n=0$, then $A$ is either $⟂$ or a propositional variable. Clearly, $M{\vDash ̸}_u⟂$ iff $M_w{\vDash ̸}_u⟂$, or $M{\vDash }_u⟂$ iff $M_w{\vDash }_u⟂$. If $A$ is some propositional variable $p$, then $M{\vDash }_{u}p$ iff $u\in V(p)$ iff $u\in V(p)$ iff $u\in V(p)$ and $u\in W_w$ (by assumption) iff $u\in V(p)\cap M_w$ iff $u\in V_w(p)$ iff $M_w{\vDash }_{u}p$.

Next, suppose $A$ is $B\to C$. Then $M{\vDash }_{u}A$ iff $u\in V{(B)}^c\cup V(C)$ iff $u\in (W-V(B))\cup V(C)$ and $u\in W_w$ (by assumption) iff $u\in W_w-V(B)$ or $u\in V_w(C)$ iff $u\in W_w-V_w(B)$ or $u\in V_w(C)$ iff $M_w{\vDash }_{u}A$.

Finally, suppose $A$ is $\mathrm{\square }B$. First let $M{\vDash }_{u}A$. To show $M_w{\vDash }_{u}A$, pick any $v\in W_w$ such that $u{R}_{w}v$. Then $uRv$, so that $M{\vDash }_{v}B$, or $v\in V(B)$. Since $v\in W_w$, $v\in V_w(B)$, or $M_w{\vDash }_{v}B$, and thus $M_w{\vDash }_{u}A$. Conversely, let $M_w{\vDash }_{u}A$. To show $M{\vDash }_{u}A$, pick any $v\in W$ such that $uRv$. Since $w{R}^{*}u$, $w{R}^{*}v$ so that $v\in W_w$. Furthermore $(u,v)\in R\cap (W_w\times W_w)=R_w$. So $M_w{\vDash }_{u}B$, or $v\in V_w(B)\subseteq V(B)$, which means $M{\vDash }_{u}A$. ∎

Corollary 1.

$M\vDash A$ iff $M_w\mathrm{\vDash }A$ for all $w\mathrm{\in }W$.

Proof.

If $M\vDash A$, then $M{\vDash }_{u}A$ for all $u\in W$, so that $M_w{\vDash }_{u}A$ for all $u\in W_w$ and all $w\in W$, or $M_w\vDash A$ for all $w\in W$. Conversely, if $M_w\vDash A$ for all $w\in W$, then in particular $M_w{\vDash }_{w}A$ (since $R^{*}$ is reflexive) for all $w\in W$, or $M{\vDash }_{w}A$ for all $w\in W$, or $M\vDash A$. ∎

Corollary 2.

$ℱ\vDash A$ iff ${\mathrm{F}}_w\mathrm{\vDash }A$ for all $w\mathrm{\in }W$.

Proof.

If $ℱ\vDash A$, then $M\vDash A$ for all $M$ based on $ℱ$, or $M_w\vDash A$, where $M_w$ is based on ${ℱ}_w$, for all $w\in W$ by the last corollary. Since any model based on ${ℱ}_w$ is of the form $M_w$, ${ℱ}_w\vDash A$. Conversely, suppose ${ℱ}_w\vDash A$ for all $w\in W$. Let $M$ be any model based on $ℱ$. Then $M_w$ is based on ${ℱ}_w$, and therefore $M_w\vDash A$. Since $w$ is arbitrary, $M\vDash A$ by the last corollary, so $ℱ\vDash A$. ∎

Title	Kripke submodel
Canonical name	KripkeSubmodel
Date of creation	2013-03-22 19:34:50
Last modified on	2013-03-22 19:34:50
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	11
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B45
Defines	generated submodel