What are we to make of this passage?
Among the triumphs of set theory are Gödel’s Incompleteness Theorems and Paul Cohen’s proof of the independence of the Continuum Hypothesis. Gödel’s theorems in particular had a dramatic effect on philosophical perceptions of mathematics, though now that it is understood that not every mathematical statement has a proof or disproof most mathematicians carry on much as before, since most statements they encounter do tend to be decidable. However, set theorists are a different breed. Since Gödel and Cohen, many further statements have been show to be undecidable, and many new axioms have been proposed that would make them decidable.
Well, we might complain that this is at least three ways misleading:
- Gödel’s Incompleteness Theorems are a triumph, but not a triumph of set theory.
- Gödel’s Incompleteness Theorems do not show that “not every mathematical statement has a proof or disproof”.
- Cohen’s and Gödel’s results are significantly different in type and shouldn’t be so swiftly bracketed together. While the Cohen proof leaves it open that we might yet find some new axiom for set theory which settles the Continuum Hypothesis (and other interesting propositions which can similarly be shown to be independent of ZFC), Gödel’s First Theorem — perhaps better called an Incompletability Theorem — tells us that adding new axioms won’t ever give as a negation-complete theory (unless we give up on recursive axiomatizability of our theory).
I’m slightly embarrassed to report, then, that the rather dodgy passage above is by a local Cambridge hero, Timothy Gowers, writing in the Princeton Companion (p. 6). Oops. I rather suspect he didn’t run this bit past his local friendly logicians …
Two quick points in response to Tim Gowers. First, the reason for fussing just a bit about saying that Gödel’s incompleteness theorems are “a triumph of set theory” is that this — no doubt unintentionally — makes it sound as if Gödel’s result needs some seriously infinitistic set-theoretic reasoning to prove it. Not so: as I noted before, the reasoning for the first theorem can itself be coded up in arithmetic — indeed, a very weak arithmetic: this is indeed what gives us the second theorem. (And it matters that the reasoning is relatively elementary, when we recall that in the historical context Gödel’s argument was supposed to convince those who are suspicious of infinitary set theory.)
Second, I think it is a bit unhappy to use “Not every statement has a proof or disproof” when what is meant is something like “When we are working on a problem and trying to prove a statement in a standard system such as ZFC, we cannot be certain that a proof or disproof actually exists in that system.” For it is the wobbling between “unprovable in ZFC” (or the like) and “unprovable, tout court” that underpins some of the wilder claims about the supposed deep implications of Gödel’s results (see a hundred and one threads over the history of discussions on sci.logic!). A working mathematician might well read Tim’s passage in just the intended way: I fear that others might read in more than intended!
Dear Peter,
Just spotted this complaint. Let me try to defend myself (also partially). Saying “set theory” was slightly sloppy I admit — I sort of bunch them together because when I was an undergraduate there was a Part II course called “Set Theory and Logic”. But I don’t think it’s harmfully misleading because this is a very brief passage and Godel’s theorem is discussed much more fully and accurately later in the book.
The point I was making when I said “Not every statement has a proof or disproof” was meant to mean something like “When we are working on a problem and trying to prove a statement in a standard system such as ZFC, we cannot be certain that a proof or disproof actually exists in that system.” I was concentrating on the practical consequences for mathematicians and arguing that they are not as great as the extraordinary philosophical consequences. I was trying to be brief and was not intending this to be a careful statement of Godel’s theorem. And the bracketing of Godel and Cohen is not to suggest that their results were of the same type: Godel showed that undecidability is endemic, and Cohen gave a method for proving that particular statements are undecidable. I see now that the sentence beginning “Since Godel and Cohen” could be taken to suggest that Godel’s proof was more of the Cohen type, but what I actually meant was more like, “The story didn’t stop with Godel and Cohen: many further statements …” I did in fact run this passage past someone who knows very precisely what all these statements say (as do I, to the extent that I understand what you don’t like about them), and he did not object, so I think it is possible to read them in the spirit that they were intended to be read.
Best wishes, Tim
I again agree very much with Aatu’s very helpful explanatory comments.
Tim: the “Pavilion C” explanation is indeed charitable :-)
The point of difference between the Gödel/Rosser proof and the Cohen proof which you remark on is indeed crucial. And it is perhaps also worth stressing the entirely elementary nature of the first incompleteness theorem. It can be formalized in a very weak system of arithmetic. And it was important to Gödel (and he thought philosophically significant) that this is so.
Mike asked
This seems consistent with it being true that, for any system T, there is some G_T or other that is not proveable in T. Does at least that much follow from incompleteness?
Yes, that is pretty much the statement of the first incompleteness theorem. A special argument is needed for concluding from this that there are arithmetical truths unprovable in the ordinary sense, that is, for which no compelling mathematical argument can ever be given.
The main point here is that the incompleteness theorems alone tell us nothing about what principles we accept as correct, come to accept as correct, or could “in principle accept as correct”, whatever, if anything, that last locution means. And we find a mathematical argument compelling only if we accept the principles used in it (and find the logical reasoning cogent and impeccable — for that there is a mathematical explication, thanks to the completeness theorem and a few observations due to Kreisel).
So we can only conclude, on basis of the incompleteness theorems, that if the totality of mathematical principles we accept as correct or come or could come to accept as correct, in whatever idealised sense, is recursive (or, as is more plausible, finite), there are arithmetical truths for which no mathematically compelling argument exists, that is, which are unprovable in the ordinary sense of the word — the sense we use in saying things like “Wiles proved Fermat’s last theorem”, “It’s possible no one can ever prove Goldbach’s conjecture”, “I couldn’t make anything of Shelah’s last proof but I’m sure it’s correct” etc.
The incompleteness theorems do directly tell us something about our ability to capture everything we accept as correct in the form of a formal theory. For if we accept T as a formalisation of principles we accept as correct, we must certainly accept that T is consistent. This piece of mathematical knowledge is necessarily unprovable in T, by the second incompleteness theorem (as is G_T by the first). Note a subtlety here: there might well be, for all the observation tells us, a formal theory that captures exactly the principles acceptable to us — but this theory itself can’t be recognisable as correct on basis of those principles.
This observation, originally due to Gödel himself, has led to many philosophically and mathematically fruitful and interesting developments in proof-theory and philosophy of mathematics. There is no better source for information about this issue than Torkel Franzén’s Inexhaustibility — a Non-Exhaustive Treatment.
In (partial) defence of Tim Gowers:
i. concession: yes, the passage quoted does blur the important distinction between Cohen-style independence-from-the-ZF-axioms and Goedel /Rosser-style incompletability.
But:
ii. any particular Goedel-Rosser undecidable statement /can/ be made decidable by adding new axioms; just as CH /can/ be made decidable in the same way. (The difference being that the Goedel-Rosser sentence for PA is obviously true — & therefore a good axiom! — whereas none of the candidates proposed to settle CH are at all obvious.)
And:
iii. (perhaps overly charitable): "set theory" is perhaps being used here to mean "foundations of mathematics", and so to include mathematical logic etc. (For Cambridge readers: "stuff that happens in pavilion C".)
well, i guess (given that T satsfies certain conditions), and probably this is why Peter speaks of incompletABILITY: whatever axiomatic system of arithmetic you come up with (if you want to have your set of axioms to be decidable), there is a recipe for constructing a sentence that’s not decided (in the proof-theoretic sense) by this theory.
Sure, just take as axioms all true statements in the language of arithmetic. This theory is not axiomatisable, however (it is not even definable in the language of arithmetic).
Aatu/Peter,
Set aside the this case (where every sentence is taken as an axiom). Peter says this,
But to establish that T cannot prove or disprove G_T does not show G_T is not provable at all. Indeed, we can standardly prove G_T in a stronger system than T.
This seems consistent with it being true that, for any system T, there is some G_T or other that is not proveable in T. Does at least that much follow from incompleteness?
Thanks to Aatu for his characteristic incisive clarity and good sense!
Mike wrote
Peter, but in that stronger system T+ in which GT is proveable, there is some other sentence GT* that is not proveable in T+, yes? But then, I guess there’s some system T* which just makes all of these otherwise unprovable sentences axioms.
Sure, just take as axioms all true statements in the language of arithmetic. This theory is not axiomatisable, however (it is not even definable in the language of arithmetic).
What is at issue is whether we can conclude, merely on basis of the incompleteness theorem, that there is some arithmetical truth for which there exists no compelling mathematical argument, that is, a piece of mathematical reasoning establishing A from principles we accept or come to accept as correct. For all the incompleteness theorems tell us, it is in some purely theoretical sense possible that for any arithmetical truth A there is some principle P we come to accept or could accept as correct in the future, such that, using P — and other principles we’ve come to accept at that point, or could be made to accept at that point — A is provable. (On this picture, the set of principles we accept at some point might well be recursive, of, more plausibly, finite.)
Of course, there is absolutely no reason to suppose this is the case, in however idealised sense we understand “principle we come to accept or could accept as correct in the future” — it is just that there is nothing in the incompleteness theorems themselves that rules the possibility out.
Another common and confused statement that is held to follow from the incompleteness theorems is
Mathematics can never be mathematically proven consistent.
This statement is of course true, but not because of the incompleteness theorems. It is true in the same sense we can’t hope for a mathematical proof of the claim that bananas are tasty; “mathematics” has no mathematical definition and thus there can be no question of mathematically proving anything about it.
But to establish that T cannot prove or disprove G_T does not show G_T is not provable at all. Indeed, we can standardly prove G_T in a stronger system than T.
Peter, but in that stronger system T+ in which GT is proveable, there is some other sentence GT* that is not proveable in T+, yes? But then, I guess there’s some system T* which just makes all of these otherwise unprovable sentences axioms.
There are weak arithmetics which are negation complete. For example, the quantifier-free arithmetic called “Baby Arithmetic” in my Gödel book.
“that includes enough arithmetic”
Why attach this? If it has less arithmetic than PA, then it can prove even less, so there will be even more unprovable sentences. You need this remark, of course, for the second GIT.
Yes, Wikipedia is more or less ok here: Gödel’s first incompleteness theorem shows that, for any formal system T that includes enough arithmetic (and is omega-consistent) is incomplete. That is to say, there is a sentence G_T which T cannot decide. That is to say, T can neither prove G_T nor its negation.
But to establish that T cannot prove or disprove G_T does not show G_T is not provable at all. Indeed, we can standardly prove G_T in a stronger system than T.
So to establish, for a given T, that there is a sentence G_T that T can neither prove nor disprove is not to show that there are mathematical statements which have no proof or disproof at all.
I think the idea is that there will be statements which are without proof (or disproof) in certain axiomatic systems not without proof (or disproof) simpliciter…
Gödel’s Incompleteness Theorems do not show that “not every mathematical statement has a proof or disproof”.
Are you sure? From Wikipedia (yes, I know, the reliability is suspect):
Gödel’s first incompleteness theorem shows that any formal system that includes enough of the theory of the natural numbers is incomplete: it contains statements that are neither provably true nor provably false