Axiom schema of specification (formula arguments)

Solution 1:

You do not need parameters.

Ralf Schindler wrote a short note where you can see the details (and Ralf and I discussed it last year around May). Eventually we found an early reference, that proves an even stronger theorem. See

Azriel Levy, Parameters in the comprehension axiom schemas of set theory, in Proceedings of the Tarski symposium, Proceedings of Symposia in Pure Mathematics, vol. 25, American Mathematical Society, Providence, RI, pp. 309–324.

(See also Akihiro Kanamori's In praise of replacement for further discussion and additional references.)

The theorem in Ralf's note is stronger than you are asking: We can formulate $\mathsf{ZFC}$ without requiring parameters in either comprehension (specification) or replacement.

As you can see, the argument is less than a page long. Let me give a quick summary: Note first that we can prove the existence of $0$ and $1$, and therefore of ordered pairs of the form $(a,0)$ or $(a,1)$ for any $a$. From (an instance of parameter-free) replacement, we get that $a\times\{0\}$ and $a\times\{1\}$ exist for any $a$. Also, for any $a$ and $b$, $(a\times\{0\})\cup\{(b,1)\}$ exists. From this we can prove that $$\{((u,0),(b,1))\mid u\in a\}$$ exists for any $a$ and $b$: First, $d=\mathcal P(\mathcal P((a\times\{0\})\cup\{(b,1)\}))$ exists, and the set we want is $$\{x\in d\mid \exists u\,\exists v\,(x=((u,0),(b,1)))\},$$ which exists by applying an instance of parameter-free specification.

We can now prove specification with parameters. For this, note that using pairing, we can code finitely many parameters into a single one, so it is enough to show the result for formulas with one parameter, say $\phi(x,v)$. That is, given $a,b$, we must show that $$\{x\in a\mid \phi(x,b)\}$$ exists.

We use the parameter-free instance of replacement given by the class function $F$ defined by $F(x)=0$ unless $x$ has the form $((u,0),(c,1))$ for some $u,c$, in which case we set $F(x)=u$. We see that $$ F''\{((u,0),(b,1))\mid u\in a\}= \{x\in a\mid \phi(x,b)\}\cup\{0\}, $$ and from this your question follows (by applying a parameter-free instance of specification to remove $0$ from the set, if needed).

To conclude, we prove replacement for formulas with one parameter (which again, by pairing, is enough). Accordingly, let $\phi(x,y,v)$ be a formula, let $b$ be a set, and suppose that for every $x$ there is a unique $y$ such that $\phi(x,y,b)$. We must show that, for any $a$, $$ \{y\mid\exists x\in a\,(\phi(x,y,b))\} $$ exists.

We use the parameter-free instance of replacement given by the class function $F$ defined by $F(z)=0$ unless there are $x,c$ with $z=((x,0),(c,1))$, and there is a unique $y$ such that $\phi(x,y,c)$ holds, in which case we set $F(z)=y$. We then see that $$ F''\{((x,0),(b,1))\mid x\in a\}=\{y\mid\exists x\in a\,(\phi(x,y,b))\}\cup\{0\} $$ and, as before, we are done by a last appeal to a (parameter-free) instance of specification, if removing $0$ from the set is needed.

Solution 2:

The necessity of the universal quantifiers is an artifact of the fact that in the classical formulations of logic the emphasis falls on propositions that could have truth values assigned to them, and therefore these propositions are necessarily represented by formulas with no free variables. In this set-up, axioms, theorems, etc. are all necessarily propositions, hence represented by formulas with no free variables. Hence, to formulate the axioms in the axiom schema as propositions, you need the universal quantifiers.

In less classical approaches (ones concerned more with the proof calculus like type theory, or category theory), the emphasis falls on hypothetical assertions that something is true. When formulating classical logic, such an assertion may be denoted by $\phi\vdash_{\vec x}\psi$, for example, where $\phi$ and $\psi$ are arbitrary formulas, and $\vec x$ is a list containing all the free variables occurring in $\phi$ and $\psi$. This assertion is to be read as: in the context that the symbols in list $\vec x$ are elements of the universe so that $\phi$ is satisfied, $\psi$ is also satisfied.

This formulation is unnecessary (though I find it convenient) for classical logic, since the assertion $\phi\vdash_{\vec x}\psi$ is, by the inference rule of implication equivalent to $\vdash_{\vec x}\phi\rightarrow\psi$ (in the context $\vec x$, the formula $\phi$ implies $\psi$ is satisfied), which is equivalent from the definition of the universal quantifierto $\vdash\forall\vec x(\phi\rightarrow\psi)$ (where $\forall\vec x$ is an abbreviation for $\forall x_1\forall x_2\forall\dots\forall x_n$ if $\vec x=[x_1,\dots,x_n]$). This assertion says that in the empty context, and with no hypotheses, the (free variable free) formula $\forall\vec x(\phi\rightarrow\psi)$ is satisfied.

(Note, however, that for non-classical logics, or fragments of classical logic for which we are granted only restricted access to quantifiers and connectives, the above equivalence may simply not be available, hence this alternative formulation).

So in particular, in this alterative formulation of classical logic, the assertion $$\vdash_{\vec w}\forall A \, \exists B \, \forall x \, ( x \in B \leftrightarrow [ x \in A \wedge \varphi] )$$ can be taken as an axiom, and is by definition of $\forall$ equivalent to the assertion $$\vdash\forall\vec w(\forall A \, \exists B \, \forall x \, ( x \in B \leftrightarrow [ x \in A \wedge \varphi] $$

Notice that we are still keeping track of the free variables. As far as I understand, you can't not keep track of the free variables, and part of the non-classical approach is that the tracking is built in (since if you want to deal with multi-sorted logic or type theory, you have to keep track not just of which symbols are variables, but also of what sort or types those variables are).

To answer the clarified question, it is simply not true in general that any two-variable formula can be replaced by an infinite family of single-variable formulas. The reason is that elements of the domain are simply not part of the alphabet over which the formulas are defined as strings of symbols. In particular for set theory, formulas are strings of symbols made out of variables ($x,y,z,\dots$), the logical connectives ($\wedge,\vee,\neg,\rightarrow$), the two quantifiers ($\exists,\forall$), parentheses ($(,)$), the equality sign ($=$), and the non-logical relation symbol $\in$.

Notice that not even the empty set, which we informally denote as $\{\}$, occurs as an expression in the above symbols. Rather, if we have a formula $\phi(u)$, and we want to instantiate it with $\{\}$, what we obtain is $\phi_{\{\}}\equiv\left(\forall x\neg(x\in u)\right)\wedge\phi(u)$. Consequently, the only formulas $\phi_z$ for $z$ an element of the domain are those which are definable, i.e. ones which are defined by the derivability (from the axioms) of the truth of a formula $\exists z\left(x\in z\leftrightarrow\phi(x)\right)$ is true where $\phi$ uses only the symbols defined above.

However, since there are countably many formulas, and uncountably many sets (this is a metatheoretical result), replacing $\phi(x,z)$ with $\phi_z(x)$, which you can only do for definable $z$, does not result in the same axiom schema: it results in the weaker schema that concerns only definable sets.