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:

- 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)$.
- 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.
- 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.
- 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?