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][1], which proved that a certain Ramsey-like property is independent of PA. Another good example is [Goodstein Sequences][2] which Anton mentioned.


  [1]: http://en.wikipedia.org/wiki/Paris%2DHarrington_theorem
  [2]: http://en.wikipedia.org/wiki/Goodstein's_theorem