Could someone explain Fagin's theorem on the equivalence between NP and existential quantifier

This quote on descriptive complexity theory is given in Wikipedia:

"The first main result of descriptive complexity was Fagin's theorem, shown by Ronald Fagin in 1974. It established that NP is precisely the set of languages expressible by sentences of existential second-order logic; that is, second order logic excluding universal quantification over relations, functions, and subsets."

Is there a simple proof of the theorem?

You can check out these lecture notes, as well as countless more. The proof of Fagin's theorem is divided into two parts: showing that every language expressible in existential second-order language is in NP, and showing that every language in NP is expressible in existential second-order language. The first part is easy – we just have to guess the quantified relations. The second part is more complicated, but resembles the proof of Cook's theorem. The idea is that the quantified relations encode the computation of an NP machine.

For more details, you can consult Neil Immerman's book Descriptive Complexity.

StackExchange Computer Science Q#26500, answer score: 5