Infinitary logics and the axiom of choice

Question

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?

Answer 1

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}]$.