I consider the following version of Gödel's first incompleteness theorem:
Assume $F$ is a formalized system which contains Robinson arithmetic $ Q$. Then a sentence $G_F$ of the language of $F$ can be mechanically constructed from $ F$ such that:
- If $F$ is consistent, then $F$ $ ⊬$ $G_F$
- If $F$ is $1$-consistent, then $F$ $⊬$ $¬G_F$
In the proof we first use the Diagonalization Lemma and apply it to the negated provability predicate $¬Prov_F(x)$: this gives a sentence $G_F$ such that
(A) $F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)$.
Where $⌈G_F⌉$ is the Gödel number of $G_F$. Thus, it can be shown, even inside $F$, that $G_F$ is true if and only if it is not provable in $F$.
It is not difficult to show that $G_F$ is neither provable nor disprovable in $F$, if $F $ only is $1$-consistent by assuming $F$ is provable, ... and so on and so forth.
But when we prove $G_F$ is unprovable didn't we also prove $G_F$, since A holds? That is, we have proved $G_F$ and at the same time we have shown we cannot prove $G_F$.
This seems contradictory to me, or am I missing something? I guess the answer must have to do with Tarski's undefinability of truth.