# Let's keep adding once undecidable statements

This present thread is inpired by the previous thread the true reason of the incompleteness of formal systems.

I have the following intuitive idea: Gödel's second incompleteness theorem states that a "reasonably strong formal system" cannot prove its own consistency (provided it is consistent after all). Thus, for example, "ZFC is consistent" is not provable in ZFC. (I assume that ZFC is consistent, since the class of all well-founded sets is a model of ZFC.) Therefore, we can strengthen ZFC by adding the new axiom "ZFC is consistent": $$\mathrm{ZFC}_2\qquad:=\qquad \mathrm{ZFC}\quad +\quad \text{"ZFC is consistent"}$$ Now, note that we can apply Gödel's second incompleteness theorem again: "$\mathrm{ZFC}_2$ is consistent" is not provable in $\mathrm{ZFC}_2$. For that reason, we can add to $\mathrm{ZFC}_2$ the new axiom "$\mathrm{ZFC}_2$ is consistent": $$\mathrm{ZFC}_3\qquad:=\qquad \mathrm{ZFC}_2\quad +\quad \text{"\mathrm{ZFC}_2 is consistent"}$$ We can go on and define $\mathrm{ZFC}_4$ to be $\mathrm{ZFC}_3$ + "$\mathrm{ZFC}_3$ is consistent". Going further, we can define $\mathrm{ZFC}_5, \mathrm{ZFC}_6, \mathrm{ZFC}_7, \dots$ and so on in a similar way. Now, we can define $\mathrm{ZFC}_\omega$ to be the union of $\mathrm{ZFC}, \mathrm{ZFC}_2, \mathrm{ZFC}_3, \mathrm{ZFC}_4 \dots$, $$\mathrm{ZFC}_\omega:=\bigcup_{n}\mathrm{ZFC}_n.$$ Then, we can define $\mathrm{ZFC}_{\omega+1}$ to be $\mathrm{ZFC}_\omega+ \text{"$\mathrm{ZFC_\omega}$is consistent"}$. And so on. We can iterate this never-ending process forever.

Question time. I can image the theory $\eta:=\bigcup\{\mathrm{ZFC}_\alpha\mid\alpha\in \mathrm{Ord}\}$. Is this even a well-defined object or just fiction? Is $\eta$ decidable? Is $\eta$ complete?

• There are a lot of subtleties in defining $ZFC_{\alpha}$, see mathoverflow.net/questions/67214 for a good discussion. – David E Speyer Jun 13 '16 at 18:15
• No matter how you resolve the aforementioned subtleties, the resulting $\eta$ must be undecidable (being a consistent extension of Robinson's arithmetic) and incomplete (as it is included in the theory ZFC + all true $\Pi^0_1$ sentences). – Emil Jeřábek Jun 13 '16 at 18:33
• Why on earth was this voted down? It's a very natural question. – Noah Schweber Jun 14 '16 at 5:58

Short answer: $ZFC_\alpha$ only makes sense for those $\alpha$ which have "nicely definable representations" - specifically, for the computable ordinals $\alpha$. (An ordinal is computable if there is a binary relation on $\omega$ which is computable, and which well-orders $\omega$ with order-type $\alpha$.) Every computable ordinal is countable, as is the least noncomputable ordinal $\omega_1^{CK}$ - so this process stops long before reaching $\omega_1$, let alone going through all of $ON$.

The details of this process are quite subtle - Sacks' book "Higher Recursion Theory" has a very good treatment in the first chapter. Especially relevant is the representation of computable ordinals via ordinal notations, and Kleene's $\mathcal{O}$. Basically, Kleene's $\mathcal{O}$ is (in a precise sense) the set of all names for computable ordinals. There's a lot of incomputability here: $\mathcal{O}$ is incomputable (in fact $\Pi^1_1$ complete!), as are the relations "codes the same ordinal as," "codes a bigger ordinal than," etc. Moreover, the natural structure of $\mathcal{O}$ is as a partial order, not a linear order, reflecting these undecidabilities. The object $ZFC_{\omega_1^{CK}}$ should, intuitively, be the result of iterating the consistency process along a "maximal" path through $\mathcal{O}$; however, there are many different maximal paths, including "short" ones (i.e. ones of order-type $\omega^2$ instead of $\omega_1^{CK}$). The study of paths through $\mathcal{O}$ is an extremely rich area of computability theory and descriptive set theory.

Tl;dr: it's a very good idea, but it's a bit more complicated than that.

• Regarding the incomputability of the order relation, I believe that the underlying partial order relation of $\mathcal{O}$ the restriction of a computable relation to the elements of $\mathcal{O}$. And furthermore, for every element $b\in\mathcal{O}$, the order relation on the cone below $b$ is a computable order. Basically, if $b\in\mathcal{O}$, then you can be sure that the programs involved in the $\mathcal{O}$ relation will all halt, and so you can simply unravel the entire order below $b$. – Joel David Hamkins Jun 13 '16 at 19:36
• Note that different notations for $\omega+1$ might disagree on what "$ZFC_{\omega+1}$" means. Choosing paths works but, as you suggest, only to a limited extent. For what it's worth: working inside a model of set theory, it makes perfect sense to consider $ZFC_\alpha$ (with the obvious straight-line definition) for any ordinal $\alpha$. Of course, this stops being recusively axiomatizable pretty quickly (in the internal sense) and then $Con(ZFC_\alpha)$ loses its arithmetic meaning. – François G. Dorais Jun 13 '16 at 19:37
• @FrançoisG.Dorais Indeed - and if I recall correctly, every true $\Pi^0_1$ is true in some version of $ZFC_{\omega+1}$. – Noah Schweber Jun 13 '16 at 19:43
• @JoelDavidHamkins Yes, but of course comparing two $\le_\mathcal{O}$-incomparable notations is in general not effective. – Noah Schweber Jun 13 '16 at 19:44
• I disagree with your last statement. Saying "a bit" is a bit of an understatement. – Asaf Karagila Jun 13 '16 at 19:55

There's some nice exposition of this topic here:

https://xorshammer.com/2009/03/23/what-happens-when-you-iterate-godels-theorem/

• That is indeed really good! – Noah Schweber Jun 14 '16 at 1:53

This classic paper of Alan Turing is the first work on this problem:

http://www.turingarchive.org/browse.php/b/15

For more recent works, see these papers of Solomon Feferman and Torkel Franzen:

http://www.jstor.org/stable/2964649?seq=1#page_scan_tab_contents

To add to the references which have already been given, I'd like to point out that Torkel Franzén wrote an entire book (at a fairly elementary level, and with a number of IMHO rather interesting philosophical digressions) pretty much about answering this exact question: Inexhaustibility, A Non-Exhaustive Treatment, ASL Lecture Notes in Logic 16 (2004). Especially see chapters 13 ("Iterated Consistency"), 14 ("Iterated Reflection") and 15 ("Iterated iteration and inexhaustibility"): they include accounts of the results by Turing, Feferman and Franzén mentioned in Payam Seraji's answer.