Gödel's incompleteness theorem: if the statement is unprovable then how did we prove its true?

Question

The proof for Gödel's incompleteness theorem shows that for any formal system $F$ strong enough to do arithmetic, there exists a statement $P$ that is unprovable in $F$ yet $P$ is true.

Let $F$ be the system we used to prove this theorem.

Then $P$ is unprovable in $F$ yet we proved it is true in $F$.

Contradiction.

Am I saying something wrong? Is $F$ forced to be inconsistent?

Answer 1

It seems you are missing a key hypothesis in the statement of Gödel's incompleteness theorem. You wrote in a comment:

Godels theorem is proved In a certain system L and shows that for any F (strong enough to do arithematic) P is true and unprovable.

This is incorrect. Gödel's theorem is proved in a certain system $L$ and says the following. Suppose $F$ is a formal system which is strong enough to do arithmetic and consistent (that is, it does not prove a contradiction). Then a certain arithmetic statement $P$ (which is defined in terms of the system $F$) is true but is not provable in $F$.

Now you want to substitute $L$ for $F$. That's fine, but in order to apply Gödel's theorem, you need to know that the hypotheses are satisfied. That is, you need to know that $L$ is strong enough to do arithmetic and that $L$ is consistent. Verifying the first hypothesis is easy, but verifying the second hypothesis is not easy at all. Before you can carry out your argument, you need to prove (within the system $L$) that $L$ is consistent.

In fact, your argument does work (modulo some details that are technical but important) if $L$ could prove that $L$ is consistent, and would reach a contradiction. So actually, your argument shows that if $L$ can prove that $L$ is consistent, there is a contradiction in $L$ (and so $L$ is not actually consistent at all!). This is exactly the statement of Gödel's second incompleteness theorem, which says that no consistent formal system strong enough to do arithmetic can prove its own consistency.

(The technical details: to reach a contradiction, you need to not prove $P$ within $L$, but prove that $L$ proves $P$ within $L$. That is, $L$ needs know not just that $P$ is true, but that $L$ can prove $P$, since this is what contradicts the fact that $P$ is unprovable in $L$. The fact that if $L$ proves $P$ then $L$ proves that it proves $P$ is a consequence of being able to do arithmetic in $L$.

These details are important because in order to prove that $L$ proves $P$, you have to actually have an honest proof of $P$ within $L$. If you have a proof within $L$ that $L$ is consistent, then you get such an honest proof of $P$ from Gödel. But if you just assume for a contradiction that $L$ is consistent, you don't get such a proof and so you cannot conclude that $L$ proves $P$; instead you only know that $P$ is true. So you can't reach a contradiction: there is no contradiction between the two statements "$P$ is true" and "$L$ cannot prove $P$".)

Answer 2

Not the biggest expert in this, but maybe this helps until the real experts show up.

To prove a statement $\phi$ from (a first-order theory) $F$ means (by the completeness theorem) to show that it holds in all models of $F$. However, still without proving $\phi$ from $F$ we can look at some particular model of $F$ (via meta theory) and find that $\phi$ indeed holds there. So we have an external proof of $\phi$ for this specific model.

Now if $\phi$ says "$\phi$ cannot be proven from $F$", then this means that we need this meta theory on this specific model to prove $\phi$ and it cannot be done from $F$ alone.

Even another way: we showed that $\phi$ holds in some model (externally). Then $\phi$ showed that there are models where it does not hold. So not all models agree. So neither $\phi$ nor $\neg \phi$ can be provable.

Answer 3

(Disclaimer: In what follows when I say formal system I mean a first-order theory)

Be careful, you are mixing two different concepts namely "provability" and "truth".

Gödel incompleteness theorem (more correctly its generalization, Rosser's theorem) says that

If $F$ is a formal system in which you can interpret arithmetic (which roughly means that you can say what is a number, a zero, a successor, the addition and multiplication and prove the axioms of arithmetic) then it is either inconsistent, hence it proves everything, or it is incomplete (that is there are statement which aren't provable nor disprovable).

In this form of the theorem there is no reference to the concept of truth.

Actually the original Gödel's incompleteness theorem says something different:

There are statement that are not provable in Peano Arithmetic but are true in the model of the natural numbers $\mathbb N$.

A statement can be proved in a formal system $F$ but it doesn't make any sense to say that it is true in $F$, a statement is either true or false in a given interpretation.

You could define that a statement is true in a formal system $F$ if it is true in all its model, that is if it is a logical consequence of the axioms in $F$. Of course by the Gödel's completeness theorem that is equivalent to the fact that the statement is provable in $F$, so clearly this is not the correct statement of Gödel incompleteness theorem.

Hope this helps.