Does finite mathematics need the axiom of infinity?

Question

A statement referring to an infinite set can sometimes be logically rephrased using only finite sets/objects. For example, "The set of primes is infinite" <-> "There is no largest prime". Pleasantly, the proof of this statement does not seem to need infinity either (assume a largest prime, contradiction).

What reason is there, other than convenience or curiosity, to adjoin infinite sets to our universe by axiomatically declaring that one exists?

Specifically:

What is an example of a theorem in ZF or ZFC which 1) does not refer to infinite sets, but 2) cannot be proven if the axiom of infinity is excluded?

(See Zermelo–Fraenkel set theory for the axiom of infinity in context.)

Answer 1

ZF - infinity + not infinity is bi-interpretable with Peano Arithmetic. Bi-interpretable means that a model of either one can view a subset of itself as a model of the other (all in a definable way). So ZF - infinity can't prove anything that PA wouldn't prove.

There are some fairly natural statements which are independent of PA but provable in ZF. In fact, they're provable in theories much weaker than ZF. The first convincing example was the Paris-Harrington Theorem, which proved that a certain Ramsey-like property is independent of PA. Another good example is Goodstein Sequences which Anton mentioned.

Answer 2

Note that this question is part of Hilbert's program. (http://en.wikipedia.org/wiki/Hilbert%27s_program)

The first part is to formalize mathematics. Some argue that the development of ZFC, together with the work of Russell/Whitehead and Bourbaki and others has done this, or at least shown that it is possible.

The second part is to prove that the resulting axiomatization is complete. Godel's results show that this can't be done.

The third part is to show (finitistically) that formalized mathematics is consistent. Godel's results show that standard finitistic mathematics (like Peano arithmetic) can't even prove itself consistent, much less the full formalized mathematics, but of course it doesn't rule out the possibility of finitistic systems like PA+Con(ZFC). Hilbert didn't anticipate this sort of result because he didn't realize that every theory even of finitistic mathematics would be incomplete.

The fourth part is what you ask here, to show that full formalized mathematics is conservative over the finitistic part. Since ZFC proves Con(PA), but PA doesn't, Godel's results already show that this was impossible. Paris-Harrington, and Goodstein's theorems, and other examples mentioned above are nice additions only because they show that relatively straightforward statements are independent. (All three of these results are just statements that every natural number has some particular property, though the property used in Con(PA) is the property of not being the Godel code of a proof of a contradiction from the axioms of PA, which is more complicated than the properties used in the others.)

The fifth part of Hilbert's program was to give a decision procedure for all mathematical statements. This of course is far more ambitious even than the 10th problem and various other problems that have turned out to be impossible. But again, Godel's results already showed that this part was doomed, because any decision procedure could be used to generate a complete axiomatization of mathematics.

Answer 3

This may be off base, but maybe this is the kind of thing you're looking for.

Start with a positive integer, like 5, and write it entirely in base 2. That is, write every number that appears in base 2, so 5=2²²⁰+2⁰. Now change all the 2's to 3's and subtract 1 to get 27. Write that entirely in base 3, so 27=3³³⁰. Change all the 3's to 4's and subtract 1. Keep going, always replacing n by (n+1), subtracting 1, and writing the number "entirely in base (n+1)".

The result is that no matter what positive integer you start with, you'll eventually get to 0. The usual proof is a complexity argument that uses ω.

Edit: this result is called Goodstein's Theorem

Answer 4

Well, certainly one good reason to adjoin infinite sets to our universe it that they're so interesting in their own right. We're not exclusively interested in results about finite sets!

Still, it is true that there are "finitistic" statements that cannot be proved by finitistic methods. One way to see this is just to apply Gödel's incompleteness theorem to a theory such as PA or, as you suggest, ZF-{axiom of infinity}. For example, letting P be the latter theory, the consistency of P itself is a "finite" statement (asserting that there is no number which encodes a proof of 1=0 in P, and "encoding a proof of 1=0" is essentially just a big, messy, but finite expression). However, that statement cannot be proven in P, while it can be proven in ZF itself (by exhibiting a model of P).

More concrete examples of such statements are Goodstein's Theorem (alluded to by Anton), The Hydra game, and other statements found by Kirby, Paris, Harrington and Harvey Friedman.

Answer 5

This isn't nearly as rigorous, but morally, it often seems useful to consider infinite sets in Ramsey theory and Ramsey-type subjects. E.g., of course, the Paris-Harrington theorem deals with a Ramsey theory result! More interestingly, there are some techniques that do require the use of infinite sets (I'm thinking in particular of ergodic-theory methods) that haven't quite been satisfactorily finitized yet.

Answer 6

Doesn't "there is no largest prime" implicitly assume the existence of the natural numbers?