The set of first-order ZF axiom sentences

Work in the external metatheory ZF. Use the pure membership signature with logical equality and the finite-word constructors of Terms and formulas as finite set codes. For any displayed ordinary formula below, its code is obtained by expanding abbreviations and serializing those constructors. In particular $\varphi \leftrightarrow \psi$ means $(\varphi \to \psi )\wedge (\psi \to \varphi )$, implication, disjunction and universal quantification have the earlier primitive expansions, and

$\mathrm{\exists }!w\varphi (w)\text{means}\mathrm{\exists }w(\varphi (w)\wedge \mathrm{\forall }v(\varphi [v\mathrm{/}w]\to v=w)),$

with $v$ the least-index variable absent from $\varphi$ and distinct from $w$. Bounded quantifiers mean $\mathrm{\forall }x\in A\varphi :=\mathrm{\forall }x(x\in A\to \varphi )$ and $\mathrm{\exists }x\in A\varphi :=\mathrm{\exists }x(x\in A\wedge \varphi )$. All bound-variable renamings and substitutions are capture-free. These are finite syntactic operations, not new logical primitives.

Let $T_{\mathrm{Z}\mathrm{F}}$ contain the codes of exactly the following six sentences, together with all instances of the two schemas below. The six sentences are those in The Axiom of Extensionality: $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\forall }z(z\in x\leftrightarrow z\in y)\to x=y)$, The Axiom of Pairing: $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\exists }z\mathrm{\forall }t(t\in z\leftrightarrow (t=x\vee t=y))$, The Axiom of Union: $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow \mathrm{\exists }s(s\in x\wedge z\in s))$, The Axiom of Power Set: $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(\mathrm{\forall }t(t\in z\to t\in x)\to z\in y)$, The Axiom of Infinity: there is a set containing a set with no elements and closed under $y\mapsto y\cup \{y\}$ and The Axiom of Foundation: $\mathrm{\forall }S(\mathrm{\exists }t(t\in S)\to \mathrm{\exists }s(s\in S\wedge \mathrm{\neg }\mathrm{\exists }u(u\in s\wedge u\in S)))$:

$\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\forall }z(z\in x\leftrightarrow z\in y)\to x=y);$

$\mathrm{\forall }x\mathrm{\forall }y\mathrm{\exists }z\mathrm{\forall }t(t\in z\leftrightarrow (t=x\vee t=y));$

$\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow \mathrm{\exists }s(s\in x\wedge z\in s));$

$\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(\mathrm{\forall }t(t\in z\to t\in x)\to z\in y);$

$\mathrm{\exists }I(\mathrm{\exists }e(e\in I\wedge \mathrm{\neg }\mathrm{\exists }t(t\in e))\wedge \mathrm{\forall }y(y\in I\to \mathrm{\exists }s(s\in I\wedge \mathrm{\forall }t(t\in s\leftrightarrow (t\in y\vee t=y)))));$

$\mathrm{\forall }S(\mathrm{\exists }t(t\in S)\to \mathrm{\exists }s(s\in S\wedge \mathrm{\neg }\mathrm{\exists }u(u\in s\wedge u\in S)))\mathrm{.}$

Power Set deliberately has the implication-only form of the published supplier. Infinity deliberately uses von Neumann successor, exactly as in the supplier, rather than the singleton-closure presentation in Moschovakis 1A.5.

For every membership-language formula $\varphi (z,\bar{p})$, choose distinct fresh variables $x,y$ absent from it and include the universal closure of

$\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow (z\in x\wedge \varphi (z,\bar{p})))\mathrm{.}$

This is the Separation schema of The Axiom Schema of Separation: for each formula $\phi$, $\mathrm{\forall }\bar{p}\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow (z\in x\wedge \phi (z,\bar{p})))$, with the input $x$ and all parameters universally quantified. For every $\varphi (z,w,\bar{p})$ choose distinct fresh $A,B$ absent from it and include the universal closure of

$\mathrm{\forall }z(z\in A\to \mathrm{\exists }!w\varphi (z,w,\bar{p}))\to \mathrm{\exists }B\mathrm{\forall }w(w\in B\leftrightarrow \mathrm{\exists }z(z\in A\wedge \varphi (z,w,\bar{p})))\mathrm{.}$

This is the functional-image form of The Axiom Schema of Replacement: for each formula $\phi$, if $\phi$ defines a class function on $A$ then its image on $A$ is a set. Parameters are precisely the other free variables, listed in increasing variable-index order; they may be an empty list. Distinct variables $z,w$ are used for the two designated places. Choose fresh variables by their least available indices, renaming bound occurrences first if necessary. Universal closure binds every remaining free variable in increasing index order. This convention changes only variable names and closure order, and leaves no free parameter in an axiom sentence.

The alphabet is explicitly countable, and Canonical natural-number codes for countable Henkin syntax supplies an injection of its sentence set into $\omega$. Schema membership and these finite transformations are set-definable, so Separation on the set of sentence codes (equivalently Replacement over the set of admissible formulas and designated variable lists) forms $T_{\mathrm{Z}\mathrm{F}}$ as a set. It is a sentence theory, not a class-sized collection. AC is excluded. No consistency, set-model existence, transitivity or external well-foundedness of models is asserted.

Conventions and prerequisites: The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations, Free variables and free-for substitution.