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.

  • $\begingroup$ You can see also this post for a related example. $\endgroup$ – 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.

  • $\begingroup$ Is this answer about the models for sentences such as the McKinsey formula? I don't quite understand. $\endgroup$ – Nikolaj-K Dec 15 '14 at 17:00
  • $\begingroup$ @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). $\endgroup$ – Mauro ALLEGRANZA Dec 15 '14 at 17:15

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.