Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
up vote 4 down vote accepted

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.

share|cite|improve this answer
Well it may not be very useful from a practical perspective, but my question is about the existence of a proof, not about practical convenience. For instance, suppose we have a proof of the conditional independence of CH from ZFC in the system PA. Can we use this proof to obtain a proof in the system FOL? – goblin Feb 5 '13 at 3:24
@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
Oh. I see. Is PA the "minimal" metatheory in which the conditional independence of (say) CH from ZFC can be expressed? – goblin Feb 5 '13 at 6:11
@user18921: PA cannot be minimal, because it is not finitely axiomatized. If you prove your result from PA, the proof will use a finite subset of the axioms, and the theory consisting of that finite subset will be smaller than PA but still able to prove the result. – Henning Makholm Feb 5 '13 at 10:50
Makes sense. Can you recommend an easy introductory book about consistency, independence etc. – goblin Feb 5 '13 at 12:06

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.