Modular Arithmetic (MA) has the same axioms as first order Peano Arithmetic (PA) except ∀x(Sx≠0) is replaced with ∃x(Sx=0). Let MA2 be the second-order variation, with second-order induction.

Answering to a question by Russell Easterly, Emil Jerabek has shown that

∃x(x≠0∧x+x=0) ∨ ∃x(x+x=S0)

is unprovable in MA. There is, however, a proof in MA2.

There are mathematical examples which distinguish first-order and second-order PA, but they are more esoteric (Paris-Harrington Theorem) or less mathematical (the consistency of first-order PA). So the result of Jerabek seems IMHO to be of interest, by providing a simple mathematical proposition and system where the second-order system can prove the proposition but not the first-order.

Are there other simple examples of a first-order theory T and an assertion S where T cannot prove S but second-order T, with second-order induction, can prove S? (Obviously, the interest of Emil's result increases if there are none which aren't "reasonably" equivalent.)