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

2$\begingroup$ I am not sure what you mean by "consistent" (there is no natural syntactic notion). Also, I don't see how your notion of ZFC2 is more explicit than Kreisel's. If T is satisfiable, then at least one of T+CH, T+nonCH is also satisfiable, and both of these systems are as recursive as T is. $\endgroup$ – Goldstern Oct 17 '11 at 17:12
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.

$\begingroup$ See my comment in response to the answer of Andreas above. $\endgroup$ – Garabed Gulbenkian Oct 14 '11 at 18:21

$\begingroup$ Actually I thought that my statement in quotes is equivalent to your statement in quotes, but maybe I am missing something. $\endgroup$ – Garabed Gulbenkian Oct 14 '11 at 18:32

$\begingroup$ This answer was many years ago, but in case anyone is still reading, here is a followup. Does the same concept apply to ZF2 for AC? That is, I understand that ZFC2, with the additional axiom that there are no strongly inaccessible cardinals, is categorical, hence CH is decided one way or another (though we don't know how). Do we have the same exact situation with ZF2? Do large cardinals change the story at all? $\endgroup$ – Mike Battaglia Oct 21 '17 at 21:47

$\begingroup$ What do you mean by "note that in order for secondorder logic to make sense, we have to make a commitment to an underlying 'real' universe of sets"? Something like: we need a settheoretic metatheory in order to make sense of the semantics of SOL? Is that really true? Can't we understand SOL ab initio? $\endgroup$ – Jori Apr 26 '20 at 16:48

$\begingroup$ @Jori "we need a settheoretic metatheory in order to make sense of the semantics of SOL" Yeah, basically. In order to tell whether a secondorder sentence is true in a structure $\mathcal{A}$, we need in general to have access to the whole powerset of $\mathcal{A}$ (in contrast to firstorder logic). So for example in order to talk about whether a secondorder sentence is true of the natural numbers, we need to admit completed infinite sets into our framework (to quantify over them). $\endgroup$ – Noah Schweber Apr 26 '20 at 16:56
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.

$\begingroup$ In response to your answer, Andreas, I should have explained more clearly what I mean by saying that a theory A is a subtheory of a theory B. I mean that the set of axioms (both logical and nonlogical) of A is a subset of the set of axioms of B. How do you know that either CH or its negation are among the axioms of ZFC2 since the set of axioms of ZFC2 is not recursively enumerable. Perhaps neither CH nor its negation is an axiom of ZFC2. $\endgroup$ – Garabed Gulbenkian Oct 14 '11 at 18:15

$\begingroup$ Since you want the question to refer to the sets of axioms, I'm curious what you take to be the set of axioms of ZFC2; in other words, what set should T be a subset of? I suppose the settheoretic axioms should be those of firstorder ZFC except that the replacement schema is replaced with the obvious single secondorder axiom. But what should the logical axioms be? $\endgroup$ – Andreas Blass Oct 14 '11 at 19:02

$\begingroup$ Yes, you definitely need to clarify what you mean by $ZFC_2$ here. My gut instinct is what I said below: there's no good way to get what you want to be true. (Also, @Andreas: is secondorder replacement enough to get secondorder powerset? Because I'd think we'd definitely want secondorder powerset.) $\endgroup$ – Noah Schweber Oct 14 '11 at 20:54

$\begingroup$ In the last chapter of the book "Theory of Recursive Functions and Effective Computability" by Hartley Rogers, it is stated that the set L of logical axioms of Secondorder Arithmetic (and thus no doubt of ZFC2 also) is not only nonrecursively enumerable but is of high rank in the Analytical Hierarchy of Descriptive Set Theory. $\endgroup$ – Garabed Gulbenkian Oct 17 '11 at 15:02

2$\begingroup$ @Garabed: If you identify "logical axiom of ZFC2" with "true sentence of pure secondorder logic", then, by Kreisel's observation, either CH is one of those axioms, or notCH is one of those axioms. So that axiom, whichever one it is, gives you a singleton subset axiomatizing a subtheory of ZFC2 that trivially decides CH. (Note that CH is expressible in pure secondorder logic; the formulation would begin with "for every Dedekindcomplete ordered field ....") $\endgroup$ – Andreas Blass Oct 18 '11 at 20:52