Is there a more useful formulation of the frame condition for the McKinsey axiom? 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.
 A: 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
A: 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))$.

