What does not having a first-order frame imply for models?

There are formulas in modal logic which which do not have a first-order frame condition, as stated here (Non-Sahlqvist formulas, Wikipedia). An example is the McKinsey formula for $p$:

$$\Box\,\Diamond\,p\rightarrow \Diamond\,\Box\,p$$

"If it's necessary that it's possible that $p$, then it's possible that it's necessary that p."

What exactly does not having a first-order frame frame mean for models of theories that contains such statements. Does this this just mean we can't replace the modal language with a first-order language, or is it more severe? If there are models, what's a simple example for a theory of some things or a situation for which the formula holds.

I'm interested in modal operators because I've seen them popping up in a form of their categorical models. Regarding this question, is there an argument to add modal operators to our formal language - it's curious how they don't seem to be used much outside of philosphy and I try to find out if it's because the relevant notions they can express are captured by the standard language anyway.

• You can see also this post for a related example. – Mauro ALLEGRANZA Dec 15 '14 at 17:31

You can see :

we will prove a theorem that may be used to determine conditions on $R$ from axioms (and vice versa) for a wide range of axioms (Lemmon and Scott, 1977). (For a more general result of this kind see Sahlqvist, 1975 $[1]$.)

The theorem concerns axioms that have the form :

(G) $\ \ \Diamond^h \Box^i A \rightarrow \Box^j \Diamond^k A.$

The notation ‘$\Diamond^n$’ represents $n$ diamonds in a row, so, for example, ‘$\Diamond^3$’ abbreviates: $\Diamond \Diamond \Diamond$. Similarly, ‘$\Box^n$’ represents a string of $n$ boxes. When the values of $h,i,j$, and $k$ are all $1$, we have axiom :

(C) $\ \ \Diamond \Box A \rightarrow \Box \Diamond A.$

The axiom (B) results from setting $h$ and $k$ to $0$, and letting $j$ and $k$ be 1.

(B) $\ \ A \rightarrow \Box \Diamond A.$

To obtain (4), we may set $h$ and $k$ to $0$, set $i$ to $1$ and $j$ to $2$.

(4) $\ \ \Box A \rightarrow \Box \Box A.$

[...]

It is interesting to see how the diagrams for the familiar conditions on $R$ result from setting the values for $h, i, j$, and $k$ according to the values in the corresponding axiom [page 213].

For (B), we have that the condition on $R$ amounts to symmetry that, as per your Wiki's reference, can be expressed with condition on the relation $R$ in first-order language : $\forall w_1 \forall w_2(w_1Rw_2 \rightarrow w_2Rw_1)$.

For (4), it amounts to transitivity, i.e. $\forall w_1 \forall w_2 \forall w_3(w_1Rw_2 \land w_2Rw_3 \rightarrow w_1Rw_3)$.

For :

(D) $\ \ \Box A \rightarrow \Diamond A$

we have seriality : $\forall w_1 \exists w_2 (w_1Rw_2)$.

For McKinsey formula see :

• Patrick Blackburn & Maarten de Rijke & Yde Venema, Modal Logic (2002), page 133 :

Example 3.11 We will show that the McKinsey formula $□◊p → ◊□p$ does not correspond to a first-order condition by showing that it violates the Lowenheim-Skolem theorem.

$[1]$ Henrik Sahlqvist, Completeness and Correspondence in First and Second-Order Semantics for Modal Logic, in Stig Kanger (editor), Proceedings of the Third Scandinavian Logic Symposium (1975), page 110-on.

• Is this answer about the models for sentences such as the McKinsey formula? I don't quite understand. – Nikolaj-K Dec 15 '14 at 17:00
• @NikolajK - according to Wiki, McKinsey formula is "Non-Sahlqvist", i.e. it is not possible to find a corresponding first-order formula for $R$; Wiki's reference for this result is : L.A.Chagrova, An undecidable problem in correspondence theory (1991). – Mauro ALLEGRANZA Dec 15 '14 at 17:15