Essentially, yes. An old result of Kleene [1], later strengthened by Craig and Vaught [2], shows that every recursively axiomatizable theory in first-order logic without identity, and every recursively axiomatizable theory in first-order logic with identity that has only infinite models, has a finitely axiomatized conservative extension. See also Mihály Makkai’s review, Richard Zach’s summary, and a related paper by Pakhomov and Visser [3].
Let me stress that the results above apply to the literal definition of conservative extension, i.e., we extend the language of $T$ by additional predicate or function symbols, and we demand that any sentence in the original language is provable in the extension iff it is provable in $T$. If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension.
But back to the standard definition. I’m assuming logic with identity from now on. What happens for theories that may also have finite models? First, [2] give the following characterization (they call condition 1 “f.a.${}^+$”, and condition 2 “s.f.a.${}^+$”):
Theorem. For any theory $T$ in a finite language, the following are equivalent:
- $T$ has a finitely axiomatized conservative extension.
- There exists a finitely axiomatized extension $T'\supseteq T$ such that every model of $T$ expands to a model of $T'$.
- $T$ is equivalent to a $\Sigma^1_1$ second-order sentence.
Following Dmytro Taranovsky’s comments, we have the following necessary condition (which is actually also mentioned in [2], referring to Scholz’s notion of spectrum instead of NP, which was only defined over a decade later):
Theorem. For any theory $T$ in a finite language, 1 implies 2:
- $T$ has a finitely axiomatized conservative extension.
- $T$ is recursively axiomatizable, and the set of its finite models is recognizable in NP.
Indeed, the truth of a fixed $\Sigma^1_1$ sentence in finite models can be checked in NP.
It is not known if this is a complete characterization: if $T$ is a r.e. theory whose finite models are NP, then $T$ is equivalent to a $\Sigma^1_1$ sentence on infinite models by [1,2], and $T$ is equivalent to a $\Sigma^1_1$ sentence on finite models by Fagin’s theorem, but it is unclear how to combine the two to a single $\Sigma^1_1$ sentence that works for all models. This is mentioned as an open problem in the recent paper [3].
References:
[1] Stephen Cole Kleene: Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two papers on the predicate calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952 (reprinted 1967), pp. 27–68.
[2] William Craig and Robert L. Vaught: Finite axiomatizability using additional predicates, Journal of Symbolic Logic 23 (1958), no. 3, pp. 289–308.
[3] Fedor Pakhomov and Albert Visser, On a question of Krajewski’s, Journal of Symbolic Logic 84 (2019), no. 1, pp. 343–358. arXiv: 1712.01713 [math.LO]
Best Answer
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.