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

Question

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?

Edit: added "quasi-"isomorphic

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

Answer 1

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.