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?
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.)