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