Consistent hierarchy of axiomatic systems

First of all, I am not an expert in model theory. I just want to get my personal view on the foundations of mathematics straight.

I just learned in Sergey Melikhov's answer to another question something about the Axiom of Determinacy (AD). This Axiom is equivalent to the statement:

$\forall G \subseteq Seq(S):$

$$\forall a \in S :\exists a' \in S :\forall b \in S :\exists b' \in S :\forall c \in S :\exists c' \in S ... : (a,a',b,b',c,c'...) \in G$$ or $$\exists a \in S :\forall a' \in S :\exists b \in S :\forall b' \in S :\exists c \in S :\forall c' \in S ... :(a,a',b,b',c,c'...) \notin G$$

where $Seq(S)$ is the set of all $\omega$-sequences of some countable set $S$. It is thus some infinitary generalization of de Morgan's rule and seems rather natural. $ZF+AD$ seems to be rather realistic (in my opinion) version of set theory, in the sense that it avoids many unphysical paradoxes (such as non-measurable sets, paradoxical decompositions, non-continuous linear functions on Banach spaces etc.) Still, it seems to be strong enough to reproduce enough infinitary mathematics, so that a development a lot of mathematics and of theoretical physics etc. is possible.

It is a fact that $ZF+AD$ can prove consistency of $ZF$. Basically, the question is whether one can continue this process. The question is more precisely:

Question: Is there a hierarchy, which consists of an axiom $AD_{\alpha}$ for each ordinal some ordinals $\alpha$ (inspired maybe by some version of de Morgan's laws for ordinal sequences of quantifiers applied to sets of sequences in sets of some cardinality), such that $AD=AD_{1}$ and $ZF + \cup_{\beta \leq \alpha} ZF_{\beta}$ can prove consistency of $ZF + \cup_{\beta < \alpha} ZF_{\beta}$.

If that is the case, why not taking $ZF + \cup_{\alpha} AD_{\alpha}$ as the axiomatic foundation of mathematics. The bad thing about this would be that the axioms do not form a set, the payoff would be that it proves the consistency of itself and is philosophically sound.

EDIT: From Emil Jeřábek's comment I understand that the question does not make sense as stated since there are only countably many formulas and hence there cannot be uncountably many axioms. So the right (and more modest) question to ask would maybe be the following:

Question: Does there exist an equally natural axiom $AD'$ (based again on some infinitary version of a well-known principle like de Morgan's laws) which proves (together with $ZF+AD$) consistency $ZF + AD$?

Maybe there is also some infinitary version of set theory which allows for sentences of arbitrary length like the one which was used above to describe the meaning of $AD$. This could be the place, where the first question could have an answer.

-
There are only countably many formulas in the language of set theory, so you cannot in principle iterate this up to uncountable ordinals. In fact, "can prove consistency of $ZF+\bigcup_{\beta<\alpha}ZF_\beta$" is meaningless unless the latter theory is supplied with a recursive axiomatization in some canonical way, which is the reason why consistency statements (and reflection principles and similar business) can usually only be iterated up to $\alpha<\omega_1^{CK}$ (the Church–Kleene ordinal). –  Emil Jeřábek Feb 21 '11 at 15:10
@Emil Jeřábek: Thanks a lot for your comment. So far, I am just trying to make as much sense as possible of this rough idea. The statement above with the infinite sequence of quantifiers does also not make sense literally, but it has a meaning if you interpret it suitably. But I see, since there are only countably many formulas at all, you cannot have uncountably many axioms. Maybe what I am asking for has to be formulated in some sort of infinitary logic where statements like the one in my informal description of AD really exist. –  Andreas Thom Feb 21 '11 at 17:33
There are only countably many formulas in the language of set theory, so there's no such collection $ZF + \cup _{\alpha} AD_{\alpha}$ of axioms that don't form a set. –  Amit Kumar Gupta Feb 21 '11 at 17:40
Well, you can indeed get a lot of infinite combinatorics out of AD. The question is whether you would like to give up useful things like the Hahn-Banach theorem. –  Stefan Geschke Feb 21 '11 at 18:39
Stefan, Hahn-Banach for separable Banach spaces can be proved with AD. That is sufficient for many applications. Since many interesting inseparable Banach spaces have a separable pre-dual, many arguments are still valid; but of course, careful analysis is needed. –  Andreas Thom Feb 21 '11 at 19:04

There is a generalization of the compactness theorem to infinitary logics that sounds somewhat close to what you want. Specifically, the compactness theorem tells us that every finitely satisfiable theory of the usual formulas from a first-order language $L$ is satisfiable. For any uncountable cardinal $\kappa$, we can extend $L = L_{\omega, \omega}$ to the infinitary language $L_{\kappa, \kappa}$ by closing the usual formulas under $\bigwedge_{\xi < \lambda}\varphi_{\xi}$, $\bigvee_{\xi < \lambda}\varphi_{\xi}$, $\exists \langle x_{\xi}| \xi < \lambda\rangle$, and $\forall \langle x_{\xi}| \xi < \lambda\rangle$ for all $\lambda < \kappa$. We then define $\kappa$ to be strongly compact if an analogous theorem holds for arbitrary $L_{\kappa, \kappa}$, mainly that if every collection of fewer than $\kappa$ many statements from a theory in $L_{\kappa, \kappa}$ is satisfiable, then the theory is satisfiable.

Now let me emphasize that while ZF + AD may sound natural, it does much much more than prove the consistency of ZF. In fact, ZF + AD proves the consistency of ZFC + "There exists a Woodin cardinal", and Woodin cardinals are quite high up in the large cardinal hierarchy (i.e., a sufficiently stronger theory than ZF that is more likely to be inconsistent than ZF alone). Also, since set theorists tend to like having choice, the usual assumption is not that AD holds in our universe. Instead, we assume that it holds in the minimal transitive ZF model containing all of the ordinals and all of the reals, i.e., $L(\mathbb{R})$.

Now from ZFC + "There exists a strongly compact cardinal", we can prove that ZF + AD holds in $L(\mathbb{R})$. Moreover, we can prove that for every $\alpha$, there exists $\beta > \alpha$ such that AD holds in the set $L_{\beta}(\mathbb{R})$. In particular, ZFC + "There exists a strongly compact cardinal" proves CON(ZF + AD), CON(ZF + AD + CON(ZF + AD)), CON(ZF + AD + CON(ZF + AD + CON(ZF + AD))), etc.

The above result illustrates how assuming a strongly compact cardinal is also a very strong large cardinal hypothesis, but it is only one (admittedly significant) jump higher in our large cardinal hierarchy.

-
>"In fact, ZF + AD proves the consistency of ZFC + "There exists a Woodin cardinal"" Is that right? Or should it be "ZF + "There exists a Woodin cardinal""? (Disclaimer - I'm not a set theorist, it just seems to contradict what you say a few lines later) –  David Roberts Feb 24 '11 at 2:06
I meant what I typed: ZFC + "There exists a Woodin cardinal". What does it seem to contradict so I can clarify what I mean? In general, we can have ZF models that think that a statement is impossible but still think it's relatively consistent with ZF (i.e., think that there's a set model of ZF where it's true). –  Jason Feb 24 '11 at 3:12
ZF + AD proves the consistency of ZFC + "There exists a Woodin cardinal," not just ZF + "There exists a Woodin cardinal." In fact it proves the consistency of ZFC + "There exist infinitely many Woodin cardinals." –  Oliver Feb 24 '11 at 3:24
@Oliver: You probably meant *CON*(ZF + AD) implies CON(ZFC + "There exist infinitely many Woodin cardinals"). ZF + AD cannot prove this (assuming ZF + AD is consistent) or it would prove its own consistency since CON(ZFC + "There exist infinitely many Woodin cardinals") implies CON(ZF + AD). In a model where ZF + AD holds, its inner model $\text{HOD}^{L(\mathbb{R})}$ will model ZFC + "There exists infinitely many Woodin cardinals", but this is a proper class. You can for any $n \in \mathbb{N}$ prove the consistency of ZFC + "There exists $n$ Woodin cardinals" from ZF + AD b/c it holds in cuts. –  Jason Mar 17 '11 at 1:10
Regarding the sentences of arbitrary length, they can be expressed with the help of infinitary logics. Roughly, the language $L_{\kappa,\lambda}$ is similar to other formal languages except for the fact that it allows any conjunction or disjunction of less than $\kappa$ sentences (and provides for an infinitary form of De Morgan's rules), and any chain of less than $\lambda$ quantifiers. So your informal $\forall a\in S:\exists a'\in S\cdots$ can be expressed properly in, say, $L_{\omega_1,\omega}$. However, I have no idea on whether someone has considered any axiom system analogous to ZFC which uses this language...
Actually, no, the game quantifiers with infinite alternating sequences of quantifiers cannot be expressed in $L_{\kappa,\lambda}$ for any $\kappa,\lambda$. See e.g. projecteuclid.org/euclid.pl/1235417276 . –  Emil Jeřábek Feb 21 '11 at 19:36
Also, you have mixed up $\kappa$ and $\lambda$. In $L_{\kappa,\lambda}$ you have conjunctions and disjunctions of size $<\kappa$, and homogeneous blocks of $<\lambda$ quantifiers. –  Emil Jeřábek Feb 21 '11 at 19:39
You're right, I didn't take into account the fact that the blocks of quantifiers must be homogeneous... otherwise we would have a transfinite Levi hierarchy for the complexity of the sentences. Do you have any idea on whether those kinds of languages (allowing some transfinite alternation of quantifiers) have ever been considered? (however it's not clear how one would interpret a sentence in such a language). P.S. yes, I mixed up $\kappa$ and $\lambda$, I just edited to fix that. –  David FernandezBreton Feb 21 '11 at 20:11
Transfinite alternation of quantifiers? No, I don't recall ever seeing more alternation than $\omega$ (as e.g. in the paper above). But I'm not very knowledgeable of this subject, people have considered many weird things, so you may be able to find something in the literature. (There is no particular problem in defining games with more than $\omega$ rounds and the corresponding strategies, which should take care of the semantics.) –  Emil Jeřábek Feb 22 '11 at 18:18