Incompleteness in reverse

Take a consistent formal system $$F$$ within which a certain amount of elementary arithmetic can be carried out.

Now out of the statements in $$F$$ there are those that can be proven true or false, and there are necessarily, due to the first incompleteness theorem, those that can’t be proven true or false within $$F$$.

Let’s take an arbitrary such statement $$a$$.

What we can do from there on is the following: we can find an undecideable statement $$g$$ in $$F$$ by following Gödel’s constructive argument, and add it to the system $$F$$ as a new axiom arriving at a more powerful system $$G$$. Then find the statement $$h$$ in $$G$$ and so on.

Of course each of the systems we construct will be incomplete.

However, here comes my question. Is it always the case that $$a$$ (an arbitrary statement that we fixed in $$F$$) can be proven true after adding a finite amount of new axioms?

• Add $a$ as an axiom, now you can prove $a.$
– user147556
Jul 6, 2021 at 14:57
• @MichaelBarz oh sure, but what if we aren’t certain in the validity of $a$? We can add $g$ because it is known to be true (otherwise $F$ is inconsistent). In my question, I assume that we always add the Gödel’s statement until we can reach a system powerful enough to prove an unrelated statement $a$. My question is — if $a$ is true after all, will we always reach a proof of it, and whether this is even known Jul 6, 2021 at 14:59
• By Godel's completeness theorem, an undecidable statement $a$ exists precisely because it is true in some models and false in other models. It is somewhat meaningless to ask about the validity of $a$--it depends on the model. Both $a$ and "not $a$" are consistent additions to your theory.
– user147556
Jul 6, 2021 at 15:01
• Perhaps what you're asking is this: Start with $F$, add its Godel sentence, then add the Godel sentence of that theory, and so on. After infinitely many steps, will you have a complete theory? The answer is no: the incompleteness theorem can be applied to the theory you get after infinitely many steps. Jul 6, 2021 at 15:04
• @Prof. Legolasov Doesn't my comment answer your question? After infinitely many steps, the theory is still incomplete, so there is some statement that is neither provable nor disprovable. Let $b$ be such a statement. Now let $a$ be either $b$ or $\neg b$, whichever is true. Then $a$ is a true statement that was not provable in $F$ and that does not become provable after any finite number of steps of adding Godel sentences. Jul 6, 2021 at 16:20

Let $$g_1$$ be the Godel sentence of $$F$$, and let $$F_1 = F + g_1$$. In other words, $$F_1$$ is the formal system that is the same as $$F$$, except that $$g_1$$ is added as an additional axiom. Now let $$g_2$$ be the Godel sentence of $$F_1$$, and let $$F_2 = F_1 + g_2$$. In general, we let $$F_{n+1} = F_n + g_{n+1}$$, where $$g_{n+1}$$ is the Godel sentence of $$F_n$$. Now let $$F_\omega$$ be the formal system in which all of the statements $$g_n$$ are added to $$F$$ as additional axioms. Then the incompleteness theorem can be applied to $$F_\omega$$ as well. Now let $$a$$ be the Godel sentence of $$F_\omega$$. Then $$a$$ is true but not provable in $$F_\omega$$, and therefore it is not provable in any $$F_n$$.
Gödel sentences are by construction $$\Pi^0_1$$ statements, that is, they have the form "for all $$n$$ ...", where ... is a recursive statement (think "a statement that a computer can decide"). For instance, the typical Gödel sentence for a system $$T$$ coming from the second incompleteness theorem says that "for all $$n$$ that code a proof in $$T$$, $$n$$ is not coding a proof of a contradiction", and a similar observation holds for the sentence from the first incompleteness theorem.
Under mild assumptions on $$T$$ (say, the assumptions on the incompleteness theorem and that $$T$$ is true in the standard model of arithmetic), you could add to it all true $$\Pi^0_1$$ statements, many of which are not provable in $$T$$ and many of which are not Gödel sentences. The result is a theory to which the incompleteness theorem no longer applies (it is not recursive), and yet it is still far from complete and there are $$\Pi^0_2$$ statements that are not provable in it (assertions that certain recursive functions are total). There are similar results if you proceed to add all true $$\Pi^0_2$$ statements to this theory and so on.
The assumption that $$T$$ is true is perhaps too strong. We can say something very general even without this requirement: the other answer indicated that if we start with $$T_0=T$$ and recursively form $$T_{n+1}$$ by adding to $$T_n$$ its Gödel sentence, then the incompleteness theorem still applies to the union of the $$T_n$$. There is a general fact here: If $$\{T_k: k\in\mathbb N\}$$ is a recursively enumerable family of theories (meaning, there is an algorithm that generates all pairs $$(\phi,n)$$ such that $$\phi$$ is a sentence and $$\phi\in T_n$$), there is a $$\Pi^0_1$$ sentence which is simultaneously undecidable in all the theories $$T_k$$.