p-morphism
Let and be Kripke frames. A p-morphism from to is a function such that
-
•
if , then ,
-
•
if and for some , then and for some ,
We write to denote that is a p-morphism from to .
Let and be Kripke models of modal propositional logic PL. A p-morphism from to is a p-morphism such that
-
•
iff for any propositional variable .
Proposition 1.
For any wff , iff .
Proof.
Induct on the number of logical connectives in . When , is either or a propositional variable. The case when is is obvious, and the other case is definition. Next, suppose is , then iff or iff or iff . Finally, suppose is , and . To show , let be such that . Then there is a such that and , so that . By induction, , or . Hence . Conversely, suppose . To show , let be such that . So , and therefore . By induction, , whence . ∎
Proposition 2.
If a p-morphism is one-to-one, then implies for any wff .
Proof.
Suppose . Let be any model based on and any world in . We want to show that .
Define a Kripke model as follows: for any propositional variable , let . Then iff iff (since is one-to-one) iff iff iff . This shows that is a p-morphism from to .
Now, let . Then by assumption. By the last proposition, . ∎
Proposition 3.
If a p-morphism is onto, then implies for any wff .
Proof.
Suppose . Let be any model based on and any world in . We want to show that .
Define a Kripke model as follows: for any propositional variable , let . Then iff , so is a p-morphism from to , and by assumption for any wff .
Now, let be a world such that . Since , in particular, and therefore or by the last proposition. ∎
Corollary 1.
If is bijective, then iff for any wff .
A frame is said to be a p-morphic image of a frame if there is an onto p-morphism . Let be the class of all frames validating a wff. Then by the third proposition above, is closed under p-morphic images: if a frame is in , so is any of its p-morphic images. Using this property, we can show the following: if is the class of all frames validating a wff , then can not be
-
•
the class of all irreflexive frames
-
•
the class of all asymetric frames
-
•
the class of all anti-symmetric frames
Proof.
Let and , where . Notice that is in both the class of irreflexive frames and the class of asymetric frames, but is in neither. Let be the obvious surjection. Clearly, implies . Also, if , then . So is a p-morphism. Suppose is either the class of all irreflexive frames or the class of all asymetric frames. If is validated by , is validated by in particular (since is in ), so that is validated by as well, which means is too, a contradiction. Therefore, no such an exists.
Next, let , where for all and , where . Let be the class of all anti-symmetric frames. Then is in but is not. Let be given by if is even and if is odd. If , then and differ by , so . On the other hand, if , then is either or , depending on whether odd or even. Pick , so and . This shows that is a p-morphism. By the same argument as in the last paragraph, no wff is validated by precisely the members of . ∎
Title | p-morphism |
---|---|
Canonical name | Pmorphism |
Date of creation | 2013-03-22 19:34:54 |
Last modified on | 2013-03-22 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 |