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$:
"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.