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, which proved that a certain Ramsey-like property is independent of PA. Another good example is Goodstein Sequences which Anton mentioned.
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.
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=2220+20. Now change all the 2's to 3's and subtract 1 to get 27. Write that entirely in base 3, so 27=3330. 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