Is first-order logic a sufficiently powerful metatheory to prove the "conditional independence" of CH from ZFC? Lets define independence and conditional independence as follows. 1. Define that an axiom $X$ is independent from a system $Y$ if and only if $Y$ can be used to prove neither $X$, nor its (syntactical) negation $\mathop{\sim}X$. That is, $X$ is independent from $Y$ if and only if $\neg(Y \vdash X) \wedge \neg(Y \vdash \mathop{\sim}X).$ 2. Define that an axiom $X$ is conditionally independent from an axiom system $Y$ precisely when the consistency of $Y$ implies that $X$ is independent of $Y$. That is, $X$ is conditionally independent of $Y$ precisely when $\neg(Y \vdash \bot) \Rightarrow \neg(Y \vdash X) \wedge \neg(Y \vdash \mathop{\sim} X).$ Is first-order logic a sufficiently powerful metatheory to prove the conditional independence of CH from ZFC? My quess would be "no" because ZFC is not finitely axiomtizable.

Raw first-order logic _itself_ is not a useful metatheory.

However, the usual conditional consistency proofs can be formalized in a metatheory consisting of ZF running on ordinary first-order logic. I think PA (also on first-order logic) will also suffice.