Why can't proofs have infinitely many steps?

Question

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.

Answer 1

http://en.wikipedia.org/wiki/Infinitary_logic

Answer 2

Even if logic were extended to allow infinitely long proofs, your attempted proof of the countable axiom of choice would still have a gap or two. After the infinitely many steps asserting that there exists an $a_i$ in $A_i$ (one step for each $i$), you still need to justify the claim that there's a function assigning, to each $i$, the corresponding $a_i$. The immediate problem is that your infinitely many steps haven't exactly specified which (of the many possible) $a_i$'s are the corresponding ones; the $a_i$'s in your formulas are just bound variables. Worse, even if the meaning of "the corresponding $a_i$" were perfectly clear, so that there's no doubt about which ordered pairs $(i,a_i)$ you want to have in your choice function, you'd still need to prove that there is a set consisting of just those ordered pairs. No ZF axiom does that job. I think you'd need an infinitely long axiom saying "for all $x_1,x_2,\dots$, there exists a set whose members are exactly $x_1,x_2,\dots$."

If you're willing to accept not only proofs consisting of infinitely many statements but also single statements of infinite length, and if you're willing to add some such infinite statements as new axioms, then I think you can "prove" the countable axiom of choice (and fancier choice principles if you allow even longer new axioms). But, as long as you need to add some axioms to ZF for this purpose, it seems simpler to just add the countable axiom of choice. It's a finite statement, so you can reason with it using the usual rules of logic.

One could view the axiom of choice as a sort of finitary (and therefore usable) surrogate for the infinitely long axioms and proofs that would come up in your approach. In fact, some of Zermelo's later work (he introduced the axiom of choice in 1904, and the work I'm thinking of dates from the late 20's or early 30's) takes an "infinitary logic" approach to the foundations of set theory (and is, in my opinion, not entirely clear).

Answer 3

Andreas Blass has nicely explained why it is not helpful to use infinitary logic in an attempt to prove the axiom of choice.

It may be worth adding that the seemingly similar idea, of considering countably infinite proofs in number theory, is helpful in a way (though not to prove FLT!). The so-called $\omega$-rule -- from proofs of $\varphi(0),\varphi(1), \varphi(2),\ldots$ to infer $\forall n\varphi(n)$ -- was used by Schütte around 1950 to simplify Gentzen's 1936 consistency proof for Peano arithmetic, PA.

Assuming $\varepsilon_0$-induction, it turns out to be easier to prove the consistency of a system PA$_\omega$ with the $\omega$-rule than to prove the consistency of the PA system it contains.

Answer 4

Your example concerning Fermat's theorem shows why we cannot do infinite proofs: your proof strategy is to check infinitely many instances, which a human being cannot do in a finite amount of time. Hence we only accept proofs dealing with infinitely many instances if we have some finite (finitistic) way of reasoning about all these instances, for instance by induction.

The fact that AC does not follow from the Zermelo-Fraenkel axioms, even AC for countable families of sets, shows that in first order logic we cannot do infinitary proofs as you suggest. But first order logic is pretty unique with respect to its nice properties.

Richard Borcherds mentions infinitary logic, which definitely has its uses, but I don't see how you can use infinitary logic to prove instances of AC, if your base theory is, say, ZF.
(Every first order sentence is also a sentence in infinitary logic.)
Infinitary logic could talk, for example, about infinitely many classes at the same time, but if you start from ZF, the infinitary logic (say $L_{\omega_1,\omega_1}$ to be specific) generated from it will have the same models as usual first order logic. If you add infinitary axioms that allow to prove more instances of AC, this means that you just add instances of AC to your axioms (possibly instances that you could not formulate by finitary first order axioms).

Answer 5

James Brotherston and Alex Simpson worked on non-well-founded proofs, see

J. Brotherston and A. Simpson: Sequent calculi for induction and infinite descent. J Logic Computation (2010)

as well as the talk "On Proof by Infinite Descent" by Alex Simpson at "Algebra & Coalgebra meet Proof Theory" in Bern, April 2012.

Answer 6

Somewhat semi-related, but I think also fitting here since connected to infinitary logic, are oracle-turing-machines. In the end, an Oracle can solve the finite Entscheidungsproblem - for your countable axiom of choice, or the theorem of fermat, you could just write an algorithm to search for a counterexample and pass it to your oracle, which will tell you whether it will terminate. Its not that this solves the problem by any means - its just a theoretical concept to do research on that kind of problem.