what does it mean for a problem to be non first order definable?

Question

I was wondering if it yields any information about the minimum complexity of its probable solutions or should it give us any intuition about the properties of the problem?

Answer 1

I have just found the answer to my question from 2 years ago. In short, it does not tell us a lot about the complexity of the problem.

On one side, graph reachability can not be expressed by an $\operatorname{FO}[\sigma]$-formula for $\sigma = \{E_{/2}\}$ (this result can by seen by Hanf locality results or by Ehrenfeucht Fraisse games), which means that not every problem in $P$ can be written as an $\operatorname{FO}[\sigma]$-formula for some $\sigma$.

On the other side, by Trakhtenbrot's Lemma, the finite satisfiability of $\operatorname{FO}[\sigma]$-formulas is not decidable (but semi-decidable), even when we restrict ourselves to $\sigma =\{E_{/2}\}$, namely to directed graphs. More specifically, an undecidable problem, namely the halting problem, can be reduced to the satisfyability problem of a specific first order formula.

---

One the other hands, Fagin's theorem describes the express-ability of second order logik. The theorem states that the set of all properties expressible in existential second-order logic is precisely the complexity class NP.