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\ot\\models_{u}\\perp$ iff $M_{w}\ot\\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 $u R v$ , 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 $u R v$ . 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$ .∎

单词	KripkeSubmodel
释义	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\ot\\models_{u}\\perp$ iff $M_{w}\ot\\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 $u R v$ , 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 $u R v$ . 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$ .∎
随便看	StableFixedPoint stable fixed point StableIsomorphism stable isomorphism StableManifold stable manifold StableManifoldTheorem stable manifold theorem StableMarriageProblem stable marriage problem StableMatrix stable matrix StableRandomVariable stable random variable StableSortingAlgorithm stable sorting algorithm StableSubspace stable subspace StablyFinite stably finite Stack stack StairFunction stair function Stalk