> I believe you can make a consistent fully provable axiomatic system by excluding statements that are not provable from your system, as meaningless.
The problem is not how to exclude the unprovable statements. The problem is that the unprovable statements will include statements that are true, but that the system can't prove. Some of those statements are probably not ones you care about, like "this statement is unprovable". But you have no way of knowing that all of the unprovable true statements are like that. Some of them might be ones you do care about.
Thus, the real import of Goedel's theorem is not "you need to exclude unprovable statements"; it is "the intuitively attractive ideal of having a system in which every true statement you care about can be proved is not achievable".
"The intuitively attractive ideal of having a system in which every true statement you care about can be proved is not achievable".
Sure it is. But the system cannot contain infinities or real numbers of infinite precision. The halting problem for deterministic computers with finite memory is solveable - the system must either halt or repeat a state, and if it repeats a state, it's in an endless loop. Yes, the number of states may be very large, but not infinite.
An interesting question to ask is "do we need infinities". In a sense, infinities are a convenience feature to make formulas simpler. Without infinities, everything has edge cases, bounds problems, tolerances, and all the annoyances known to people who do serious computer number-crunching. Theory in that area has lots of case analysis.
It's perhaps unfortunate that Russell lived in the pre-computer era. Simple theorems were essential in the paper and pencil era. In the 1970s and 1980s, Boyer and Moore took on much the same problem as Principia Mathematica. They published "A Computational Logic"[1], and built the first good inductive theorem prover for constructive mathematics. (I used it back then, and a few years ago I got it running again on Common LISP and put it on Github, so you can still run it.[2]) Proofs that come out of that thing have lots of case analysis. Mathematicians used to hate proofs like that. Many still do.
At one point Boyer and Moore formalized what a floating point unit does, and this was used to verify an AMD floating point unit. This followed an embarrassing recall of Intel CPUs that were slightly off on division, and was paid for by AMD. It's a huge, ugly problem to formalize, compared to the ordinary rules for real arithmetic. It is, however, a system in which every true statement you care about can be proved.
The proof of the four-color theorem shook up the field. Thousands of cases. A simple problem with a huge proof that required machine assistance was a new thing back then. Now it's more common. Still makes many mathematicians unhappy.
> 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.
> The problem is that the unprovable statements will include statements that are true, but that the system can't prove.
"5 contains itself" might also be true in some extended system where numbers are considered to also be sets. But in system where numbers are numbers and sets are something different this statement is unprovable because it's nonsensical.
What does even "true" mean if you are allowed to tangle things like "true" and "provable" in self referential paradox and draw conclusions from it?
I think Godel result comes from lax definition of "true". Like Russel's paradox comes from lax definition of how can you define a set.
I can concede that it may depend on the precise formal system you are using, but I think you can easily imagine a logic where a predicate ∈ takes two variables (x, y) of any kind and returns "true" iff y is a set and x is in y. In a well-founded system where numbers are ur-elements ∈(5, 5) would be well-formed and equal to "false" as every other expression of the form ∈(x, x).
In this vein I would consider "5 smells insanity" nonsencial in the colloquial sense and at the same time false.
I'm not a mathematican or logician, so take this with a grain of salt, but in my understanding, you can't really say that some unprovable thing is "really really true although unprovable". It's more like, it's independent from the axioms you started with. It might be true or false, depending on what additional axioms you decide to use.
The problem is not how to exclude the unprovable statements. The problem is that the unprovable statements will include statements that are true, but that the system can't prove. Some of those statements are probably not ones you care about, like "this statement is unprovable". But you have no way of knowing that all of the unprovable true statements are like that. Some of them might be ones you do care about.
Thus, the real import of Goedel's theorem is not "you need to exclude unprovable statements"; it is "the intuitively attractive ideal of having a system in which every true statement you care about can be proved is not achievable".