Fix some reasonable computable enumeration of the axioms of ZFC, and let $ZFC_n$ be the theory consisting of the first n axioms.

Is it the case that, for each natural number n, and each sentence $\phi$, ZFC proves the sentence

$(ZFC_n \vdash \phi ) \rightarrow \phi$?

(Where we formalize provability in ZFC in some reasonable way.)

Please note that this is distinct from asking whether ZFC proves

$\forall n \forall \phi \ : \ (ZFC_n \vdash \phi ) \rightarrow \phi$

(Which ZFC trivially does not, if it is consistent.)

  • $\begingroup$ Yes, this is true. The proof is basically a variation of the proof of the reflection theorem, that $\mathsf{ZFC}$ proves the consistency of each of its finite fragments. (I'm adding this as a comment rather than an answer since that variation isn't immediate; if I can find the time later I'll write an answer with the prof.) Amusingly, this argument is internal to $\mathsf{ZFC}$! That is, $\mathsf{ZFC}$ proves "$\mathsf{ZFC}$ proves the soundness of each of its finite fragments." $\endgroup$ Nov 1 '20 at 20:48
  • $\begingroup$ Of course, this is again different from $\mathsf{ZFC}$ proving "each of $\mathsf{ZFC}$'s finite fragments is sound," which $\mathsf{ZFC}$ can't do unless it's inconsistent. $\endgroup$ Nov 1 '20 at 20:51
  • $\begingroup$ @Noah thanks for the reply. I would def be interested to see the nontrivial adaptation of the RT proof. I had come to believe that the statement was true, and had tried to prove it without doing "real work" (as a simple corollary of various theorems) but was unable to. $\endgroup$ Nov 2 '20 at 0:18

Consider any finite list $\Phi$ of axioms of ZFC and any other sentence $\phi$. By the Lévy-Montague reflection theorem, there is some rank-initial segment $V_\theta$ of the universe for which all the sentences in $\Phi$ and also $\phi$ are absolute between $V_\theta$ and $V$. Since the sentences of $\Phi$ are part of ZFC, they are true in $V$ and hence also in $V_\theta$. In particular, $V$ looks upon $V_\theta$ as a model of $\Phi$, according to the truth predicate that it can define for this set structure. Therefore, if $V$ thinks that $\Phi\vdash\phi$, then it will think that $V_\theta\models\phi$. Since $\theta$ was chosen so that this sentence is absolute, this implies $\phi$ holds in $V$, as desired. So we've established any instance of the implication.

As you noted in the question, we get this implication only as a scheme, a separate statement for each instance, because we have the reflection theorem also only as a scheme.

Addendum. Let me explain that one can also strengthen the conclusion somewhat, by assuming not that the sentences of $\Phi$ are part of ZFC, but rather merely that they are true. In other words, I claim that ZFC proves every instance of the scheme: $$(\psi\vdash\phi)\to(\psi\to\phi).$$ If we take $\psi$ to be the conjunction of the sentences in $\Phi$, this generalizes your scheme. But the same proof works here. By the Lévy-Montague reflection theorem, there is $V_\theta$ for which both $\psi$ and $\phi$ are absolute between $V_\theta$ and $V$. Now, if $\psi\vdash\phi$ and $\psi$ is true (in $V$), then $\psi$ is true in $V_\theta$, and so $\phi$ also is true there, and so $\phi$ is true in $V$, as desired.

  • $\begingroup$ Thanks JDH. I had come up with something similar, but got confused because I thought this argument only showed that $\phi$ is true in V, and not that ZFC proves $\phi$ from the assumption $ZFC_n \vdash \phi$. But now I realize that ZFC actually proves $(V_\theta \models \phi) \leftrightarrow \phi$, and also $(ZFC_n \vdash \phi) \rightarrow (V_\theta \models ZFC_n \ \rightarrow \ V_\theta \models \phi)$. $\endgroup$ Nov 2 '20 at 14:01
  • $\begingroup$ I watched your great YouTube courses recently and asked a question regarding first-order logic: math.stackexchange.com/q/3983971. I would greatly appreciate you could take a look at that. $\endgroup$
    – user9464
    Jan 13 at 20:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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