This paragraph in the wikipedia page of the P vs NP problem tries to explain a characterization of languages in P and those in NP, however this characterization is not very clearly stated.
Indeed, for first order logic they say "the language of a finite structure with a fixed signature including a linear order relation [with a suitable fixed point combinator]"; but it's not clear what this means, and it doesn't seem to be explained further.
For existential second order logic, the article just says "NP is the set of languages expressible in existential second-order logic" without any explanation: what does it mean for a language to be expressible in (existential) second-order logic ?
So my question is
What do these characterizations mean, precisely ?
To answer, you can assume I know what a formal language is, that I know what first order logic and existential second order logic, and that I know some decent amount of model theory. Note that I'm not asking for a proof of the characterization (although if there is a quick one I won't mind seeing it), just for a definition of the characterization.