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?

  • $\begingroup$ 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$.) $\endgroup$ – Noah Schweber Nov 10 '17 at 2:00
  • $\begingroup$ I think you're right. Thank you very much. $\endgroup$ – 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.)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.