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.