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](http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory#The_axioms) for the axiom of infinity in context.)



Does finite mathematics need the axiom of infinity?
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](http://en.wikipedia.org/wiki/Paris%2DHarrington_theorem), which proved that a certain Ramsey-like property is independent of PA. Another good example is [Goodstein Sequences](http://en.wikipedia.org/wiki/Goodstein%27s_theorem) which Anton mentioned.


