Lost if we completely exclude free variables from ZFC

logicset-theory

Just as an example, in some places the Axiom Schema of Comprehension is formulated with a free variable for example Kunen:

Axiom 3. Comprehension Scheme. For each formula, φ, without y free,
$\exists y \forall x (x \in y \longleftrightarrow x \in z \land \phi(x))$

In other places such as Wikipedia and Hrbacek, Jech formulates it without free variables:

The Axiom Schema of Comprehension: Let P(x) be a property of x. For
any set A, there is a set B such that x ∈ B if and only if x ∈ A and P(x).

There is a difference in what can be deduced inside ZFC (I mean without using model theory or semantic resources) between

$\exists y \forall x (x \in y \longleftrightarrow x \in z \land \phi(x))$

and

$\forall z \exists y \forall x (x \in y \longleftrightarrow x \in z \land \phi(x))$ ?

In general, What is lost if we completely exclude free variables from ZFC?

I know that "There is nothing specific in 𝖹𝖥𝖢 regarding free variables" but we can build a ZFC theory where all formulas are closed. What limitation may have that theory?

Best Answer

In fact Kunen's book has all the axioms as closed formulas: in both Axiom 3 (Comprehension) and Axiom 6 (Replacement) it says "the universal closure of the following is an axiom"; the other axioms are all single closed formulas.

Related Question