# Model-checking and Turing Machines

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.

-
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