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?
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.
