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 :
[...]
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 :
we have seriality : $\forall w_1 \exists w_2 (w_1Rw_2)$.
For McKinsey formula see :
$[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.