You are here
Homepmorphism
Primary tabs
pmorphism
Let $\mathcal{F}_{1}=(W_{1},R_{1})$ and $\mathcal{F}_{2}=(W_{2},R_{2})$ be Kripke frames. A pmorphism from $\mathcal{F}_{1}$ to $\mathcal{F}_{2}$ is a function $f:W_{1}\to W_{2}$ such that

if $uR_{1}w$, then $f(u)R_{2}f(w)$,

if $sR_{2}t$ and $s=f(u)$ for some $u\in W_{1}$, then $uR_{1}w$ and $t=f(w)$ for some $w\in W_{1}$,
We write $f:\mathcal{F}_{1}\to\mathcal{F}_{2}$ to denote that $f$ is a pmorphism from $\mathcal{F}_{1}$ to $\mathcal{F}_{2}$.
Let $M_{1}=(\mathcal{F}_{1},V_{1})$ and $M_{2}=(\mathcal{F}_{2},V_{2})$ be Kripke models of modal propositional logic PL${}_{M}$. A pmorphism from $M_{1}$ to $M_{2}$ is a pmorphism $f:\mathcal{F}_{1}\to\mathcal{F}_{2}$ such that
Proposition 1.
For any wff $A$, $M_{1}\models_{w}A$ iff $M_{2}\models_{{f(w)}}A$.
Proof.
Induct on the number $n$ of logical connectives in $A$. When $n=0$, $A$ is either $\perp$ or a propositional variable. The case when $A$ is $\perp$ is obvious, and the other case is definition. Next, suppose $A$ is $B\to C$, then $M_{1}\models_{w}A$ iff $M_{1}\not\models_{w}B$ or $M_{1}\models_{w}C$ iff $M_{2}\not\models_{{f(w)}}B$ or $M_{2}\models_{{f(w)}}C$ iff $M_{2}\models_{{f(w)}}A$. Finally, suppose $A$ is $\square B$, and $M_{1}\models_{w}A$. To show $M_{2}\models_{{f(w)}}A$, let $t$ be such that $f(w)R_{2}t$. Then there is a $u$ such that $t=f(u)$ and $wR_{1}u$, so that $M_{1}\models_{u}B$. By induction, $M_{2}\models_{{f(u)}}B$, or $M_{2}\models_{t}B$. Hence $M_{2}\models_{{f(w)}}A$. Conversely, suppose $M_{2}\models_{{f(w)}}A$. To show $M_{1}\models_{w}A$, let $u$ be such that $wR_{1}u$. So $f(w)R_{2}f(u)$, and therefore $M_{2}\models_{{f(u)}}B$. By induction, $M_{1}\models_{u}B$, whence $M_{1}\models_{w}A$. ∎
Proposition 2.
If a pmorphism $f:\mathcal{F}_{1}\to\mathcal{F}_{2}$ is onetoone, then $\mathcal{F}_{2}\models A$ implies $\mathcal{F}_{1}\models A$ for any wff $A$.
Proof.
Suppose $\mathcal{F}_{2}\models A$. Let $M=(W_{1},R_{1},V_{1})$ be any model based on $\mathcal{F}_{1}$ and $w$ any world in $W_{1}$. We want to show that $M\models_{w}A$.
Define a Kripke model $M^{{\prime}}:=(W_{2},R_{2},V_{2})$ as follows: for any propositional variable $p$, let $V_{2}(p):=\{s\in W_{2}\mid f^{{1}}(s)\cap V_{1}(p)\neq\varnothing\}$. Then $M\models_{w}p$ iff $w\in V_{1}(p)$ iff $f^{{1}}(f(w))=\{w\}\subseteq V_{1}(p)$ (since $f$ is onetoone) iff $f^{{1}}(f(w))\cap V_{1}(p)\neq\varnothing$ iff $f(w)\in V_{2}(p)$ iff $M^{{\prime}}\models_{{f(w)}}p$. This shows that $f$ is a pmorphism from $M$ to $M^{{\prime}}$.
Now, let $w\in W_{1}$. Then $M^{{\prime}}\models_{{f(w)}}A$ by assumption. By the last proposition, $M\models_{w}A$. ∎
Proposition 3.
If a pmorphism $f:\mathcal{F}_{1}\to\mathcal{F}_{2}$ is onto, then $\mathcal{F}_{1}\models A$ implies $\mathcal{F}_{2}\models A$ for any wff $A$.
Proof.
Suppose $\mathcal{F}_{1}\models A$. Let $M=(W_{2},R_{2},V_{2})$ be any model based on $\mathcal{F}_{2}$ and $s$ any world in $W_{2}$. We want to show that $M\models_{s}A$.
Define a Kripke model $M^{{\prime}}:=(W_{1},R_{1},V_{1})$ as follows: for any propositional variable $p$, let $V_{1}(p):=\{w\in W_{1}\mid f(w)\in V_{2}(p)\}$. Then $w\in V_{1}(p)$ iff $f(w)\in V_{2}(p)$, so $f$ is a pmorphism from $M^{{\prime}}$ to $M$, and by assumption $M^{{\prime}}\models A$ for any wff $A$.
Now, let $w\in W_{1}$ be a world such that $f(w)=s$. Since $M^{{\prime}}\models A$, $M^{{\prime}}\models_{w}A$ in particular, and therefore $M\models_{{f(w)}}A$ or $M\models_{s}A$ by the last proposition. ∎
Corollary 1.
If $f:\mathcal{F}_{1}\to\mathcal{F}_{2}$ is bijective, then $\mathcal{F}_{1}\models A$ iff $\mathcal{F}_{2}\models A$ for any wff $A$.
A frame $\mathcal{F}^{{\prime}}$ is said to be a pmorphic image of a frame $\mathcal{F}$ if there is an onto pmorphism $f:\mathcal{F}\to\mathcal{F}^{{\prime}}$. Let $\mathcal{C}$ be the class of all frames validating a wff. Then by the third proposition above, $\mathcal{C}$ is closed under pmorphic images: if a frame is in $\mathcal{C}$, so is any of its pmorphic images. Using this property, we can show the following: if $\mathcal{C}$ is the class of all frames validating a wff $A$, then $\mathcal{C}$ can not be

the class of all irreflexive frames

the class of all asymetric frames

the class of all antisymmetric frames
Proof.
Let $\mathcal{F}_{1}=(\mathbb{N},<)$ and $\mathcal{F}_{2}=(\{0\},R)$, where $0R0$. Notice that $\mathcal{F}_{1}$ is in both the class of irreflexive frames and the class of asymetric frames, but $\mathcal{F}_{2}$ is in neither. Let $f:\mathbb{N}\to\{0\}$ be the obvious surjection. Clearly, $m<n$ implies $f(m)Rf(n)$. Also, if $f(m)R0$, then $f(m)Rf(m+1)$. So $f$ is a pmorphism. Suppose $\mathcal{C}$ is either the class of all irreflexive frames or the class of all asymetric frames. If $A$ is validated by $\mathcal{C}$, $A$ is validated by $\mathcal{F}_{1}$ in particular (since $\mathcal{F}_{1}$ is in $\mathcal{C}$), so that $A$ is validated by $\mathcal{F}_{2}$ as well, which means $\mathcal{F}_{2}$ is $\mathcal{C}$ too, a contradiction. Therefore, no such an $A$ exists.
Next, let $\mathcal{F}_{3}=(\mathbb{N},S)$, where $nS(n+1)$ for all $n\in\mathbb{N}$ and $\mathcal{F}_{4}=(\{0,1\},R)$, where $R=\{(0,1),(1,0)\}$. Let $\mathcal{C}$ be the class of all antisymmetric frames. Then $\mathcal{F}_{3}$ is in $\mathcal{C}$ but $\mathcal{F}_{4}$ is not. Let $f:\mathcal{F}_{3}\to\mathcal{F}_{4}$ be given by $f(n)=0$ if $n$ is even and $f(n)=1$ if $n$ is odd. If $aSb$, then $f(a)$ and $f(b)$ differ by $1$, so $f(a)Rf(b)$. On the other hand, if $f(a)Rx$, then $x$ is either $0$ or $1$, depending on whether $a$ odd or even. Pick $b=a+1$, so $aSb$ and $f(b)=x$. This shows that $f$ is a pmorphism. By the same argument as in the last paragraph, no wff $A$ is validated by precisely the members of $\mathcal{C}$. ∎
Mathematics Subject Classification
03B45 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections