I recently saw the proof of the finite axiom of choice from the ZF axioms. The basic idea of the proof is as follows (I'll cover the case where we're choosing from three sets, but the general idea is obvious): Suppose we have $A,B,C$ non-empty, and we would like to show that the Cartesian product $A \times B \times C$ is non-empty. Then $\exists a \in A$, $\exists b \in B$, $\exists c \in C$, all because each set is non-empty. Then $a \times b \times c$ is a desired element of $A \times B \times C$, and we are done.

In the case where we have infinitely (in this case, countably) many sets, say $A_1 \times A_2 \times A_3 \times \cdots$, we can try the same proof. But in order to use only the ZF axioms, the proof requires the infinitely many steps $\exists a_1 \in A_1$, $\exists a_2 \in A_2$, $\exists a_3 \in A_3$, $\cdots$

My question is, why can't we do this? Or a better phrasing, since I know that mathematicians normally work in logical systems in which only finite proofs are allowed, is: Is there some sort of way of doing logic in which infinitely-long proofs like these are allowed?

One valid objection to such a system would be that it would allow us to prove Fermat's Last Theorem as follows: Consider each pair $(a,b,c,n)$ as a step in the proofs, and then we use countably many steps to show that the theorem is true.

I might argue that this really is a valid proof - it just isn't possible in our universe where we can only do finitely-many calculations. So we could suggest a system of logic in which a proof like this is valid.

On the other hand, I think the "proof" of Fermat's Last Theorem which uses infinitely many steps is very different from the "proof" of AC from ZF which uses infinitely many steps. In the proof of AC, we know how each step works, and we know that it will succeed, even without considering that step individually. In other words, we know what we mean by the concatenation of steps $(\exists a_i \in A_i)_{i \in \mathbb{N}}$. On the other hand, we can't, before doing all the infinitely many steps of the proof of FLT, know that each step is going to work out. What I'm suggesting in this paragraph is a system of logic in which the proof of AC above is an acceptable proof, whereas the proof of FLT outlined above is not acceptable.

So I'm wondering whether such a system of logic has been considered or whether any experts here have an idea for how it might work, if it has not been considered. And, of course, there might be a better term to use than "system of logic," and others can give suggestions for that.