The formula expressing the consistency of a theory I read in some set theory book that the consistency of a theory, say $T$ can be expressed as: 
   $$\exists \mathcal{M} (\mathcal{M} {\rm \; is \; a \; model\; and \;} \mathcal{M} \models T)$$
 where everything (model, theory, etc...) has been formalized.
   What is the status of such a statement (i.e. is it $\Sigma^1_2$?)
Thank you
 A: It depends on the complexity of $T$:


*

*If $T$ is recursively enumerable and interprets arithmetic, then the syntactic statement of consistency is $\Pi^0_1$ ("no $n$ codes a proof of $0=1$"). That $T$ interprets arithmetic is not essential, other than to provide a canonical sentence meaning "$T$ is consistent". In general, you just have to fix a sentence $\phi$ in the language of $T$, and the consistency of $T$ can be expressed by saying that "no $n$ codes a proof of $\phi\land\lnot\phi$". (Of course, different $\phi$ give different formulas as a result, which is why I mention lack of "canonicity".) 

*If we go further and remove the assumption of recursive enumerability of $T$, as long as $T$ is countable, we can think of it as a real (coding a theory), and express the above as a $\Pi^0_1$ statement, that now uses the parameter $T$, which we typically write as $\Pi^0_1(T)$.

*If rather than the syntactic version you want the model theoretic (semantic) one, for an arithmetic theory $T$, to claim that there is a model $M$ that satisfies $T$ is $\Sigma^1_1$: We can assume that $M$ is countable, thanks to the downward Löwenheim-Skolem theorem. We can then say that a countable $M$ satisfies $T$ by stating that there is a real coding a model $M$, and formalizing satisfaction, which can be done in a $\Sigma^1_1$ way. 

*Beyond this, for countable theories you would need using $T$ as a parameter, and the semantic version of the statement will be $\Sigma^1_1(T)$. 


In any case, these statements are definitely absolute between transitive models of enough set theory (having $T$ as an element).  
Details of the formalization can be found in Devlin's book on constructibility (and probably also in Drake's book on large cardinals). Particularly, Devlin's book presents the argument in good amount of detail, since this is relevant to computing the complexity of $0^\sharp$. 
