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

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?

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.
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.
• @RobArthan OK, but then the version of the completeness theorem you can express is false: first-order logic is not complete for finite structures. (E.g. the set $\{$"there are $\ge n$ elements": $n\in\omega\}$ semantically entails $\perp$ for finite models, but obviously doesn't prove $\perp$.) I guess I don't call false statements satisfactory. I think we'll have to agree to disagree on this point, as well as whether it's moot (I think the OP is interested in the actual compactness theorem). – Noah Schweber Jan 21 '16 at 3:30