# 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?

## 2 Answers

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 ...).

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.

• I would dispute your first sentence: derivability is not something that can be talked about directly in PA (PA talks about numbers not logical syntax); PA can also be used to talk (indirectly) about sets (which, in its standard model, are finite). So entailment can be modelled in PA, but the resulting model is less satisfactory than its model of derivability. – Rob Arthan Jan 20 '16 at 23:08
• @RobArthan If you can only talk about finite models, you can't talk about models in any meaningful sense as far as the completeness theorem is concerned. Yes, PA can work with finite models, but that's not really relevant. – Noah Schweber Jan 20 '16 at 23:25
• so how does PA talk directlly about syntax? – Rob Arthan Jan 20 '16 at 23:59
• @RobArthan I consider Godel coding to be direct. Meanwhile, there is no coding mechanism whereby PA can talk about arbitrary structures, and finite structures simply are not sufficient for saying anything interesting in the context of the completeness theorem. – Noah Schweber Jan 21 '16 at 0:01
• @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