> The First Incompleteness Theorem tells us that assuming PA is consistent, one can formulate propositions that cannot be proved (nor disproved) on the basis of PA, but which are nevertheless true.
As far as I know, that last clause was never a claim made by Godel. Specifically the claim that these propositions are nevertheless true. This follows quite simply from the assumption that either a proposition is true, or its negation is true (i.e. the law of the excluded middle).
But I recall reading that Godel, in his proofs, went to great lengths to avoid the law of the excluded middle over infinite sets.
Indeed, (again AFAIK) godel's first incompleteness theory still holds in constructive mathematics (roughly where the law of the excluded middle cannot be used). As such, I think the addition that these propositions are 'nevertheless true' actually hides a lot of complexity.
Because there are philosophical positions in which these independent propositions are neither true not false.
And really, this is why we call them independent. The truthiness of these propositions is not determined by their axiom systems. It's a rather big philosophical stance to say that the 'truth' of these propositions can be determined outside of the axiomatic systems. It seems to me like that claims there is an objective (as in, not dependent on an axiomatic system) definition of what is true.
There is an objective definition of truth in any particular model. For any particular model M of, say, Peano arithmetic, there is an objective, unambiguous, perfectly well-defined notion of truth in that model (of course, the definition of truth cannot itself be formalized within the model).
> There is an objective definition of truth in any particular model.
"in any particular model" - this is exactly parent's point.
From Wikipedia, a restatement of the 1st incompleteness theorem:
> there are statements of the language of F which can neither be proved nor disproved in F
The truth of a proposition P, within F, means "P is an axiom of F, or can be proved in F".
Saying "there are statements of the language of F which can neither be proved nor disproved in F... but the statements are true nevertheless" is appealing to some 'objective notion' of truth that transcends F.
>The truth of a proposition P, within F, means "P is an axiom of F, or can be proved in F".
No, truth and proof are NOT the same thing. The system F needn't have any notion of truth. For example, Peano arithmetic has no notion of truth. Peano arithmetic has notions of zero, successor, addition, and multiplication--none of truth.
Almost all competent mathematicians would agree that there exist theorems in the language of PA which are neither provable nor disprovable in PA but which are nevertheless true. Here, "true" means "true in the standard model of PA", not "true according to PA"---the latter isn't even meaningful because there is no such thing as "truth according to PA".
1. The original example would be Goedel's own example, namely, the statement (formulated in the language of PA) that PA is consistent, i.e., that PA does not prove 1=0.
Philosophical arguments aside, Gödel himself was absolutely, even evangelically, a mathematical realist. He believed any meaningful statement about mathematics had an objective truth value, axiomatic systems be damned.
> It's a rather big philosophical stance to say that the 'truth' of these propositions can be determined outside of the axiomatic systems.
I don’t think so. ZFC is either consistent or it isn’t. That is, a Turing machine enumerating all theorems of ZFC either produces 0=1 or it doesn’t. This is, however, independent of ZFC (if the latter is consistent) by the second incompleteness theorem. See https://mathoverflow.net/a/332266, in particular Nik Weaver’s comment:
> I think the strongest argument in favor of the definiteness of ℕ, and against the idea that PA, or any other axiomatization, is the be-all end-all, is the evident fact that we have an open-ended ability to go beyond any computable set of axioms, for instance by affirming their consistency. If you accept PA you should accept Con(PA), and the process doesn't stop there: you can then accept Con(PA + Con(PA)), and so on. This goes on to transfinite levels. If our understanding of ℕ really were fully captured by some particular set of axioms then we would not feel we had a right to strengthen those axioms in any special way; the fact that we do feel we have this right shows that our understanding is not captured by any particular set of axioms.
I'm not 100% sure this perspective works, but could one take the position that this is because of a disconnect between model and reality?
You look at some big list of symbols and say "this formula (model) corresponds to whether a Turing machine enumerating all theorems of ZFC produces 0=1 (reality)". But does it really?
In a way. Consider a Turing machine that enumerates all proofs in ZFC and halts iff it finds a proof of 0=1 (i.e. a contradiction). The statement that this Turing machine halts (like the statement that any given Turing machine halts) is what’s called a Sigma_1 statement, which lies at the bottom of the arithmetic hierarchy (right above bounded-quantifier statements). ZFC + ~Con(ZFC) is consistent but Sigma_1-unsound and therefore omega-inconsistent [1].
What Gödel does is the following: he constructs a sequence of symbols which is not decidable (i.e. there is no “proof” of it or of its negation).
Then (and this is super important) he explains that IN THE STANDARD INTERPRETATION that sequence of symbols can be translated to “the sequence of symbols corresponding to the number XXXXX is a statement which has no proof” (and has to be true) and that very sequence corresponds to that number XXXXX.
But those two things (the construction and the interpretation) are totally separated, and goes to great lengths to keep them so.
As far as I know, that last clause was never a claim made by Godel. Specifically the claim that these propositions are nevertheless true. This follows quite simply from the assumption that either a proposition is true, or its negation is true (i.e. the law of the excluded middle). But I recall reading that Godel, in his proofs, went to great lengths to avoid the law of the excluded middle over infinite sets.
Indeed, (again AFAIK) godel's first incompleteness theory still holds in constructive mathematics (roughly where the law of the excluded middle cannot be used). As such, I think the addition that these propositions are 'nevertheless true' actually hides a lot of complexity. Because there are philosophical positions in which these independent propositions are neither true not false.
And really, this is why we call them independent. The truthiness of these propositions is not determined by their axiom systems. It's a rather big philosophical stance to say that the 'truth' of these propositions can be determined outside of the axiomatic systems. It seems to me like that claims there is an objective (as in, not dependent on an axiomatic system) definition of what is true.