Comment by pdonis
3 days ago
> I always thought that the incompleteness theorems says, there are theorems that are true or false in all models but cannot be proved to be so.
As the GP points out, that's not what Godel's incompleteness theorem actually shows. Although it's a common misconception (one which unfortunately is propagated by many sources that should know better).
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. For example, no set of first-order axioms can ever pin down "the standard natural numbers" as the only model satisfying the axioms. There will always be other models that also satisfy them. So if you want to pin down a single model, you always have to go beyond just a set of first-order axioms.
Using the natural numbers as an example, consider a model that consists of two "chains" of numbers:
(0, 1, 2, 3, ....)
(..., -3a, -2a, -1a, 0a, 1a, 2a, 3a, ...)
The first chain is, of course, the standard natural numbers, but the second chain also satisfies the standard first-order axioms that we normally take to define natural numbers. So this model, as a whole, satisfies those axioms. And there is no way, within first-order logic, to say "I only want my model to include the first chain". That's what Godel's incompleteness theorem (or more precisely, his first incompleteness theorem combined with his completeness theorem) tells us.
I think you’re right that "true in all models but unprovable" is not accurate. By Godel’s completeness theorem if a FO sentence is true in every model of the axioms then it is provable from those axioms.
But I don’t think incompleteness is best described as saying "no first-order axioms can pin down a single model" That’s more about non-categoricity/compactness/Lowenheim–Skolem.
> I don’t think incompleteness is best described as saying "no first-order axioms can pin down a single model"
Well, it's an obvious implication of the two theorems (completeness and incompleteness) combined: if a FO sentence is not provable from a system of FO axioms, it can't be true in all models of those axioms. And if an FO sentence is not provable, its negation can't be either (since proving its negation true would prove the sentence itself false). So the negation also can't be true in all models. That means there must be at least one model in which the FO sentence is false, and at least one in which its negation is false (so the sentence itself is true). Which means there must be at least two models of that set of FO axioms--i.e., the axioms can't pin down a single model. And the incompleteness theorem proves that there is such a sentence in every system of FO axioms.
I agree that the Lowenheim-Skolem theorem has similar consequences, since it says there must be models with different infinite cardinalities.
> That’s more about non-categoricity/compactness/Lowenheim–Skolem.
As I understand it, the proof of the Lowenheim-Skolem theorem requires the axiom of choice, but the proof of the two Godel theorems does not. That would make a difference for people who are doubtful about the axiom of choice.
> 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.
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.
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.
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.