• Consider sublanguages of all languages that encode models via the standard model encoding.
• Which of these languages can be recognized by NP?
• Crazy theorem: the ones that are exactly describable by monadic second order logic .
• Subtlety: we first fix the formula, and we then solve the problem if a model (encoded as a string) makes the formula true
• Sketch of MSO can be accepted by NP: First see that MSO can be figured out by NP: Make the guess for the relation, then do the usual thing of testing a fixed formula. We need as many loops as there are quantifiers in the formula. But since the formula is fixed, this is $n^k$ where $n$ is the size of the model / size of the input string. So we are done.

§ Hard part: every NP model property can be figured out by MSO

• Key idea: we want to run cook-levin, but we don't have booleans.
• Note that the largest numbers we will ever need to do cook levin are at most $n^k$ for some fixed $k$ (running time of NP machine).
• Use MSO to pick a total order on the model.
• On a finite model, a total order is an ordinal!
• From this, get integers [0...n). Example: 0 is the smallest integer. so it is given by the least element in the ordering, so exists x, forall y, x <= y.
• Successor is given by "next" element in the ordering. succ(x) is the element y such that x < y and there is no z such that x < y < z.
• OK, but we need n^k.
• Get n^k by building tuples MxMx..xM and imposing lex ordering! lex ordering can also be expressed as a FOL formula.
• Done, we have arithmetic upto n^k.
• Sweet, now run cook-levin inside the model using our arithmetic. sugoi!