ZF has an effective standard arithmetic interpretation

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 def-set-coded-terms-and-formulas. 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 def-axiom-of-extensionality, def-axiom-of-pairing, def-axiom-of-union, def-axiom-of-power-set, def-axiom-of-infinity and def-axiom-of-foundation:

$\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 def-axiom-schema-of-separation, 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 def-axiom-schema-of-replacement. 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 lem-countable-henkin-syntax-coding 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: def-language-of-set-theory, def-free-variables-and-syntactic-substitution.

Primitive-recursive syntax and certified proof checking: For the fixed effective signature and sentinel encoding, term/formula recognition, free-variable and free-for tests, capture-free substitution, numeral formation, negation, and certified derivation checking are primitive recursive. Invalid inputs return zero or false.

The recursion theorem: Let $(N,0,\sigma )$ be a Peano system (def-peano-system), in particular the natural numbers $\mathbb{N}$ (def-natural-numbers). For any set $A$, any element $a\in A$, and any function $f:A\to A$, there is a unique function $g:N\to A$ such that $g(0)=a$ and $g(\sigma (n))=f(g(n))$ for all $n\in N$.

Interpretations with proof-translation data: An interpretation of a sentence theory S in T specifies formulas D(x) and E(x,y), invariant relation formulas, and functional graph formulas. T proves D nonempty, E an equivalence on D, invariance under E of all relations and graphs, and totality and uniqueness modulo E of each function graph on domain-valued inputs. Fixed parameters are target constants. No other free variables occur in the interpretation data.

Define a domain-valued term graph by $V_x(z):=D(z)\wedge E(x,z)$ and $V_{f(\bar{t})}(z):=D(z)\wedge \mathrm{\exists }\bar{u}({\bigwedge }_i{V}_{t_i}(u_i)\wedge F_f(\bar{u},z))$; the nullary case uses the constant graph. Atomic relations and equality quantify term values and then apply the interpreted relation or E. Translation commutes with negation/conjunction and replaces $\mathrm{\exists }x\varphi$ by $\mathrm{\exists }x(D(x)\wedge {\varphi }^I)$, always using fresh bound variables. T must prove every translated source axiom.

For a source formula $\varphi$ put $G_{\mathrm{F}\mathrm{V}(\varphi )}={\bigwedge }_{v\in \mathrm{F}\mathrm{V}(\varphi )}D(v)$. Its guarded proof translation is $G_{\mathrm{F}\mathrm{V}(\varphi )}\to {\varphi }^I$. For sentences the empty guard is a fixed tautology. Effective certificate data provides the required target certificates effectively. Formalized data additionally provides a base-verifiable total primitive-recursive map on proof codes; effectiveness alone does not assert that stronger property.

Use def-set-coded-formal-derivation for the calculus and lem-primitive-recursive-syntax-and-proof-checking for the finite numerical operations. Logical theorem preservation is a conclusion of the next lemma, not an interpretation axiom. No quotient representatives or choice function are specified.

The principle of mathematical induction: Let $S\subseteq \mathbb{N}$. If $0\in S$ and $\sigma (n)\in S$ whenever $n\in S$, then $S=\mathbb{N}$. Equivalently (property form): if a property $P$ satisfies $P(0)$ and ($P(n)\Rightarrow P(\sigma (n))$) for all $n$, then $P(n)$ holds for all $n\in \mathbb{N}$. This is the induction principle, the basis of proof by induction.

Robinson arithmetic, PA, and numeral conventions: Use the arithmetic signature $0,S,+,\cdot ,=$. Robinson arithmetic $Q$ consists of the universal closures of these seven formulas:

$Sx\mathrm{\ne }0;Sx=Sy\to x=y;x\mathrm{\ne }0\to \mathrm{\exists }yx=Sy;$ $x+0=x;x+Sy=S(x+y);x\cdot 0=0;x\cdot Sy=x\cdot y+x\mathrm{.}$

PA adds, for every formula $\varphi (x,\bar{z})$, the universal closure of $[\varphi (0,\bar{z})\wedge \mathrm{\forall }x(\varphi (x,\bar{z})\to \varphi (Sx,\bar{z}))]\to \mathrm{\forall }x\varphi (x,\bar{z})$. Parameters $\bar{z}$ are allowed. No induction schema is included in $Q$.

For an external natural number $n$, its numeral is the term $\bar{n}=S^{n}0$. Define $x\le y$ by $\mathrm{\exists }z(z+x=y)$ and $x<y$ by $x\le y\wedge x\mathrm{\ne }y$, with $z$ fresh. The left-addend witness is intentional: commutativity is not an axiom of Q.

Use def-set-coded-formal-derivation for the six logical schemes and three rules. Negation, conjunction and existential quantification are primitive: $A\to B$ expands to $\mathrm{\neg }(A\wedge \mathrm{\neg }B)$, $A\vee B$ to $\mathrm{\neg }(\mathrm{\neg }A\wedge \mathrm{\neg }B)$, and $\mathrm{\forall }xA$ to $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }A$. Inequality means negated equality. Substitute capture-free, always taking the least available fresh variable index and universally closing the remaining parameters in increasing index order. Thus each displayed axiom and each induction instance is a definite finite sentence.

Derivability conditions for the chosen proof predicate: For the standard certified predicate of an effective T extending PA, the following hold for sentences $\varphi ,\psi$: D1, if $T⊢\varphi$ then $T⊢{\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)$; D2, T proves ${\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi \to \psi <mi\; mathvariant="normal">⌝</mi>)\to ({\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\psi <mi\; mathvariant="normal">⌝</mi>))$; D3, T proves ${\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>{\mathrm{Prov}}_T(<mi\; mathvariant="normal">⌜</mi>\varphi <mi\; mathvariant="normal">⌝</mi>)<mi\; mathvariant="normal">⌝</mi>)$. The interpreted version requires an effective PA copy and verification there of the arithmetic proof constructors and axiom-proof translations used below.