A naive inquiry of Godel's incompleteness--or why does mathematics need proofs of unprovability?

Question

My question stems from reading Swetz, 1994 (mostly excerpts from the journal Mathematics Teacher) and Berlinski, 2005 (a popular book on 10 most important mathematical breakthroughs in history).

1) I'm having difficulty understanding why Godel's theorem (if I understand what I have read) requires both formulas provable and unprovable. My naive concept of mathematics is a system containing only "positive" theorems and laws and I imagine the same for science. That the scientific method culls anything proven wrong, so as not to carry failures as baggage together with its laws. Where failure, mistakes, and problems are separated as historical study or challenge. Why do unprovable statements need be admitted to a proper system?

In anticipation of my enlightenment, I have a few follow-up Qs,

2) Its my understanding the Hilbert project meant to take the point of view that mathematics and formalism needed to take a meta-point of view for the purpose of separating formulas (as symbols) from the discussion (in natural language) about mathematics. If these unprovable formulas are necessary to prove other provable proofs, then why not segregate them to yet another meta-level?

3) What I gather about Godel's argument from these sources includes a point about mathematics' use of symbols (representing numbers, variables for formulas, variables for sets and sets of sets, etc.). Then is it his argument to suggest that where a proof can be admitted to the system which can be neither proved or disproved, the substitution of variables will propagate this error?

Answers need not be technical, only sufficient to sort my "Godel baggage".

Chris

PS. I found this January post very useful for its references and look forward to finding a volume for my naive appetite for the history of formalism:Understanding Gödel's Incompleteness Theorem---

Answer 1

As your quotes from Berlinski suggest, the heart of Godel's statements is arguably not in the unprovability itself, but in the fact that the system is able to 'talk about itself' - that is, that statements about provability can be cast as strictly arithmetic questions. It might help to familiarize yourself with another undecidability result which goes through roughly the same route: Matiyasevich's Theorem about the solvability of diophantine equations (i.e., the question 'does this polynomial in $x$, $y$, $z$, $w$, etc. ever evaluate to zero at some integer values of $x$, $y$, $\ldots$?'). The root of the proof lies in showing that diophantine equations are expressive enough to represent all recursively enumerable sets; what Godel does is essentially the same, showing that Peano Arithmetic (or any similar system) is expressive enough that questions about 'provability' can be cast as arithmetic questions.

As for why unprovable statements need admission, the point isn't simply that they're unprovable but that they're unprovable and true - that is, that the set of 'things we can prove' will always be a proper subset of 'things that are true'. Obviously this isn't a crippling discovery; mathematics didn't stop as of Godel! But it is arguably a profound one, and one that has substantial practical implications: for instance, as noted above there can't possibly be an algorithm for solving diophantine equations; there can't be algorithms for finding a 'minimal forbidden minor' categorization of many sets of graphs; there can't be algorithms for solving the Word Problem for groups; etc, etc.

Answer 2

When people set about formalizing Mathematics, they did it this way:

1. List the symbols you're allowed to use to make mathematical statements,

2. Give some rules to distinguish "well-formed formulas" (like $3+4=6$) from other strings of symbols (like $3\div\gt4=$),

3. List the axioms (a finite list),

4. List the "rules of inference" (the methods you are allowed to use to get from one well-formed formula to another).

The theorems are then the well-formed formulas you can get to, starting from the axioms and using the rules of inference; they are the things you can prove.

The naive hope was that for every well-formed formula $P$, there would either be a proof of $P$, or a proof of the negation of $P$ (but not both).

What Godel proved was that if your axioms and rules of inference are strong enough to do ordinary arithmetic, then the naive hope cannot be realized. Either the system is inconsistent (meaning that you can prove every statement, including the negation of statements you can prove), or it is incomplete (meaning there are well-formed formulas $P$ such that you can't prove $P$ and you can't prove the negation of $P$).

I don't understand what you mean by "admitting unprovable statements to a proper system." We don't accept them as theorems; we note that neither they nor their negations are theorems. What would you have us do with unprovable statements?

Answer 3

It is important to see the theorems in the context of Hilbert's attempt to formalize mathematics. Formalization here means reducing the whole Mathematics-making art into something as simple, in principle, as manipulating strings according to some fixed rules. In Hilbert's times there wasn't computers yet, but I'm sure he had in mind a goal that can be stated as "allowing computers to do math without thinking".

This formalization has two strengths. One is obvious - you can find theorems by letting your computer run, in an ordered way much different from current-day's guessing and searching in the dark game. The second one was no less important to Hilbert - if you can show all mathematics can be derived from extremely simple, "obviously true" rules, then our faith in the correctness of mathematics will be high. Remember, this was around the time of the "great crisis in the foundations of mathematics", raised by Russel's paradox (which requires only the extremely plausible hypothesis that you can define sets freely using mathematical predicates) and other paradoxes.

So Hilbert was looking out for a simple axiomatic system from which all mathematics could be derived. But what is "all" mathematics? It is not only what can be proven in some sort of system, but everything that is true about the objects we are interested in. One such object are the natural numbers. Now consider Goldbach's conjecture - that every even number greater than 4 can be written as the sum of two odd primes. This is surely either true or false (or is it...? But we adopt the viewpoint that believes this). The only question remaining is - can Hilbert's wonderful system prove it using no thinking at all, only manipulation of symbols? If it can't prove nor disprove it, surely it does not cover "all" mathematics.

What Godel showed is exactly that - that no matter what proof system Hilbert will give, it will have some flow: Either it won't be consistent (can prove and disprove the same thing, and from it usually follows you can prove everything), or it won't be complete (there will be some claim you won't be able to prove or disprove), or it won't be effective (in the sense you won't be able to check if a proof is legal or not - there will be no simple mechanical rules for doing it) or it won't talk about the nautral numbers (with the operations of addition and multiplication; Presburger arithmetic eludes Godel's theorems because it leaves the operation of multiplication out of the game).

What makes Godel's proof all the more interesting is that it uses the strengths of the system against it. On the other hand, the system can talk about natural numbers, and we can encode very intricate claims using natural numbers; on the other hand, the systems' rules are very simple, so they can be encoded themselves with natural numbers; and hence the system can indirectly prove things about itself, and this leads to some sort of "explosion". This is a very powerful idea, which has also given birth to the theory of Computability.