# Can it be shown that there exists no finite proof of CH from second-order set theory?

As is well known, all models of (full) second order set theory (e.g., ZFC2) are quasi-isomorphic. This implies (or at any rate: has been taken to imply) that CH is "decided" by second-order set theory. Independently from all possible philosophical interpretations of this results, my questions is purely mathematical: can it (in light of the Gödel-Cohen independence result) be shown that there does not exist a finite derivation, neither of CH nor not-CH, from the axioms of ZFC2 using second order logic?

My immediate intuition was that any such proof, given that it can make use of at most finitely many axioms, ought to be translatable directly into a proof in ZFC, but I'm not sure whether I'm not overlooking something?

Edit2: I mean "quasi-isomorphic"/"quasi-categorical" in Zermelo's sense of "normal domains" (Normalbereiche): for any two models $$M$$ and $$N$$ of ZFC2 (without urelements), either one is a (possibly proper) rank initial segment of the other. That is, each model $$M$$ has an ordinal $$o(M)$$ associated with it (either omega or strongly inaccessible), which is the order type of its von Neumann ordinals. Each $$M$$ is characterized up to isomorphism by $$o(M)$$, and the substructures of any two models $$M,N$$ consisting of the sets of rank $$<\alpha$$ are isomorpic, provided $$\alpha$$ is not greater than $$o(N)$$ or $$o(M)$$. (Comp. Tait (1998), Zermelo's Conception of Set Theory and Reflection Principles.)

• (1) What does quasi-isomorphic mean here? (2) If you're using 2nd-order Replacement, then you might need to translate it to infinitely many axioms. (3) There's no completeness theorem for 2nd-order logic, so being valid does not mean provable. Sep 8, 2020 at 12:40
• @Asaf I believe the OP intended the quasi-categoricity of models of second-order $\mathsf{ZFC}$ Sep 8, 2020 at 12:45
• The point of (3) is that it's not at all clear what "derivation using second-order logic" even means. That needs to be pinned down before the question can be answered. As you observe at the beginning of the OP there is a finite fragment of $\mathsf{ZFC2}$ which semantically decides whether CH is true - so if the definition of "derivation" is loose enough we therefore get a positive answer. Sep 8, 2020 at 13:00
• @10012511 It's more naturally a corollary of the first incompleteness theorem in my opinion: there's a single second-order sentence which entails the full theory of arithmetic, and so from a c.e. sound-and-complete proof procedure for SOL we would get that $Th(\mathbb{N})$ is computable. Actually, this is really a corollary of Tarski's undefinability theorem: the argument of that theorem shows more generally that no logic $\mathcal{L}$ simultaneously has a "good Godel numbering system," extends a tiny fragment of FOL, and has the $\mathcal{L}$ theory of $\mathbb{N}$ be $\mathcal{L}$-definable. Sep 8, 2020 at 13:17
• @10012511 See my answer. Sep 8, 2020 at 13:21

As you observe at the beginning, $$\mathsf{ZFC2}$$ - indeed a finite fragment thereof - semantically decides whether $$\mathsf{CH}$$ holds. So if we interpret "derivation" sufficiently loosely, we get a positive answer.

However, this is a very loose interpretation of "derivation," and one which (in my opinion anyways) doesn't match what we actually mean. A derivation should be "concrete" in some sense. On the other hand, of course no forcing-invariant notion of "derivation" will suffice here ... and this leads to a strong negative result via absoluteness: there is no notion $$\Pi^1_2$$ notion of "derivation" which is sufficiently strong, and assuming large cardinal axioms we can push this well beyond $$\Pi^1_2$$.

(More precisely: there is no $$\Pi^1_2$$ formula which defines a notion of derivation sufficient to answer $$\mathsf{CH}$$ from $$\mathsf{ZFC2}$$ and which $$\mathsf{ZFC}$$ - the first-order one - proves is sound for SOL. And we can strengthen that under large cardinals.)

Let me put the above in a bit more context.

Via Godel, we can show that the set of second-order validities is not c.e. However, we can in fact do much better by following the argument of Tarski's undefinability theorem: that argument shows that there is no logic $$\mathcal{L}$$ which has a "good Godel numbering system" (specifically: so that the appropriate substitution functions are $$\mathcal{L}$$-definable), extends (a tiny fragment of) first-order logic, and has the property that the $$\mathcal{L}$$-theory of $$\mathbb{N}$$ is $$\mathcal{L}$$-definable. SOL clearly satisfies the first two conditions above. Moreover, since there is a single second-order sentence $$\theta$$ characterizing $$\mathbb{N}$$ up to isomorphism the set of second-order validities computes the second-order theory of $$\mathbb{N}$$: $$\mathbb{N}\models\varphi$$ iff $$\theta\rightarrow\varphi$$ is a second-order validity. Hence the set of second-order validities can't be second-order definable, or more reminiscently of the main answer can't be $$\Pi^1_n$$ for any $$n\in\omega$$.

Granted, the above isn't actually relevant to the question. In one direction, the Tarskain argument doesn't in any way point to a particular second-order sentence whose second-order-validity-status is "hard to determine," it just addresses the complexit of the whole set of second-order sentences. In the other direction, absoluteness/forcing arguments don't give Tarskian complexity: we can whip up a silly logical system which changes from model to model but which has low complexity in any particular model. But they do reinforce each other flavor-wise, in my opinion.

• The $\Pi_2^1$ absoluteness explanation is very illuminating. One question: what do you mean by "local obstacle" and "tameness"? Sep 8, 2020 at 13:29
• @10012511 See my edit. Sep 8, 2020 at 13:35
• Do you mean by "c.e." computationally enumerable (recursively enumerable), and if so, do you mean "the second-order validities are not c.e."? Sep 8, 2020 at 13:43
• @10012511 Computability theory/recursion theory has some serious language redundancy, with "computable/computably enumerable/etc." being used synonymously with "recursive/recursively enumerable/etc." Older texts also use "(semi)decidable" to mean "computabl(y enumerable), although that's less common now. But yes, I did miss a "not" - fixed. The "computable" language is more recent than the "recursive" language - that shift started in the 90s if I recall correctly (I wasn't very mathematical then) - and now there's roughly a 50/50 split between the "r" and "c" terminologies, annoyingly enough. Sep 8, 2020 at 13:50
• Another case in point: "entscheidungsdefinit" (Gödel), "decidable" (Heijenoort), "vertretbar" (Hilbert & Bernays), "numeralwise expressible" (Kleene), "definable" (Tarski, Mostowski & Robinson), "representable" (Enderton), "bi-numerable" (Feferman), "ziffernweise repräsentierbar" (Rautenberg), for predicates representable by a formula in an extension of Q. Sep 8, 2020 at 13:59