Simple model-theoretic arguments in set theory

Question

Consider the following simple proof that PA has models with nonstandard numbers.

The type $\{ x > n \mid n \in \mathbb{N} \}$ is finitely realizable, so there is an $M \models \mathrm{PA}$ which fully realizes it. Any realization of this type is larger than all the standard natural numbers. QED

Arguments of this kind, and analogous ones via omitting types instead of realizing them, are the bread and butter of model theory. My question is this. Are there any obvious reasons why simple arguments of this kind can't prove the basic results of undecidability?

Naively, "PA doesn't prove its own consistency" is equivalent to "there is $M \models \mathrm{PA}$ which contains a proof of 0=1". (Of course, such a proof would be nonstandard.) I tried for a bit to prove this by a type-realization argument like the one above, but couldn't. Are there known obstacles to such a strategy?

Relatedly, could there be a simple type realizing/omitting argument to construct an $M \models \mathrm{PA}$ which contains some sentence $\varphi$ such that, in M, there are no proofs of $\varphi$ nor $\lnot\varphi$? This wouldn't quite show incompleteness of PA (as $\varphi$ could be nonstandard) but it would be interesting to me.

In general, I guess I'm looking for a bit more of a connection between basic computability and basic model theory -- even if the connection is, "here are good reasons why simple methods from the latter don't work in the former".

Answer 1

The point is that any technique for showing that (say) $\mathsf{PA}$ is incomplete must use something rather special about $\mathsf{PA}$, such as its computable axiomatizability. This is because there are in fact complete consistent extensions of $\mathsf{PA}$; the most obvious example is true arithmetic $\mathsf{TA}=Th(\mathbb{N};+,\times)$, but there are more exotic examples as well.

Basic model theory does provide us with quite flexible tools for building models with various sructural properties (compactness, Lowenheim-Skolem, omitting types). However, these tools are too flexible for establishing independence results: since they apply to all theories without finite models, including complete ones, they can't possibly be used to establish incompleteness.

Answer 2

Here's one explanation, not too far from the lines Noah is drawing in his answer.

How do you prove your result? Well, first you say, add a constant $c$ and axioms stating that it is realising this type. These are finitely consistent, using $\Bbb N$ itself as a model. So by compactness, there is a model where this type is realised. But how do you prove this compactness result? Using ultraproducts and Łoś's theorem, usually,¹ and therefore in this case the model where you realise the type is elementarily equivalent to $\Bbb N$. If we want a countable model, we use the Löwenheim–Skolem theorem, which also preserve elementarity.

So all of the steps we took to get to the model do not change the theory, and in fact, do not change the theory of the language expanded with constants for the original model (in this case this is unnecessary since $\Bbb N$ is very nice: every element has a closed term which defines it).

Therefore, we did not produce a model of $\sf PA$ whose theory is different from that of $\Bbb N$. Now you can argue that "in principle, we could have!" but to do that you'd have to use other models of $\sf PA$ first, and you don't yet know they exist (in principle). Only after we have proved the incompleteness of $\sf PA$ you can use the fact that there models with different theories.

---

_{1. Once I was discussing choice-related stuff with a model theorist, and they were quite surprised to find out that compactness does not follow from Łoś's theorem, as a general principle, and it is just a rather convenient proof we get in $\sf ZFC$. The point is that in $\sf ZF$ the compactness theorem is independent from Łoś's theorem.}