Aftermath of the incompletness theorem proof

Question

This is somewhat of a minor point about the incompletness theorem, but I'm always a little unsure:

So one proves that there is a formula which is unprovable in the theory of consideration. Okay, at this point one is done.

Then, as that unproven sentence contains the claim that this (the unprovable-ness) would happen, one is in some sense justified to say "So the statement really is true, but still, it's unprovable within the theory". Now here is my problem: I'm very unsure in which sense this notion of truth which somewhat comes from outside the theory is sensible. There is a note on that point on the wikipedia page but I don't really comprehend it.

The word "true" is used disquotationally here: the Gödel sentence is true in this sense because it "asserts its own unprovability and it is indeed unprovable" (Smoryński 1977 p. 825; also see Franzén 2005 pp. 28–33). It is also possible to read "GT is true" in the formal sense that primitive recursive arithmetic proves the implication Con(T)→GT, where Con(T) is a canonical sentence asserting the consistency of T (Smoryński 1977 p. 840, Kikuchi and Tanaka 1994 p. 403)

So I can see that if one is technically aware that one is now talking in a meta language, that one has introduced a new "true". But then again (a) if one reflects on the fact that one draws such technicals conclusions outside of the initial freamework, then it seems to me one should really introduce another meta-meta-language. And (b) isn't it really just a little ambiguous to say "Gödels incompleteness theorems says that there are true statements, which can't be proven within a certain strong theory"?

I'd be thankful if someone could elaborate on that.

Answer 1

There might be a bit of a chicken-and-egg happening here. For the common proofs of Gödel's Incompleteness Theorem, we put special priority on the structure $( \mathbb{N} , 0, S, + , \cdot , \mathrm{exp} )$ of elementary arithmetic. If something is true in this structure, then we often refer to that statement as true.

Peano Arithmetic is one attempt to axiomatize all truths of this structure. In more modern terms, it was perhaps hoped that the statement $$\mathbb{N} \models \phi \;\Leftrightarrow\; \text{PA} \vdash \phi$$ would have been true (or true). Gödel's Theorem tells us that this is impossible, and, more, that any attempt to "nicely" axiomatize truth in $\mathbb{N}$ is doomed to fail, by being either inconsistent, or incomplete.

As the structure $\mathbb{N}$ "exists" outside of the formal system PA (and "existed" well before this system was devised), we can argue about truth within the structure $\mathbb{N}$ using methods outside the formal system PA. In fact, there are several truths about $\mathbb{N}$ that we know cannot be proved within PA (e.g., Goodstein's Theorem and a certain strengthening of the finite Ramsey's Theorem). As long as there is no real controversy about these extra-PA methods used, the truth of these results is similarly uncontroversial. It is by using such methods outside of PA that we argue that if PA is consistent, then $G_{\text{PA}}$ is true (in $\mathbb{N}$).

While perhaps a bit ambiguous, this consequence of Gödel's Theorem could be restated (somewhat awkwardly) as "Given any "nice" consistent axiom system capable of expressing elementary arithmetic, there are number-theoretic statements which are true in $\mathbb{N}$ that cannot be proved within that system."

Answer 2

The incompleteness theorem, in its usual form, talks about the natural numbers $\mathbb N$ together with some relations such as $\leq$, constants such as $0$ and $1$ and operations $+$ and $\cdot$. To simplify matters, we are ready to add another operation, exponentiation $n^m$. There is an inductive definition of when a sentence $\varphi$ in the appropriate language is true in $\mathbb N$. This inductive definition over the complexity of $\varphi$ is just what you would expect:

For example, if $\varphi(x_1,\dots,x_n)$ is a formula and we already know, given natural numbers $m_1,\dots,m_n$, whether $\varphi(m_1,\dots,m_n)$ holds in $\mathbb N$, then $\exists x_1\varphi(x_1,\dots,x_n)$ holds for $m_2,\dots,m_n$ in place of $x_2,\dots,x_n$ if there is some $m\in\mathbb N$ such that $\varphi(m,m_2,\dots,m_n)$.

A simpler example, the formula $x\leq y$ holds for $m$ and $n$ in place of $x$ and $y$ if we actually have $m\leq n$ in $\mathbb N$.

Now we use Gödel's technique to construct a sentence $\varphi$ that intuitively says "I am not provable". This is actually highly non-trivial, but we just assume it can be done. If $\varphi$ were provable, we could prove a statement that is wrong in $\mathbb N$. (Because if $\varphi$ were true, we could not prove it.) But we assume that from our axioms we can only prove true statements in $\mathbb N$. So $\varphi$ is actually unprovable and thus true in $\mathbb N$ in the sense discussed above.

The really technical part of this argument is to show that we can talk about provability in the language of $\mathbb N$. For me the most impressive part of Gödel's argument is that there is a sentence that basically says "I am not provable". This is the so-called fixed point lemma.

Answer 3

This is an extension of a comment below Arthur Fischer's answer. For concreteness we will work with the theory PA but in principle any sufficiently strong theory would act the same.

Working in PA, or even in the weaker theory PRA, we can formally prove the implication $$ \text{Con}(PA) \to G_{PA} $$ where $G_{PA}$ is the Gödel sentence of PA. This leads to two conclusions:

1. Because we know from the first incompleteness theorem that $G_{PA}$ is not provable in PA, and because $\text{Con}(PA) \to G_{PA}$ is provable in PA, $\text{Con}(PA)$ must not be provable in PA. This is the standard way to prove the second incompleteness theorem.

2. If we were working in a setting where we had already assumed $\text{Con}(PA)$, and we have access to the normal resources of PRA, then we can prove $G_{PA}$. In particular, when we are proving the incompleteness theorems we are working in normal mathematics, which includes much more than just PRA, and we assume $\text{Con}(PA)$ when we are proving that theorem. Under that assumption we can prove $G_{PA}$ in normal mathematics. Thus the Gödel sentence is "true" in exactly the same sense that $\text{Con}(PA)$ is true when we assume it as a hypothesis to prove the incompleteness theorem.

The key point in the second bullet is that we don't prove $G_{PA}$ starting with nothing. We prove $G_{PA}$ starting with the knowledge or assumption that $\text{Con}(PA)$ holds. If we did not assume the truth of $\text{Con}(PA)$, or have a separate proof of $\text{Con}(PA)$, the argument in that bullet would be useless. But once we do assume $\text{Con}(PA)$ is true, it only takes a very weak theory (PRA) to deduce that $G_{PA}$ is also true under that assumption.