Are there first-order statements that second order PA proves that first order PA does not? Are there first-order statements that second order PA proves that first order PA does not? Is this known one way or the other? Could you share an example? (edit: to clarify, by 'second order PA' I don't mean any first order theory)
 A: This question more or less reduces to asking for natural arithmetic statements unprovable in PA.  A very interesting but lesser-known example that I learned about recently concerns fusible numbers. The term "fusible" may be unfamiliar but it arises as a natural generalization of a well-known puzzle involving measuring lengths of time by burning fuses (finite pieces of string) of different lengths.  The puzzle is an old one and was not specifically constructed to produce unprovable statements, so the unprovable statements involving fusible numbers are arguably the most "natural" PA-unprovable statements around.
A: According to Wikipedia, Goodstein's Theorem is provable from second order arithmetic, and since it implies Con(PA), PA can't prove it, assuming that PA is consistent. "Kirby and Paris showed that [Goodstein's Theorem] is unprovable in Peano arithmetic (but it can be proven in stronger systems, such as second-order arithmetic)."
A: It depends what you mean by "second-order $\mathsf{PA}$." If you really mean full second-order $\mathsf{PA}$, then since that theory characterizes $\mathbb{N}$ up to isomorphism it's complete, and consequently all the sentences first-order $\mathsf{PA}$ doesn't prove (of which there are lots, per Godel) are examples.
However, in my experience people often say "second-order $\mathsf{PA}$" when what they really mean is the first-order, two-sorted theory $\mathsf{Z}_2$, which is annoyingly called "second-order arithmetic." This theory consists of the ordered semiring axioms, the axiom of extensionality, and the comprehension and induction schemes over all two-sorted formulas allowing arbitrary parameters. $\mathsf{Z}_2$ is a computably axiomatizable first-order theory, hence per Godel is not complete.
That said, $\mathsf{Z}_2$ is vastly stronger than $\mathsf{PA}$ even for first-order sentences. The most obvious examples are consistency principles: among others, $\mathsf{Z}_2$ proves $\mathsf{Con(PA), Con(ATR_0)}$, and $\mathsf{Con(\Pi^1_n-CA_0)}$ for each $n\in\mathbb{N}.$ That said, keep in mind that $\mathsf{PA}$ is quite strong - there are very few sentences in the language of first-order arithmetic which are independent of $\mathsf{PA}$ and are "natural" (and in particular aren't consistency/soundness/etc. principles). Of course, this last bit is subjective, and Harvey Friedman for example would argue that there are actually lots of these, but in my opinion they're not really that natural.
