Axiom of choice in infinitary logic First of all, I am a beginner in the field of Set Theory and my knowledge about Infinitary Logic is only at the informative level, so my questions might be nonsense.
One could think that, for any set $S$ whose elements are non-empty sets $S_i$ (with $i\in I$), there is a function taking any element of $S$ and giving an element of $S_i$. This is clear, because $S_i\not=\varnothing$, so, we can take some element from $S_i$.
That is the naive way of thinking, because it is useful only for finite sets. This is because first order logic is finitary. In particular, you can't ask your butler to pick a sock arbitrarily from each box if you have infinitely many boxes, it would take (at least) all of eternity to have one set of socks, one from each box. This is where the axiom of choice comes in, stating that it is possible to obtain such a set (although there is no way to explain it to the butler in finite time).
I needed that very basic introduction to be able to continue my reasoning. It seems natural to me that an infinitary logic would allow a rule to obtain a choice function for any set. For example, applying "$S_i$ is non-empty, so take some element from it" infinitely many times. But I read on wikipedia something about infinitary logic and they talk about the axiom of choice being required in some cases. So, my reasoning above is surely wrong.
Now I can formulate my questions. Why isn't it possible to do something like the above? Does infinitary logic work otherwise? Is there an infinitary logic in which it is possible? And, if so, is it an extension of usual first-order logic or something bizarre?
Thanks for your answers.

Edit: after the dialogue with Asaf, it seems convenient to clarify some things.
First, the goal is to obtain the axiom of choice as a theorem from a
few axioms (such as $\mathsf{ZF}$) and the fact that an infinitary logic
allows infinite formulas and this can be exploited to obtain a choice
function for infinite sets (something similar to what is done with
finite formulas to obtain choice functions for finite sets).
Second, the problem is perhaps too open, since a specific logic would
have to be defined and some axioms introduced and, even if it were
possible to do the above, the problems involved in using an infinitary
logic are enormous.

 A: I think the following helps de-mystify things (it did for me, anyways):

To start with, let's forget about logic entirely for a second and look for a "purely mathematical" situation where the axiom of choice makes sense but fails. This is actually much easier to come by than you might expect. For instance, given a family of functions $\mathbb{F}$ on the real numbers, let $\underline{\mathbb{F}}$ be the two-sorted structure consisting of

*

*a "numbers sort" ranging over reals and a "functions sort" ranging over elements of $\mathbb{F}$, and


*the usual field structure on the numbers sort and the application operation relating the numbers and functions sorts.
Specifically, I'm interested in the case where $\mathbb{F}$ is the set of continuous functions; call this $\mathbb{F}_c$. We then have the following "failure of choice inside $\underline{\mathbb{F}_c}$:"

*

*the sentence $$(*)\quad\forall x\exists y[(x=0\leftrightarrow y=0)\wedge (x\not=0\leftrightarrow y=1)]$$ is true in $\underline{\mathbb{F}_c}$, but


*for no $f$ in the "function sort" of $\underline{\mathbb{F}_c}$ do we have $$\underline{\mathbb{F}_c}\models \forall x[(x=0\leftrightarrow f(x)=0)\wedge (x\not=0\leftrightarrow f(x)=1)].$$
What I want to emphasize is that there is no logical subtlety here at all. In particular, there is "in reality" a function $h$ with the property that for each $x\in\mathbb{R}$ we have $\mathbb{F}_c\models (x=0\leftrightarrow h(x)=0)\wedge(x\not=0\leftrightarrow h(x)=1),$ but this $h$ exists "outside" the structure-of-interest $\underline{\mathbb{F}_c}$. And it doesn't matter what logic we decide to use to talk about this structure.

Taking logic back into account, one way to describe the situation that I like is the following:
When we choose to analyze a structure $\mathfrak{A}$ using a logic $\mathcal{L}$, we might choose to think of the logic $\mathcal{L}$ as a giant machine whose behavior is determined by our "metatheory." In particular, depending on the details of $\mathcal{L}$ and our metatheory it is entirely possible that $\mathcal{L}$ can "build choice sequences" for every family of sets coming from $\mathfrak{A}$. However, this has no bearing on whether $\mathfrak{A}$ satisfies (the appropriately-phrased "internal" version of) the axiom of choice: the giant machine $\mathcal{L}$ can build whatever shiny objects it wants to, but those objects might not have counterparts in the possibly-very-limited structure $\mathfrak{A}$. Tension only appears in this context emerges when we try to smuggle in an implicit assumption that the structure we're looking at "does everything our machines can do" - that is, when we conflate theory (= the hypotheses on our structure-of-interest $\mathfrak{A}$) and metatheory (= that part of our metatheory governing $\mathcal{L}$).
(In fact when we're careful to avoid this conflation there is a lot of interesting stuff to do involving versions of $\mathsf{ZF}$ for logics other than first-order logic - see e.g. this old question of mine - but in order to put this on firm ground we have to be very careful about "language level" issues.)
