# Kripke submodel

Let $\mathcal{F}=(W,R)$ be a Kripke frame. A subframe of $\mathcal{F}$ is a pair $\mathcal{F}^{\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 wR^{*}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 $\mathcal{F}_{w}$ the subframe of $\mathcal{F}$ 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\in W_{w}$, $M\models_{u}A$ iff $M_{w}\models_{u}A$.

###### Proof.

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

If $n=0$, then $A$ is either $\perp$ or a propositional variable. Clearly, $M\not\models_{u}\perp$ iff $M_{w}\not\models_{u}\perp$, or $M\models_{u}\perp$ iff $M_{w}\models_{u}\perp$. If $A$ is some propositional variable $p$, then $M\models_{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}\models_{u}p$.

Next, suppose $A$ is $B\to C$. Then $M\models_{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}\models_{u}A$.

Finally, suppose $A$ is $\square B$. First let $M\models_{u}A$. To show $M_{w}\models_{u}A$, pick any $v\in W_{w}$ such that $uR_{w}v$. Then $uRv$, so that $M\models_{v}B$, or $v\in V(B)$. Since $v\in W_{w}$, $v\in V_{w}(B)$, or $M_{w}\models_{v}B$, and thus $M_{w}\models_{u}A$. Conversely, let $M_{w}\models_{u}A$. To show $M\models_{u}A$, pick any $v\in W$ such that $uRv$. Since $wR^{*}u$, $wR^{*}v$ so that $v\in W_{w}$. Furthermore $(u,v)\in R\cap(W_{w}\times W_{w})=R_{w}$. So $M_{w}\models_{u}B$, or $v\in V_{w}(B)\subseteq V(B)$, which means $M\models_{u}A$. ∎

###### Corollary 1.

$M\models A$ iff $M_{w}\models A$ for all $w\in W$.

###### Proof.

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

###### Corollary 2.

$\mathcal{F}\models A$ iff $\mathcal{F}_{w}\models A$ for all $w\in W$.

###### Proof.

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

Title Kripke submodel KripkeSubmodel 2013-03-22 19:34:50 2013-03-22 19:34:50 CWoo (3771) CWoo (3771) 11 CWoo (3771) Definition msc 03B45 generated submodel