I am looking for a Kripke frame condition corresponding to the McKinsey axiom M: $\Box\Diamond p \rightarrow \Diamond\Box p$. I read somewhere the following condition:

"For every partitioning of the set of worlds into two disjoint partitions, every world can see a world whose successors lie all in the same partition."

This follows from rewriting the formula as $\Diamond\Box \lnot p \lor \Diamond\Box p$. But it is difficult to use because it involves sets of worlds.

So I am looking for a frame condition for KM of the form $\forall w P(w)$, where $P$ is a predicate expressing visibility between $w$ and other worlds. In the case of M, this condition cannot be first-order, but it could still be second order. For example:

  • Formula $(p\land \Box(\Diamond p \rightarrow p)) \rightarrow \Box p$ corresponds to frames for which $\forall w$, if $wRw'$ then there is a finite sequence $w_0,...,w_n$ such that $w_0=w'$, $w_0Rw_1Rw_2...Rw_nRw$ and also $wRw_i$ for $1\le i \le n$. See article A Simple Incomplete Extension of T which is the Union of Two Complete Modal Logics with f.m.p. by Roy A. Benton.

  • Formula $\Box(\Box p \rightarrow p) \rightarrow \Box p$ (Loeb) corresponds to frames for which $\forall w$ we have $wRw' \land w'Rw'' \rightarrow wRw''$ (transitive) and also there is no infinite sequence of worlds $wRw_1Rw_2R...$ starting from $w$ (converse well-founded). See P. Blackburn Modal Logic pp 131; it is also shown there that both the Loeb and the McKinsey formulas do not correspond to a first order condition.

The above examples are not first-order conditions. But note that they describe their class of frames by stating what an arbitrary world can see, i.e. without using a partition or a valuation.

So my question is: is there a similar frame condition known for axiom M?

This should correspond to the frames of KM itself, i.e not in conjunction with other axioms. My hope is that in such a form it would be better suited for analyzing the extensions of KM − any extension, not just K4M.

  • $\begingroup$ How would you formalize the condition that "$P$ is a predicate expressing visibility between $w$ and other worlds" in a way that excludes the condition you gave, if you're allowing $P$ to be second-order? Do you mean that $P$ has access to an extra "reachability" relation, aside from the visibility one, but that no explicit second-order quantification is allowed? $\endgroup$ May 12 '15 at 17:38
  • $\begingroup$ Let $P(w)$ say that $p$ holds at world $w$, and leq $R(w,v)$ say that $v$ is visibile from $w$. Then the McKinsey axiom is directly stated as $(\forall w)(\exists v)[R(w,v) \land P(v)] \to (\exists w)(\forall v)[R(w,v) \to P(v)]$. If that is not what you are looking for, can you clarify what you are looking for? $\endgroup$ May 12 '15 at 17:51
  • $\begingroup$ @Gregory J. Puleo: I am not sure how to formalize this, but I would like something that does not quantify over partitions of worlds. Something like in the example I gave (there are formulas that correspond to such descriptions.) As I understand, $w$ sees $w'$ in one step or in two steps is first-order, but in a finite number of steps is not. The purpose is to get a condition which can be combined more easily with other frame conditions like transitivity, convergence etc. $\endgroup$
    – JuneA
    May 12 '15 at 17:54
  • $\begingroup$ @Carl Mummert: I would like something that does not involve the valuations $P(v)$. Only who sees who if possible. $\endgroup$
    – JuneA
    May 12 '15 at 17:58
  • $\begingroup$ Edited to clarify, added examples. $\endgroup$
    – JuneA
    May 13 '15 at 4:55

I believe the question is answered by the following paper;

  • "A Note on Modal Formulae and Relational Properties", J. F. A. K. van Benthem, The Journal of Symbolic Logic, Vol. 40, No. 1 (Mar., 1975), pp. 55-58. DOI: 10.2307/2272270 URL: http://www.jstor.org/stable/2272270

which states:

Theorem 1. There is no first-order formula $\phi$ such that $F \vDash \phi \Leftrightarrow F \vdash \Box\Diamond p \to \Diamond \Box p$ for all $F$.

I found the result cited in

  • "The McKinsey Axiom is not Canonical", Robert Goldblatt, The Journal of Symbolic Logic, Vol. 56, No. 2 (Jun., 1991), pp. 554-562, DOI: 10.2307/2274699 URL: http://www.jstor.org/stable/2274699

Goldblatt attributes the result independently to van Benthem's paper above and to his own paper

  • "First-Order Definability in Modal Logic", R. I. Goldblatt, The Journal of Symbolic Logic, Vol. 40, No. 1 (Mar., 1975), pp. 35-40. DOI: 10.2307/2272267 URL: http://www.jstor.org/stable/2272267
  • $\begingroup$ I understand that the class of frames corresponding to M is not first-order definable. But does this mean there is no frame condition of the form I am asking? $\endgroup$
    – JuneA
    May 13 '15 at 4:48

See :

  • Alexander Chagrov & Michael Zakharyaschev, Modal Logic (1997), page 82 :

A transitive frame $\mathfrak F$ validates the McKinsey formula iff satisfies the McKinsey condition

where the McKinsey condition is :

$\forall x \exists y(xRy \land \forall z(yRz \to y=z))$.

  • $\begingroup$ Yes, this is also called "every world sees a final world" in Hughes&Cresswell pp. 131. But it only works in conjunction with axiom 4, i.e. in K4M, or in S4.M if also reflexive. I am looking for a frame characterzation of KM. $\endgroup$
    – JuneA
    May 13 '15 at 4:49

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.