Church-Rosser property and normal modal logic

I am trying to prove soundness and completeness for S4.2 and I am considering Kripke frames which are reflexive, transitive and have the Church-Rosser property. Now, there is one thing that really puzzles me, though it might be quite obvious and due to some triviality I'm currently missing.

If I compute the corresponding Sahlqvist formula for $\Diamond\Box p \rightarrow \Box\Diamond p$ (which is an axiom of S4.2) what I obtain is $\forall x,y,z (Rxy \land Rxz \rightarrow \exists w (Ryw \land Rzw))$. So I take the former axiom of S4.2 to define the class of Kripke-frames which have the Church-Rosser property.

However, it seems to me that it is possible to find a conterexample: just consider the Kripke-model$\mathbb{M}=(W,R,V)$ where:

• W= {1, 2, 3, 4, 5, 6, 7}
• R= {R12, R13, R24, R35, R57, R46}
• V(p)={3, 4}

So we seem to have that $\mathbb{M}\vDash \Diamond\Box p \rightarrow \Box\Diamond p$. However, this frame clearly does not have the Church-Rosser property. Thus there is an evaluation $V$ s.t. the frame (W,R) validates the axioms of S4.2 but it does not have the Church-Rosser property.

I guess there some mistake in this reasoning, but I don't understand where and why. Can someone help?

• At a glance, I think the point is that your frame does not validate $S4.2$ - there is a valuation on the frame which satisfies $S4.2$, but it is not the case that every valuation on that frame satisfies $S4.2$. And the claim is only that the frames which validate $S4.2$ have the Church-Rosser property. (And there are simpler examples: for any frame at all, the valuation making $p$ true at every world satisfies $\Diamond\Box p\implies \Box\Diamond p$.) – Noah Schweber Nov 10 '17 at 2:00
• I think you're right. Thank you very much. – D.Q. Nov 10 '17 at 13:51

To say that a frame validates a sentence is to say that every valuation on that frame makes the sentence true. You have found a valuation on a frame which makes $S4.2$ true, but the frame does not in fact validate $S4.2$ - there is a valuation on it which makes $\Diamond\Box p\rightarrow\Box\Diamond p$ false (exercise).
(It's worth observing that for any frame, the valuation making every atomic sentence true at every world satisfies all $\neg$-free sentences; and meanwhile any valuation on the one-point irreflexive frame makes every sentence of the form $\Box \varphi$ or of the form $(\Diamond \varphi)\implies\psi$ true.)