# Does ZF prove that a finite subtheory axiomatizes it over transitive proper class models?

If $\text{ZF}$ is consistent, then it is not finitely axiomatizable. For if $\Gamma$ is a finite axiomatization, then $\text{ZF}$ proves by reflection that $\Gamma$ has a set model, and hence (since $\Gamma$ axiomatizes $\text{ZF}$) so does $\Gamma$. By the Second Incompleteness Theorem, $\Gamma$ is inconsistent. This is absurd, since it axiomatizes $\text{ZF}$.

The following therefore intrigues.

Theorem. There is a finite $\Gamma \subseteq \text{ZF}$ such that every transitive proper class model of $\Gamma$ verifies $\text{ZF}$.

I wish to know whether any obstacle prevents formalizing this in $\text{ZF}$. If not, how does that bear on the aforementioned theorem about finite axiomatizability?

For instance, if formalization is possible, it seems to follow that $\text{ZF}$ proves that, if $\text{ZF}$ is consistent, then $\Gamma$ has a model refuting $\text{ZF}$. Else "every model of $\Gamma$ verifies $\text{ZF}$" is consistent with $\text{ZF + Con(ZF)}$, which is absurd since the joint theory proves that $\text{ZF}$ both is and isn't finitely axiomatizable. But that's not very interesting. Perhaps the theorem implies something about nonfirstorderizability of transitivity? Do tell!

Here is a proof, the length of which merits apology. Seems formalizable to me!

Proof. We specify $\Gamma$ in stages. First let it contain all axioms of $\text{ZF}$ besides Comprehension and Replacement. Next let $\Gamma$ contain the finitely many instances of Comprehension and Replacement needed, in addition to the above, to prove the facts invoked below about absoluteness and the cumulative hierarchy. Following Kunen, let $\text{En}(i,X,j)$ be the set of $j$-tuples from $X$ satisfying the $i$th formula in $j$ variables, relativized to $X$. Where $\ast$ denotes concatenation, write $\eta(m,n,s,t,A,B)$ for

$m, n \in \omega \wedge t \in B \wedge A \in B \wedge s \in B^n \wedge s\ast\langle t, A \rangle \in \text{En}(m, B, n+2)$

and $\mu(m,n,s,t,A,B,y)$ for

$m, n \in \omega \wedge t \in B \wedge A \in B \wedge s \in B^n \wedge y \in B \wedge s\ast\langle t, y, A \rangle \in \text{En}(m, B, n+3).$

Finally, let $\Gamma$ contain the instance (+)

$\forall m,n,s,A,B\ \exists y\ \forall t\ [t \in y \leftrightarrow t \in A \wedge \eta(m,n,s,t,A,B)].$

of Comprehension, and the instance (++)

$\forall m,n,s,A,B[\forall t \in A\ \exists!y\ \mu(m,n,s,t,A,B,y) \rightarrow \exists Y\ \forall t \in A\ \exists y \in Y\ \mu(m,n,s,t,A,B,y)]$

of Replacement. Let nothing else be in $\Gamma$.

Now suppose $M$ is a transitive proper class model of $\Gamma$. To prove that $M$ verifies $\text{ZF}$, it suffices to check that it verifies arbitrary instances of Comprehension and Replacement. We do the former; the latter is similar, using (++) in place of (+). Let $\theta(w_1, \dots, w_n, t, A)$ be a formula, and take sets $w_1, \dots, w_n, A$ in $M$. By Comprehension in $V$, let $a$ be the set of all $t \in A$ such that $\theta^M(w_1, \dots, w_n, t, A)$. We aim to show that $a$ is an element of $M$.

Since $M$ is transitive and contains $A$, $a$ is a subset of $M$. And since $M$ verifies $\Gamma$, the tuple $s = \langle w_1, \dots, w_n \rangle$ is in $M$. Define a cumulative hierarchy on $M$ by setting $M_\alpha = M \cap V_\alpha$. By the reflection theorem, take $\beta > \text{max rank}(a, A, s, \omega)$ such that $\theta$ and $\Gamma$ are absolute for $M_\beta$, $M$. Now $M_\beta$ is a transitive model of $\Gamma$ containing $w_1, \dots, w_n, A, s, \omega$, and each element of $a$. Moreover, $M_\beta \in M$, since $M$ thinks $V_\beta$ exists.

By definition of $\text{En}$ there is an integer $q$, the Gödel number of $\theta$, such that $\text{En}(q, M_\beta, n+2)$ is the set of (n+2)-tuple from $M_\beta$ satisfying $\theta^{M_\beta}$. Using (+) in $M$ with $m = q$ and $B = M_\beta$, and computing relativizations and absoluteness with the aid of $\Gamma$, there is $y \in M$ containing precisely the $t \in M$ such that $t \in A \wedge \theta^{M_\beta}(w_1, \dots, w_n, t, A)$. Since $a$ is a subset of $M_\beta$ and $\theta$ is absolute for $M_\beta$, $M$, this $y$ is just $a$. So $a$ is in $M$, as desired.

QED

By the way, the theorem is Exercise 7 in Chapter V of Kunen.

-
I only got to the second sentence of the question so far, but, assuming only that $\Gamma$ axiomatizes ZF, how do you know that ZF sees that $\Gamma$ axiomatizes ZF? It seems clearer to me to modify the argument in your first paragraph to avoid this issue. Since ZF proves that $\Gamma$ has a set model, so does $\Gamma$, and therefore $\Gamma$ proves its own consistency and must be inconsistent. Since $\Gamma$ axiomatizes ZF, it would follow that ZF is inconsistent. –  Andreas Blass Aug 28 '11 at 22:09
To clarify my previous comment: I realize that, for each individual axiom $\alpha$ of ZF, ZF would see that $\Gamma$ proves $\alpha$. But that's not the same as seeing the single sentence "$\Gamma$ axiomatizes ZF", and I think your argument uses the latter, stronger seeing. –  Andreas Blass Aug 28 '11 at 22:15
Good point, Andreas. I assumed that, since $\Gamma$ and $\text{ZF}$ are computably enumerable, there are predicates $A$ and $B$ representing them in $\text{ZF}$ such that $\text{ZF}$ proves "Every $B$ has an $A$-proof." Then, I thought, $\text{ZF}$ must prove $\text{Con(B)}$ since it proves $\text{Con(A)}$. Is that right? In any case, I like your argument better, so I'll edit the question. –  Cole Leahy Aug 29 '11 at 17:32
If ZF proves the sentence that formalizes "Every axiom of ZF is provable from $\Gamma$" then there's no problem. But the $\Pi^0_2$ sentence in quotation marks here might be true without being provable in ZF. In that case, $\Gamma$ would axiomatize ZF but ZF wouldn't know it. –  Andreas Blass Aug 29 '11 at 22:32
What extra hypotheses would ensure that $\Gamma$ does prove the quoted sentence? –  Cole Leahy Aug 29 '11 at 23:45

To see this, observe first that the theorem you state is actually merely a theorem scheme, asserting of any axiom $\varphi$ of ZFC that any proper class model of $\Gamma$ is also a model of $\varphi$. That is, the theorem proves each instance of ZFC separately to hold in the given class $M$, if it satisfies $\Gamma$. The proof you give appeals at a critical stage to the Reflection theorem, which is also merely a theorem scheme, and this is why we cannot amalgamate the whole argument as one internal induction. Rather, the way to think about it is that the theorem is proved by an induction that takes place in the meta-theory, establishing each meta-theoretical axiom of ZFC to hold in $M$ as a separate claim. Thus, we only conclude that the standard (meta-theoretic) axioms of ZFC hold in $M$, and we may not deduce that $V$ thinks that $M$ satisfies the internal version of ZFC, using the formulas having Gödel codes in $V$. Indeed, because of Tarski's theorem on the non-definability of truth, we have in general no way to express that a given formula coded by a Gödel code is true in a given class, and so no way even to express that a class $M$ satisfies all of (the internal) ZFC, as opposed to expressing this as a scheme.
Thanks, as usual. Now I see that the theorem and proof are schemes. But each instance of the proof can be formalized, so that ZF proves the formalization of "$M$ verifies $\phi$", whenever $M$ is a transitive proper class model of $\Gamma$ and $\phi$ an axiom of ZF. Right? Suppose we add a satisfaction predicate to the language. Does the schematic nature of the reflection theorem still thwart a unified formal theorem? If not, and if satisfaction can be added conservatively, does this get us close to contradicting the theorem that ZF isn't finitely axiomatizable? –  Cole Leahy Aug 28 '11 at 0:25
So in MK one can prove both: (a) no finite theory $\Delta$ has $\text{Mod}(\Delta) = \text{Mod}(\text{ZF})$; and (b) for the $\Gamma$ defined in the question, $\text{Mod}(\Gamma)$ restricted to transitive proper classes equals $\text{Mod}(\text{ZF})$ restricted to transitive proper classes? –  Cole Leahy Aug 28 '11 at 1:11