p-morphism


Let 1=(W1,R1) and 2=(W2,R2) be Kripke frames. A p-morphism from 1 to 2 is a function f:W1W2 such that

  • if uR1w, then f(u)R2f(w),

  • if sR2t and s=f(u) for some uW1, then uR1w and t=f(w) for some wW1,

We write f:12 to denote that f is a p-morphism from 1 to 2.

Let M1=(1,V1) and M2=(2,V2) be Kripke models of modal propositional logicPlanetmathPlanetmath PLM. A p-morphism from M1 to M2 is a p-morphism f:12 such that

Proposition 1.

For any wff A, M1wA iff M2f(w)A.

Proof.

Induct on the number n of logical connectives in A. When n=0, A is either or a propositional variable. The case when A is is obvious, and the other case is definition. Next, suppose A is BC, then M1wA iff M1⊧̸wB or M1wC iff M2⊧̸f(w)B or M2f(w)C iff M2f(w)A. Finally, suppose A is B, and M1wA. To show M2f(w)A, let t be such that f(w)R2t. Then there is a u such that t=f(u) and wR1u, so that M1uB. By inductionMathworldPlanetmath, M2f(u)B, or M2tB. Hence M2f(w)A. Conversely, suppose M2f(w)A. To show M1wA, let u be such that wR1u. So f(w)R2f(u), and therefore M2f(u)B. By induction, M1uB, whence M1wA. ∎

Proposition 2.

If a p-morphism f:F1F2 is one-to-one, then F2A implies F1A for any wff A.

Proof.

Suppose 2A. Let M=(W1,R1,V1) be any model based on 1 and w any world in W1. We want to show that MwA.

Define a Kripke model M:=(W2,R2,V2) as follows: for any propositional variable p, let V2(p):={sW2f-1(s)V1(p)}. Then Mwp iff wV1(p) iff f-1(f(w))={w}V1(p) (since f is one-to-one) iff f-1(f(w))V1(p) iff f(w)V2(p) iff Mf(w)p. This shows that f is a p-morphism from M to M.

Now, let wW1. Then Mf(w)A by assumptionPlanetmathPlanetmath. By the last propositionPlanetmathPlanetmath, MwA. ∎

Proposition 3.

If a p-morphism f:F1F2 is onto, then F1A implies F2A for any wff A.

Proof.

Suppose 1A. Let M=(W2,R2,V2) be any model based on 2 and s any world in W2. We want to show that MsA.

Define a Kripke model M:=(W1,R1,V1) as follows: for any propositional variable p, let V1(p):={wW1f(w)V2(p)}. Then wV1(p) iff f(w)V2(p), so f is a p-morphism from M to M, and by assumption MA for any wff A.

Now, let wW1 be a world such that f(w)=s. Since MA, MwA in particular, and therefore Mf(w)A or MsA by the last proposition. ∎

Corollary 1.

If f:F1F2 is bijectiveMathworldPlanetmathPlanetmath, then F1A iff F2A for any wff A.

A frame is said to be a p-morphic image of a frame if there is an onto p-morphism f:. 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 A, then 𝒞 can not be

  • the class of all irreflexiveMathworldPlanetmath frames

  • the class of all asymetric frames

  • the class of all anti-symmetric frames

Proof.

Let 1=(,<) and 2=({0},R), where 0R0. Notice that 1 is in both the class of irreflexive frames and the class of asymetric frames, but 2 is in neither. Let f:{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 p-morphism. Suppose 𝒞 is either the class of all irreflexive frames or the class of all asymetric frames. If A is validated by 𝒞, A is validated by 1 in particular (since 1 is in 𝒞), so that A is validated by 2 as well, which means 2 is 𝒞 too, a contradictionMathworldPlanetmathPlanetmath. Therefore, no such an A exists.

Next, let 3=(,S), where nS(n+1) for all n and 4=({0,1},R), where R={(0,1),(1,0)}. Let 𝒞 be the class of all anti-symmetric frames. Then 3 is in 𝒞 but 4 is not. Let f:34 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 p-morphism. By the same argument as in the last paragraph, no wff A 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