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$ .∎
随便看	proof of theorem for normal matrices ProofOfTheoremOnEquivalentValuations proof of theorem on equivalent valuations ProofOfTheoremsInAdditivelyIndecomposable proof of theorems in additively indecomposable ProofOfThePowerRule proof of the power rule ProofOfTheRingOfIntegersOfANumberFieldIsFinitelyGeneratedOvermathbbZ proof of the ring of integers of a number field is finitely generated over ℤ ProofOfTheUniformizationTheorem proof of the uniformization theorem ProofOfTheWeakNullstellensatz proof of the weak Nullstellensatz ProofOfTheWellfoundedInductionPrinciple proof of the well-founded induction principle ProofOfThirdIsomorphismTheorem proof of third isomorphism theorem ProofOfThuesLemma proof of Thue’s Lemma ProofOfTietzeExtensionTheorem proof of Tietze extension theorem ProofOfTopologicallyIrreducibleRepresentationsAreAlgebraicallyIrreducibleForCalgebras proof of topologically irreducible representations are algebraically irreducible for C^*-algebras ProofOfTranscendentalRootTheorem proof of transcendental root theorem