Some logicianssuch as G. Kreiselhave stated that the Continuum Hypothesis is decided in ZFC2 ("SecondOrder ZFC") although we do not know which way it is decided. This is rather confusing, since it is not usually made clear just what the collection of axioms (both logical and nonlogical) of ZFC2as a formalized theoryis to include. ZFC2 is presumably formalized in the Classical SecondOrder Predicate Calculus which is not recursively axiomatizable. Is (at least) the following weaker alternative to Kreisel"s statement correct? "If T is any consistent and recursively axiomatizable subtheory of ZFC2, then neither the Continuum Hypothesis nor its Negation is provable in T."

Think of it this way: Let $V$ be a model of $ZFC_2$. Then I claim CH holds in $V$ if and only if $CH$ is actually true (note that in order for secondorder logic to make sense, we have to make a commitment to an underlying "real" universe of sets). The proof of this is as follows. First, $\omega^V$ has order type $\omega$: clearly it has a subset of order type $\omega$, and by the secondorder version of the powerset axiom, $P^V(\omega^V)=P(\omega^V)$, so if $\omega^V$ had the wrong order type $V$ would "see" the error. A fortiriori, we can deduce that $\omega^V$ is countable. By similar reasoning, $P^V(P^V(\omega^V))=P(P(\omega^V))$. Now CH is false if and only if $P(P(\omega^V))$ contains three infinite sets $X, Y, Z$ no two of which have the same cardinalities (lefttoright is trivial; righttoleft follows from the countability of $\omega^V$). Suppose $CH$ is false; let $X, Y, Z$ be as above. Since $P(P(\omega^V)=P^V(P^V(\omega^V))$, we have $X, Y, Z\in V$; by the axiom of extensionality, $V$ sees that the cardinalities of $X$, $Y$, and $Z$ are different, and by the secondorder powerset axiom $V$ sees that $X$, $Y$, and $Z$ are infinite. So $CH\implies (ZFC_2\models \neg CH)$. Suppose now that $CH$ is true. Let $X, Y, Z\in P(P(\omega^V))$; again, we have $X, Y, Z\in V$. Since $CH$ holds, by the secondorder powerset axiom plus separation we can find a bijection $f$ between two of $X, Y, Z$, so $CH$ holds in $V$. So $\neg CH\implies (ZFC_2\models CH)$. This shows that $ZFC_2\models CH$ or $ZFC_2\models \neg CH$. The point is that the full power of secondorder logic allows $V$ to "ask" certain settheoretic questions of the "real" underlying universe of sets; these questions include ``Is CH true?" Similarly, it seems to me that they include all questions of the form "Does $V_\alpha\models \phi$ hold?" where $\alpha$ is a computable ordinal and $\phi$ is $\Sigma_1$ over $V_\alpha$ ($\Sigma_1$ is somewhat arbitrary; higher quantifier depth can (I believe) be achieved by passing to larger computable $\alpha$). I'd imagine that in fact this phenomenon extends much further than what I've outlined, and that a staggeringly large class of sentences of set theory are known to be decided in $ZFC_2$, even if we don't know which way they are decided. I just realized that I didn't answer your actual question. As Andreas says above, your statement is not correct: both $ZFC+CH$ and $ZFC+\neg CH$ are recursively axiomatizable, and consistent (assuming $ZFC$ is), and one of them is a subtheory of $ZFC_2$ (although we can't tell which). You could try to add some effectiveness criterion to your statement  something along the lines of, "There is no recursively axiomatizable consistent theory $T$ which decides CH and that is provably a subtheory of $ZFC_2$"  but it's unclear to me how to do this in a way that results in a nontrivial, but also not false, statement. The moral is that secondorder logic is really nasty. For instance, it wouldn't even make sense to ask for a derivation of CH (or $\neg CH$) from $ZFC_2$, since there's no meaningful proof system for secondorder logic. To understand how ridiculously awful this is, there are proof systems for some infinitary logics that are very useful in model theory and proof theory  LopezEscobar developed one that Barwise used (altered? my history is a little vague on this point), but I don't know a good reference  and logics that can express concepts like "is uncountable" or can quantify over automorphisms of certain kinds of structures are even compact. Basically, secondorder logic is totally unusable (although, as always, there are exceptions). Also, it occurs to me that we don't even need all of $ZFC_2$ to decide CH. Look at the natural secondorder version of the firstorder theory which is commonly called, annoyingly enough, "secondorder arithmetic" (so I guess its secondorder counterpart should be called "secondorder analysis"). This will be enough to decide CH, since the arguments above will all go through. 


Either firstorder ZFC plus CH is a counterexample to your weaker alternative, or firstorder ZFC plus notCH is a counterexample. The point is that, by Kreisel's observation, one of these is a subtheory of ZFC2. 

