# 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 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 ${\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\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 $\u27c2$ or a propositional variable. Clearly, $M{\vDash \u0338}_{u}\u27c2$ iff ${M}_{w}{\vDash \u0338}_{u}\u27c2$, or $M{\vDash}_{u}\u27c2$ iff ${M}_{w}{\vDash}_{u}\u27c2$. 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.

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

###### Proof.

If $\mathcal{F}\vDash A$, then $M\vDash A$ for all $M$ based on $\mathcal{F}$, or ${M}_{w}\vDash 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}\vDash A$. Conversely, suppose ${\mathcal{F}}_{w}\vDash 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}\vDash A$. Since $w$ is arbitrary, $M\vDash A$ by the last corollary, so $\mathcal{F}\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 |

\@unrecurse |