Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am reading proof of Fagin's theorem, which says

"A problem $\pi$ $\in$ NP iff there is a existential second-order sentence of the form $\phi$ = $\exists{R_1}\exists{R_2}...\exists{R_n}\psi$ , where $\psi$ is a first-order formula such that Mod($\phi$) = $\pi$."

Proving in the direction Mod($\phi$) $\in$ NP , we proceed as follows:

Given structure $\mathcal{A}$ and $\phi$ , NDTM say M, carries out following procedure:

(1) Guesses relations $R_1,R_2,...,R_n$ .

(2) Checks if ($\mathcal{A}$,$R_1,R_2,...,R_n$) $\models$ $\psi$

I know how M guesses relations. My confusion is that how the machine M carries out check in (2). I will build my own understanding someone could just kindly give me any sources where I should go looking for this answer. Any book name etc. Or if you don't know any original sources than please throw some light on it.

share|cite|improve this question
Which formalism is $\psi$ supposed to be in? (For example, it can't be Peano arithmetic, because that can express everything computable and a good deal more even without second-order existentials wrapping it). – Henning Makholm Sep 1 '11 at 1:25
By formalism you mean which logic $\psi$ belongs to? If yes then, $\psi$ is a first-order formula. If no, then sorry I didn't get your question. – user5187 Sep 1 '11 at 3:08
up vote 1 down vote accepted

The model checking can be done by an easy recursive procedure based on the structure of the formula.

It is easy to check the satisification of an atomic formula in a given structure.

If the last operation is a logical connective, we check each of the operand subformulas in the model, and then return the answer based on the connective and the result returned by checking subformulas.

If it is a quantifier, lets say an existential quantifier, then put all possible values (there are only finitely many of them) for the variable and check the satisfiability of the subformula, and return true if one of them returns true.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.