A question about Second-Order ZFC and the Continuum Hypothesis

Question

Some logicians-such as G. Kreisel-have stated that the Continuum Hypothesis is decided in ZFC2 ("Second-Order 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 non-logical) of ZFC2-as a formalized theory-is to include. ZFC2 is presumably formalized in the Classical Second-Order 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 sub-theory of ZFC2, then neither the Continuum Hypothesis nor its Negation is provable in T."

Answer 1

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 second-order 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 second-order 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 (left-to-right is trivial; right-to-left 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 second-order 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 second-order 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 second-order logic allows $V$ to "ask" certain set-theoretic 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 non-trivial, but also not false, statement. The moral is that second-order 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 second-order 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 - Lopez-Escobar 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, second-order 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 second-order version of the first-order theory which is commonly called, annoyingly enough, "second-order arithmetic" (so I guess its second-order counterpart should be called "second-order analysis"). This will be enough to decide CH, since the arguments above will all go through.

Answer 2

Either first-order ZFC plus CH is a counterexample to your weaker alternative, or first-order ZFC plus not-CH is a counterexample. The point is that, by Kreisel's observation, one of these is a sub-theory of ZFC2.