# Why can't proofs have infinitely many steps?

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.

-
I think something has gone wrong with copy/paste here. –  Eric Tressler Aug 29 '10 at 17:56
I object to your "proof" of FLT: you have not convinced me that every step in your proof is valid (or rather, I know it to be valid because I trust the peer-review system enough to believe that FLT is true, but if this is what your proof rests on, then it does not illustrate your discussion). –  Theo Johnson-Freyd Aug 29 '10 at 20:15
In principle why not; but the problems will start when you try to submit it. I tell you, nobody will publish infinitely many pages. –  Pietro Majer Aug 29 '10 at 20:26
Another thing that would be "fixed" by proofs with infinitely many steps: The existence of polynomials in several variables such that it is undecidable whether they have an integer root (cf mathoverflow.net/questions/32892/…), which seems absurd. It "should" be possible to just check all points in $\mathbf{Z}^n$, and either find a root or don't, but logic says no. –  Mike Hall Aug 29 '10 at 23:04
To Pietro: no problem, you split the proof in infinitely many papers. –  Angelo Jun 23 '12 at 11:40

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

-
+1 for an infinitely long proof having "a gap or two" :-) –  efq Jan 31 '11 at 7:03
-
I think this was better have been written as a comment, as answers should be slightly more verbal than a mere link to wikipedia. –  Asaf Karagila Aug 29 '10 at 18:13
+1 : This is a perfectly good answer. –  Andy Putman Aug 29 '10 at 19:15
When there is a good short answer that could be written, then just giving a link to Wikipedia is indeed lazy, and not as good as an answer that gives the link and then extracts the relevant parts so that someone can get the gist of the answer quickly on the spot. But in an open-ended question like this, there’s not really any full answer shorter than the Wikipedia article — and this answer gets that point across very, very well :-) –  Peter LeFanu Lumsdaine Jan 7 '11 at 17:50

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.

-
And I think it's worth adding that this idea is still finding application in proof theory and computer science, where an "infinite proof" can be seen as just a way of speaking about a lazily computed object. See for example [linta.de/~aehlig/university/pub/08-proofnotation.pdf On the Computational Complexity of Cut-Reduction] by Aehlig and Beckmann, from LICS 2008. –  Noam Zeilberger Aug 30 '10 at 12:24

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

-
I should mention that I'm not trying in any way to use this to prove number-theoretic statements like FLT, at least for a standard definition of "use." The point is a theoretical idea about the foundations of mathematics. –  David Corwin Jun 21 '12 at 21:27

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.

-

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.

-