This present thread is inpired by the previous thread The true reason for the incompleteness of formal systemsThe true reason for 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?