> The problem is that the unprovable statements will include statements that are true, but that the system can't prove.
No, that is a misrepresentation of Goedel's results. A theorem that is undecidable (neither provable nor refutable) from a set of axioms cannot be 'true' in the logical sense (because there are models of that set of axioms in which the theorem is true, and other models in which the theorem is false) - see Goedel's completeness theorem, which says that every truth is provable (and vice versa).
Goedel's incompleteness theorems can be understood on the semantic level as the mathematical structure of natural numbers cannot be characterized by a sane set of axioms, so any such attempt (e.g. peano axioms) that describes natural numbers also describes a different mathematical structure (a nonstandard model of arithmetic) and there exists a theorem that is true in one and false in the other model (so that theorem is undecidable).
An undecidable proposition is true in the logical sense if we declare it true and adopt it as an axiom.
It might seem that it's not true in that logical way which insists that truth is derived from existing axiom. But that concept depends on unproven axioms in the first place, and derivation can be a zero-step process.
That is to say the axiom we have added is now derived from an existing axiom (itself) by an empty sequence of logical steps.
How do you find that undecidable proposition? You derive it from axioms. You can't declare it axiomatic if you can't find it because it's undecidable.
The big idea that the Incompleteness Theorem torpedoed was that it's possible to enumerate all and only those theorems that are true/provable for a given set of axioms. To get all of them, you must allow unprovable theorems; to eliminate the unprovable ones, you'll necessarily also eliminate some provable theorems. It's Heisenberg's Uncertainty Principle for logic, and it was exactly that destructive to logical determinism/positivism.
> A theorem that is undecidable (neither provable nor refutable) from a set of axioms cannot be 'true' in the logical sense (because there are models of that set of axioms in which the theorem is true, and other models in which the theorem is false)
Yes, fair point. A more careful way to make the point I was trying to make is that you might care about the models in which the undecidable statement is true.
E.g. we certainly care about geometries in which a pair of lines that cross another line at the same angle are truly parallel, such that they do not meet.
We care about this even though it's not provable from four other postulates of geometry.
This is hairsplitting. It's okay to say that there are true yet unprovable sentences without always carrying "true under the standard interpretation" around. It's understood from context.
IMHO in context of logic, the usual meaning of 'true' is 'true in theory' i.e. 'true in all models of theory'. Using it for 'true in standard model' is kind of sleight of hand to make more bombastic statement that it really is.
> The idea is sometimes expressed that instead of speaking of arithmetical statements as true or false, we should say that they are "true in the standard model" or "false in the standard model". The following comment illustrates:
>> This is the source of popular observations of the sort: if Goldbach's conjecture is undecidable in PA, then it is true. This is actually accurate, if we are careful to add "in the standard model" at the end of the sentence.
> The idea in such comments seems to be that if we say that an arithmetical statement A is "true" instead of carefully saying "true in the standard model", we are saying that A is true in every model of PA. This idea can only arise as a result of an over-exposure to logic. In any ordinary mathematical context, to say that Goldbach's conjecture is true is the same as saying that every even number greater than 2 is the sum of two primes. PA and models of PA are of concern only in very special contexts, and most mathematicians have no need to know anything at all about these things. It may of course have a point to say "true in the standard model" for emphasis in contexts where one is in fact talking about different models of PA.
No, that is a misrepresentation of Goedel's results. A theorem that is undecidable (neither provable nor refutable) from a set of axioms cannot be 'true' in the logical sense (because there are models of that set of axioms in which the theorem is true, and other models in which the theorem is false) - see Goedel's completeness theorem, which says that every truth is provable (and vice versa).
Goedel's incompleteness theorems can be understood on the semantic level as the mathematical structure of natural numbers cannot be characterized by a sane set of axioms, so any such attempt (e.g. peano axioms) that describes natural numbers also describes a different mathematical structure (a nonstandard model of arithmetic) and there exists a theorem that is true in one and false in the other model (so that theorem is undecidable).