[Epa095]

> The key point of the incompleteness theorem is that it shows that (at least in first order logic, which is the logic in which the theorem holds) no set of axioms can ever pin down a single model.

No, this was known before the incompleteness theorem, ref Löwenheim–Skolem theorem.

[pdonis]

The Lowenheim Skolem theorem only applies to first-order axiom systems that have an infinite model. So it would apply to the axioms for the natural numbers, yes.

The Godel theorems apply to any first-order axiom system, regardless of whether it has an infinite model or not.

[Epa095]

I don't understand what you mean by this. Gödels two incompleteness theorems are about theories of natural numbers, so their models are infinite. I don't understand what you could mean by them applying to finite models.

I stand by my claim. The key point of Gödels incompleteness is NOT that no single theory can pin down a single model, that was known before.

[Paracompact]

He's right, the Godel theorems have nothing to do with existence of models satisfying this-or-that. Such would be "semantic" truths. The reason Hilbert's program survived Löwenheim–Skolem is that Hilbert was a formalist concerned with "syntactic" truth, that is, whether there are statements P such that neither P nor not-P could be proven by the axiom system.

You might think LS would trivially demonstrate as much---"Just take P = our underlying model is countable!"---but this is not formalizable within the system itself.