Any “natural” examples of true statements in number theory not provable in 2nd order systems?

I know that there are a few theorems in number theory that are somehow known to be true, but have been shown not to be provable in first-order Peano arithmetic (PA).

Have any so-called "natural" examples of true statements in number theory (not some variation of the Liar Paradox) that have been shown to be unprovable in a system which allows quantification over sets (i.e. a 2nd order system)? How would you go about proving it?

• How about the statement claiming the consistency of second order arithmetic? – Andrés E. Caicedo Jan 22 '14 at 14:51
• I was looking for something a little more "natural." – Dan Christensen Jan 22 '14 at 14:53
• The Paris - Harrington theorem is well known, here's a link: en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem . – Alan Jan 22 '14 at 14:57
• @Alan I think you mean the Strengthened Finite Ramsey Theorem. PH proved that SFRT was unprovable in PA. At your link it says SFRT was, however, proven in "2nd order arithmetic." – Dan Christensen Jan 22 '14 at 15:10
• Goodstein's theorem is another good example of a "natural" true statement in number theory that is provable in a 2nd order system but not in first-order PA. See: en.wikipedia.org/wiki/Goodstein's_theorem – Dan Christensen Jan 22 '14 at 15:13

I do not believe there are any known examples like that. Of course the issue is "naturalness". But the general phenomenon is that the few somewhat-natural arithmetical principles known to be unprovable in PA are all provable in relatively modest fragments of second-order arithmetic.

Actually, it is even hard to find examples of natural statements in second order arithmetic that are not provable in second order arithmetic. Second order arithmetic is just phenomenally strong for proving theorems of non-set-theoretical mathematics.

For example, there was some discussion about whether Fermat's Last Theorem is provable in second-order arithmetic, because a cursory reading of the proof suggests it uses set theoretical methods. But the consensus of experts seems to be that FLT should be provable in PA, and quite possibly weaker systems, if the proof is revised to focus just on the case at hand without any artificial generality in the lemmas.

There is a closely related conjecture by Harvey Friedman, who states

Conjecture 1. Every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement) can be proved in EFA. EFA is the weak fragment of Peano Arithmetic based on the usual quantifier free axioms for 0,1,+,x,exp, together with the scheme of induction for all formulas in the language all of whose quantifiers are bounded. ... 1

The role of the Annals in that conjecture is to restrict the theorems to ones that have actually been studied by non-logicians.

• Is it fair then to say that, apart from variations of the Liar Paradox and formal proofs of consistency, there are no known examples of true statements in number theory that are not provable in certain 2nd-order systems (i.e. ones allowing quantification over sets). – Dan Christensen Jan 22 '14 at 16:18
• I don't know of any that I can think of after a little reflection. The issue of course is how "natural" each particular statement is. But if we are talking about statements of first-order arithmetic that are unprovable in second order arithmetic, it is hard to find any that is "natural". – Carl Mummert Jan 22 '14 at 18:12