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

-

@user18921: My point is that you can't even express the properties you're speaking about in pure FOL without any proper axioms. Proving them is completely moot, then. You might be able to cheat and represent a computable function by, say, $Q\to \phi(x,y)$ where $Q$ is the conjunction of the finitely many axioms of Robinson arithmetic and $\phi(x,y)$ is the standard arithmetical representation of the function in question -- but then you're not really working in raw FOL anyway; you're just working in Q while pretending you're not. (Or the same for NBG set theory instead of Q). –  Henning Makholm Feb 5 '13 at 3:32