Comment by kazinator
3 days ago
Gödel's Incompleteness means that formal systems that are sufficiently expressive can be used to write down new kinds of statements that can neither be derived nor contradicted from their existing axioms. Those statements can be adapted as new axioms.
Unfortunately, Gödel's proof method per se only shows an example that is not so meaningful, involving self-reference. He builds a number-theoretical formal system which can talk about its own formulas, by encoding them as integers (something we do with computers now as a daily matter: all computer program text and other data is arithmetically encoded into binary, which has an interpretation as a number). In the context of Gödel's work, we call this arithmetic encoding "Gödel numbering".
Whether a proposition is true is reformulated as a number-theoretical property: instead of asking, is this proposition or equation true, we ask, is the arithmetic encoding of this proposition an integer which belongs to the set of theorem-integers; is it a theorem-number?
Within this framework, Gödel shows that a proposition can be made which says "G is not a theorem-number", such that this very propostion's own Gödel number is G! In other words, a kind of Quining is going on, whereby the proposition embeds a coded reference to itself. Essentially, Gödel introduces the idea that we can make a statement which says "I am unprovable", in formal, rigorous way. If that statement can be derived from the axioms, then a contradiction results: it was derived, yet it asserts the falsehood that it is not derivable, and so a falsehood was derived from the system's axioms. If it is true, then it points to incompleteness: there is a truth that can be expressed in the syntax of the system, yet cannot be derived.
Thus if we have any system expressive enough to encode the "G is unprovable" statement where that statement itself is G, that system is either inconsistent (allows a falsehood to be derived) or incomplete (allows true statements to be written which cannot be derived).
> formal systems that are sufficiently expressive
One of the more interesting bits about this is understanding what "sufficiently expressive" means. The Naturals are incomplete, the Reals aren't.