What you propose is very reasonable, of course, since when we believe in a theory T, then it is natural for us also to believe that T is consistent. And the axioms that you propose to add to ZFC formalize this process. The (philosophical) question here is, does this process somehow find a completion? (Let me quibble with your remark that we can formalize ZFC<sub>α</sub> for *any* ordinal α. We need that the ordinal α is somehow representable in the theory in order for the assertion Con(ZFC<sub>α</sub>) to be expressible. Of course, in a countable language, we have only countably many statements, and so we must eventually run out of representable ordinals.) The answer is that your axioms are the pre-beginnings of the large cardinal hierarchy, as hinted at by Kristal Cantwell and Dorais. If there is a (strongly) inaccessible cardinal κ, then V<sub>κ</sub> is a model of ZFC, and so your theory ZFC<sub>1</sub> holds. But I claim much more, and from a weaker hypothesis. One doesn't need an inaccessible cardinal even to know that *all* the expressible ZFC<sub>α</sub> are consistent. I claim that if there is an ω model of ZFC, then all the expressible ZFC<sub>α</sub> are true and consistent. To see this, suppose that M is an ω model of ZFC. This means that M has the standard natural numbers. From this, it follows that the ordinals of M are well-founded for some distance above ω, but may become ill-founded much higher up. Since M has the same natural numbers as we do in the meta-theory, it follows that M has exactly the same formulas in the language of set theory and, more importantly, exactly the same proofs. Thus, for any theory T that exists in M, it will be consistent in M if and only if it is consistent. This is enough to perform an interesting ramping-up argument. Namely, since M is a model of ZFC, it follows that ZFC is consistent for us, and so M agrees, and so M is a model of ZFC+Con(ZFC), which is to say, of ZFC<sub>1</sub>. Thus, ZFC<sub>1</sub> is consistent, and so M agrees that ZFC<sub>1</sub> is consistent, and so M is a model of ZFC<sub>2</sub>. Thus, ZFC<sub>2</sub> is consistent, and so M agrees, and so ZFC<sub>3</sub> is consistent, and so on. Do you see how it works? If ZFC<sub>α</sub> is consistent, then M will agree (if α is in M), and so ZFC<sub>α+1</sub> is also consistent. (And limit stages are basically free, since proofs are finite.) So the scheme of theories ZFC<sub>α</sub> forms a hierarchy of consistency strength that sits very low below the beginning of the large cardinal hierarchy. I think much of the sense of your question is this: - We know by the Incompleteness theorem that no theory can prove its own consistency, and so we want to consider theories that transcend this consistency in the way you describe. And this is exactly what the large cardinal hierarchy provides. Each level of the large cardinal hierarchy implies the consistency of the lower levels, and the consistency of the consistency and so on, iterating in the style of your questions. But the large cardinals are able to jump higher than these small steps of consistency, by finding natural axioms that imply the consistency of all iterations of the consistency process that you describe for the lower levels. ----------- I just noticed the bit at the end of your question, about whether independence results also hold for ZFC<sub>α</sub>. This is a very interesting question, and the answer is Yes, they all work just the same. The reason is that all the independence results, proved either by forcing or by the method of inner models, have the property that the resulting models have the same arithmetic truths as the original model. Since the consistency statements you are considering are arithemtic statements, they are not affected by forcing or inner models. In particular, Cohen's proof that Con(ZFC) implies Con(ZFC+¬CH) turns directly into a proof that Con(ZFC<sub>α</sub>) implies Con(ZFC<sub>α</sub>+¬CH). If one formalizes a version of (ZFC+¬CH)<sub>α</sub>, it follows that it will be equivalent to ZFC<sub>α</sub>+¬CH. And the same holds for all the other indpendence results of which I am aware.