To see how substitution works, consider the formula (∃*x*)(*x* = *sy*). (It reads, “There exists some variable x that is the successor of *y*,” or, in short, “*y* has a successor.”) Like all formulas, it has a Gödel number—some large integer we’ll just call *m*.

Now let’s introduce *m* into the formula in place of the symbol *y*. This forms a new formula, (∃*x*)(*x* = *sm*), meaning, “*m* has a successor.” What shall we call this formula’s Gödel number? There are three pieces of information to convey: We started with the formula that has Gödel number *m*. In it, we substituted *m* for the symbol *y*. And according to the mapping scheme introduced earlier, the symbol *y* has the Gödel number 17. So let’s designate the new formula’s Gödel number sub(*m*, *m*, 17).

Substitution forms the crux of Gödel’s proof.

He considered a metamathematical statement along the lines of “The formula with Gödel number sub(*y*, *y*, 17) cannot be proved.” Recalling the notation we just learned, the formula with Gödel number sub(*y*, *y*, 17) is the one obtained by taking the formula with Gödel number *y* (some unknown variable) and substituting this variable *y* anywhere there’s a symbol whose Gödel number is 17 (that is, anywhere there’s a *y*).

Things are getting trippy, but nevertheless, our metamathematical statement—“The formula with Gödel number sub(*y*, *y*, 17)) cannot be proved”—is sure to translate into a formula with a unique Gödel number. Let’s call it *n*.

Now, one last round of substitution: Gödel creates a new formula by substituting the number *n* anywhere there’s a *y* in the previous formula. His new formula reads, “The formula with Gödel number sub(*n*, *n*, 17) cannot be proved.” Let’s call this new formula G.

Naturally, G has a Gödel number. What’s its value? Lo and behold, it must be sub(*n*, *n*, 17). By definition, sub(*n*, *n*, 17) is the Gödel number of the formula that results from taking the formula with Gödel number *n* and substituting *n* anywhere there’s a symbol with Gödel number 17. And G is exactly this formula! Because of the uniqueness of prime factorization, we now see that the formula G is talking about is none other than G itself.

G asserts of itself that it can’t be proved.

But can G be proved? If so, this would mean there’s some sequence of formulas that proves the formula with Gödel number sub(*n*, *n*, 17). But that’s the opposite of G, which says no such proof exists. Opposite statements, G and ~G, can’t both be true in a consistent axiomatic system. So the truth of G must be undecidable.

However, although G is undecidable, it’s clearly true. G says, “The formula with Gödel number sub(*n*, *n*, 17) cannot be proved,” and that’s exactly what we’ve found to be the case! Since G is true yet undecidable within the axiomatic system used to construct it, that system is incomplete.

You might think you could just posit some extra axiom, use it to prove G, and resolve the paradox. But you can’t. Gödel showed that the augmented axiomatic system will allow the construction of a new, true formula Gʹ (according to a similar blueprint as before) that can’t be proved within the new, augmented system. In striving for a complete mathematical system, you can never catch your own tail.

No Proof of Consistency

We’ve learned that if a set of axioms is consistent, then it is incomplete. That’s Gödel’s first incompleteness theorem. The second—that no set of axioms can prove its own consistency—easily follows.

social experiment by Livio Acerbo #greengroundit #wired https://www.wired.com/story/how-godels-proof-works