Model-checking and Turing Machines

Question

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.

Answer 1

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.