[Math] A naive inquiry of Godel’s incompleteness–or why does mathematics need proofs of unprovability

incompletenesslogic

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

Best Answer

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.