Are there any examples of second order arithmetic statements that are independent of ZFC? There are first order statements that are independent, often linked to the halting problem. One is used to put an upper bound on what n the busy beaver problem can be solved. 
There are examples of third order statements that are independent, the continuum hypothesis being the most famous example.
I don't know of any second order arithmetic statements that are independent though, are there any known examples that aren't trivially reducible to a first order statement? Are they shown true or false by large cardinals or are they truly unsolvable like the continuum hypothesis? 
 A: EDIT: A tangentially-related issue which came up in the comments was:

Are there natural axioms which settle CH but which don't "rule out" any sets?

Of course, both "natural" and "rule out" are subjective, but this is still a mostly-meaningful question one can ask. For instance, V=L rules out the existence of lots of things, so isn't allowed here.
There are two main types of axioms I know of which are natural (in my opinion), settle CH, and which add rather than restrict sets (again, in my opinion).


*

*Forcing axioms. These are statements of the form "If $\mathbb{P}$ is a 'nice' partial order and $\mathcal{D}$ is a 'small' collection of dense subsets of $\mathbb{P}$, then there is a $\mathcal{D}$-generic filter through $\mathbb{P}$." Remember that forcing adds totally generic filters; forcing axioms roughly state that a certain amount of forcing has "already happened" in a certain sense. CH itself can be thought of as a kind of degenerate forcing axiom; more natural is MA, which is consistent with CH (and consistent relative to ZFC). More interesting things happen when we look higher up: there are forcing axioms (the proper forcing axiom PFA and Martin's Maximum MM$^+$ are two of the more natural examples) which directly negate CH! These strong forcing axioms have high large cardinal strength, incidentally - e.g. PFA is known to have consistency strength at least as high as a proper class of strong cardinals and a proper class of Woodin cardinals, and is suspected to be equiconsistent with a supercompact (which is a known upper bound).

*Inner model hypotheses. Like forcing axioms, inner model hypotheses are statements which assert that the universe is "large" in precise ways, and I personally find them much more natural (although they have a number of strange properties). As far as I know, they were initially isolated by Friedman. The inner model hypothesis (IIMH) asserts that any parameter-free sentence that can hold in an inner model of an outer model of $V$, already happens in an inner model of $V$ (note that this is an external statement about $V$, not a statement inside $V$ itself - but we can still examine its consequences by looking at what must be true of a model which satisfies IMH; additionally, there are various first-order projections of IMH with the same implications, so this isn't too bad). E.g. if we force to add a bunch of Cohen reals (outer model) and look at an appropriate symmetric submodel (inner model of outer model), we get a model of ZF + "There is an amorphous set"; so IMH says that $V$ must already have an inner model with an amorphous set. Note that this kills $V=L$ right away. Going further, we can show that IMH implies that the singular cardinal hypothesis holds. Interestingly, it is inconsistent with large cardinals - IMH implies that there are no inaccessibles! So the idea that large cardinals don't rule out structure is not entirely true: even weak large cardinals rule out lots of interesting possible inner models. The one-sentence "sell" for large cardinals is not entirely true . . . And to make matters even more complicated, although it rules out large cardinals in $V$, it outright implies the existence of inner models with large cardinals (currently, we know it implies an inner model with measurable cardinals of arbitrarily high Mitchell order); and it is known to be consistent relative to large cardinals (a Woodin with an inaccessible above). Incorporating parameters, we get the strong IMH, which implies that the continuum hypothesis fails. SIMH is not yet known to be consistent relative to large cardinals, but frankly I find it much more intuitively compelling than (say) a Woodin limit of Woodins.
Note that there's an interesting gloss on IMH that says that it does rule out sets by allowing lots of classes; and so the large cardinal vs. IMH distinction comes down to whether we want interesting class structure or interesting set structure, and the observation that "ZFC + IMH + inaccessible" is inconsistent shows that these are fundamentally orthogonal behaviors. I think an important question in philosophy of mathematics is to understand the arguments for maximal class structure, as opposed to maximal set structure, better, and to come to a good philosophical understanding of why they oppose each other.

Yes, there are lots.
For example, consider the statement 

$(*)\quad$ "There exists a nonconstructible real."

This is second-order (specifically, $\Sigma^1_3$), and undecidable from ZFC: Goedel showed that ZFC+$V=L$ is consistent relative to ZFC, and Cohen showed that ZFC+"There is a nonconstructible real" is also consistent relative to ZFC (specifically, if $M$ is a model of ZFC and $M[G]$ is a generic extension containing a new real, then $M[G]$ does not satisfy $(*)$).
It is not immediate that $(*)$ is second-order (or even expressible in the language of set theory), but set theory texts like Kunen or Jech go into the details of how to do this. Note that $(*)$ is a second-order version of the higher-order principle "$V=L$".

We can also get second-order versions of first-order principles - e.g. the statement "There is a countable well-founded model of ZFC" is second-order when formalized appropriately, and is strictly stronger than the first-order sentence "ZFC is consistent" (incidentally, if we dropped "well-founded" we'd just get usual consistency by the Completeness Theorem).
And there are also examples of statements which appear third-order, but since they only involve quantification over simply-definable sets of reals are expressible in second-order, like "There is a $\Delta^1_4$ well-ordering of $\mathbb{R}$" or "Every $\Sigma^1_{15}$ game on $\omega$ is determined." These statements are often intertwined with large cardinal axioms - e.g. large cardinals imply that simply definable games are determined and simply definable relations do not well-order $\mathbb{R}$. 
Finally, there are second-order statements about individual reals which are intertwined with large cardinals - e.g. "$0^\sharp$ exists".

Incidentally, you may be interested in Shoenfield absoluteness: this states (among other things) that no $\Pi^1_2$ sentence can be altered by forcing. So any $\Pi^1_2$ sentence can't be shown independent of ZFC via forcing (it may be independent of ZFC, but forcing won't help demonstrate that).
