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 $u{R}_{1}w$, then $f(u){R}_{2}f(w)$,

•
if $s{R}_{2}t$ and $s=f(u)$ for some $u\in {W}_{1}$, then $u{R}_{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

•
${M}_{1}{\vDash}_{w}p$ iff ${M}_{2}{\vDash}_{f(w)}p$ for any propositional variable $p$.
Proposition 1.
For any wff $A$, ${M}_{\mathrm{1}}{\mathrm{\vDash}}_{w}A$ iff ${M}_{\mathrm{2}}{\mathrm{\vDash}}_{f\mathit{}\mathrm{(}w\mathrm{)}}A$.
Proof.
Induct on the number $n$ of logical connectives in $A$. When $n=0$, $A$ is either $\u27c2$ or a propositional variable. The case when $A$ is $\u27c2$ is obvious, and the other case is definition. Next, suppose $A$ is $B\to C$, then ${M}_{1}{\vDash}_{w}A$ iff ${M}_{1}{\vDash \u0338}_{w}B$ or ${M}_{1}{\vDash}_{w}C$ iff ${M}_{2}{\vDash \u0338}_{f(w)}B$ or ${M}_{2}{\vDash}_{f(w)}C$ iff ${M}_{2}{\vDash}_{f(w)}A$. Finally, suppose $A$ is $\mathrm{\square}B$, and ${M}_{1}{\vDash}_{w}A$. To show ${M}_{2}{\vDash}_{f(w)}A$, let $t$ be such that $f(w){R}_{2}t$. Then there is a $u$ such that $t=f(u)$ and $w{R}_{1}u$, so that ${M}_{1}{\vDash}_{u}B$. By induction^{}, ${M}_{2}{\vDash}_{f(u)}B$, or ${M}_{2}{\vDash}_{t}B$. Hence ${M}_{2}{\vDash}_{f(w)}A$. Conversely, suppose ${M}_{2}{\vDash}_{f(w)}A$. To show ${M}_{1}{\vDash}_{w}A$, let $u$ be such that $w{R}_{1}u$. So $f(w){R}_{2}f(u)$, and therefore ${M}_{2}{\vDash}_{f(u)}B$. By induction, ${M}_{1}{\vDash}_{u}B$, whence ${M}_{1}{\vDash}_{w}A$. ∎
Proposition 2.
If a pmorphism $f\mathrm{:}{\mathrm{F}}_{\mathrm{1}}\mathrm{\to}{\mathrm{F}}_{\mathrm{2}}$ is onetoone, then ${\mathrm{F}}_{\mathrm{2}}\mathrm{\vDash}A$ implies ${\mathrm{F}}_{\mathrm{1}}\mathrm{\vDash}A$ for any wff $A$.
Proof.
Suppose ${\mathcal{F}}_{2}\vDash 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{\vDash}_{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)\ne \mathrm{\varnothing}\}$. Then $M{\vDash}_{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)\ne \mathrm{\varnothing}$ iff $f(w)\in {V}_{2}(p)$ iff ${M}^{\prime}{\vDash}_{f(w)}p$. This shows that $f$ is a pmorphism from $M$ to ${M}^{\prime}$.
Now, let $w\in {W}_{1}$. Then ${M}^{\prime}{\vDash}_{f(w)}A$ by assumption^{}. By the last proposition^{}, $M{\vDash}_{w}A$. ∎
Proposition 3.
If a pmorphism $f\mathrm{:}{\mathrm{F}}_{\mathrm{1}}\mathrm{\to}{\mathrm{F}}_{\mathrm{2}}$ is onto, then ${\mathrm{F}}_{\mathrm{1}}\mathrm{\vDash}A$ implies ${\mathrm{F}}_{\mathrm{2}}\mathrm{\vDash}A$ for any wff $A$.
Proof.
Suppose ${\mathcal{F}}_{1}\vDash 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{\vDash}_{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}\vDash A$ for any wff $A$.
Now, let $w\in {W}_{1}$ be a world such that $f(w)=s$. Since ${M}^{\prime}\vDash A$, ${M}^{\prime}{\vDash}_{w}A$ in particular, and therefore $M{\vDash}_{f(w)}A$ or $M{\vDash}_{s}A$ by the last proposition. ∎
Corollary 1.
If $f\mathrm{:}{\mathrm{F}}_{\mathrm{1}}\mathrm{\to}{\mathrm{F}}_{\mathrm{2}}$ is bijective^{}, then ${\mathrm{F}}_{\mathrm{1}}\mathrm{\vDash}A$ iff ${\mathrm{F}}_{\mathrm{2}}\mathrm{\vDash}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 $$ 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, $$ 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}$. ∎
Title  pmorphism 

Canonical name  Pmorphism 
Date of creation  20130322 19:34:54 
Last modified on  20130322 19:34:54 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  12 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B45 
Related topic  Bisimulation 
\@unrecurse 