# Infinitary logics and the axiom of choice

Suppose we want to enhance ZF by allowing for infinitary formulas instead of just first-order ones in our axiom schema of separation and/or replacement. It seems that we don't need much power in our infinitary logic for the resulting system to also imply some form of the axiom of choice - or perhaps implicitly assert it - and I am curious how to make sense of this. The basic idea:

1. We have a set of sets called $$S$$, and we want to build a choice function as a set of pairs $$(x \in S, y \in x)$$.
2. We note that for any particular $$x \in S$$ and $$y \in x$$, the pair $$(x, y)$$ exists as a set. Also, there exists some singleton formula which is only true for this set.
3. Using some appropriate infinitary logic, we guarantee the existence of various infinitary disjunctions of these singleton formulas, of which many will be valid choice functions.
4. Then, via specification on the set $$S \times \cup S$$, we guarantee that these are also sets.

Of particular interest to me is that you get some version of the above even with relatively "reasonable," fairly tame infinitary logics. For instance $$\mathcal{L}_{\omega_1, \omega}$$ lets you build these kind of countable disjunctions of singleton formulas, as long as you have equality and constant symbols for elements of the domain. So if $$S$$ is countable, we'd have a choice function. Thus, from $$\mathcal{L}_{\omega_1,\omega}$$ we get countable choice.

My question is just to ask what is going on here! The above line of reasoning makes sense to me, but infinitary logic is weird and I've never heard of this before. The situation with $$\mathcal{L}_{\omega_1,\omega}$$ is particularly interesting to me. Am I nuts? If not, is there any general statement that can be made about what happens if we augment ZFC with various infinitary logics in this way?

What you're basically describing is the result of replacing, in the usual definition of $$\mathsf{ZF}$$, schemes ranging over first-order formulas by schemes ranging over formulas in a different logic $$\mathcal{L}$$; call the resulting $$\mathcal{L}$$-theory $$\mathscr{ZF}[\mathcal{L}]$$ (so in particular $$\mathsf{ZF}=\mathscr{ZF}[\mathsf{FOL}]$$).

Actually depending on how exactly you define $$\mathscr{ZF}[\mathcal{L}]$$ this may not be quite right - in order to run your argument we also want to tweak the way parameters show up, so that a sentence can use infinitely many parameters - but I'm going to ignore this subtlety since it's not really the key point here.

This is indeed something we can do; see e.g. this old MSE post of mine. And, as you observe, using infinitary logics seems to give us some choice.

However, there's a crucial subtlety here. What we can prove is the following:

$$(*)\quad$$ Suppose $$M$$ is a model of $$\mathscr{ZF}[\mathcal{L}_{\omega_1,\omega}]$$. Then $$M$$ satisfies countable choice.

But this proof itself assumes countable choice in the metatheory in order to argue that the relevant infinitary formulas actually exist! The infinitary formula you invoke to show that $$S$$ admits a choice function is really no less complicated than a choice function for $$S$$, after all. In particular, $$(*)$$ is a theorem of $$\mathsf{ZFC}$$ + "Every set is contained in a transitive set model of $$\mathsf{ZFC}$$" but is not a theorem of $$\mathsf{ZF}$$ + "Every set is contained in a transitive set model of $$\mathsf{ZF}$$."

This is closely related to Quine's objection to second-order logic as "set theory in sheep's clothing." When $$\mathcal{L}$$ is a "strong" logic, the $$\mathcal{L}$$-theory $$\mathscr{ZF}[\mathcal{L}]$$ is more dependent on (or perhaps "aware of") the background reality than we may expect it to be since for example whether or not choice holds in reality has no bearing on whether or not choice is provable in the first-order theory $$\mathscr{ZF}[\mathsf{FOL}]$$.

• Thanks, makes sense! I get your objection that asserting the existence of these infinitary formulas is similar to just asserting AC. Regarding modeling $\mathscr{ZF}[\mathcal{L}_{\omega_1,\omega}]$ in some (first-order?) meta-theory: the reason I brought up $\mathcal{L}_{\omega_1,\omega}$ to begin with is that it seems reasonably well-behaved in that it has a completeness theorem. Is it possible to say anything cogent about what can be proved directly from the theory $\mathscr{ZF}[\mathcal{L}_{\omega_1,\omega}]$ without interpreting it within some first-order theory? Commented Jun 20 at 5:37
• @MikeBattaglia The whole point of my answer is that even $\mathcal{L}_{\omega_1,\omega}$ is such a set-theoretically-complicated object that it doesn't make sense to divorce it from the metatheory. We don't even "know" what the formulas of $\mathcal{L}_{\omega_1,\omega}$ are without some appeal to the structure of infinite sets! Commented Jun 20 at 5:41
• @MikeBattaglia Of course, we can compromise by using a weak background theory - e.g. ask what about $\mathscr{ZF}[\mathcal{L}_{\omega_1,\omega}]$ we can prove in just $\mathsf{ZF}$, and call this the "direct consequences" of $\mathscr{ZF}[\mathcal{L}_{\omega_1,\omega}]$ - but that winds up breaking the argument in your original post. Commented Jun 20 at 5:44
• Yes, I see what you are saying: we clearly can't solve the problems with first order logic, which doesn't know what "all" predicates are, by moving to a logic which now requires us to know what "all" formulas are. So in some sense one can raise the same kind of objection as with second order logic. I'm somewhat surprised that the consensus is so strong against any form of infinitary logic at all, though, given Zermelo's interest - intapi.sciendo.com/pdf/10.2478/slgr-2021-0042 - though perhaps such things were viewed differently back then. Commented Jun 20 at 6:14
• @MikeBattaglia It doesn't seem to me that anything Noah Schweber said implies a "strong consensus against any form of infinitary logic" per se. It's just that infinitary logic doesn't really give us any philosophical insight into whether countable choice is "true." $\mathcal{L}_{\omega_1,\omega}$ is not really "tame" as far as countable choice is concerned. That said, in principle, there might be other foundational questions that $\mathcal{L}_{\omega_1,\omega}$ could shed some light on. Commented Jun 21 at 10:34