## § Fagin's theorem

- 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!