I was going through Fagin's Theorem (summary on wiki) and if I understood correctly Existential Second Order Logic (ESO) can be used to represent any NP problem, the same can be said for a Non-deterministic Turing Machine. Now I have a few questions about that:
- If ESO logic is enough to characterise all the NP problems, what does the full Second Order Logic (SOL) characterise more?
- If the answer to the first question is "nothing more", does that mean that any SOL can be reduced to ESO logic (it is true already that Higher Order Logics can be reduced to SOL for instance...)?
- Perhaps I am missing and confusing something to have such questions in mind. Would it be possible to have some papers' link to fill in the gap?