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.