Is it possible to formalize $T \models \sigma$ within the deductive calculus?

Question

I know that the notion of $T \vdash \sigma$ is formalizable within any sufficiently powerful theory $T$ but is $T \models \sigma$ formalizable as well? How is this possible if there are infinitely many models (including uncountable ones) to consider? And if it's not possible then doesn't the completeness theorem contradict itself because it is a true theorem which cannot be proven through the deductive calculus?

Answer 1

To formalize a notion in a theory $T$ means to represent the notion using the language of $T$. When we do this we make a value judgment about the fidelity of that representation. If we are formalizing "syntactic" notions like $T \vdash \sigma$ in PA, our representions of syntax as numbers need to be faithful to our intuitions about syntax, but we tend to be fairly complacent about the representation of one kind of finitistic object as another. In ZF set theory, we can formalize the "semantic" notion $T \models \sigma$ and prove the completeness theorem for first-order logic. To do this, the representation of models as sets need to be faithful to our intuitions about models. We may be less comfortable with a language that can talk about things like uncountable sets, but the concepts involved in the definition of a model aren't difficult.

You may find it useful to read about Tarski's concept of a metalanguage http://plato.stanford.edu/entries/tarski-truth/. This lets you formalize the notion of formalization and eliminates the meta-level "value judgments" I mentioned above (but then gives you a meta-meta-level to worry about ...).

Answer 2

Certainly semantic entailment is not something which can be directly talked about in $PA$ (although it can be in ZF); however, note that this does not contradict the completeness theorem. Completeness only says "any sentence which is a semantic consequence of $T$ and is expressible in the language of $T$ is provable in $T$." This expressibility condition is crucial.