# What is lost if we completely exclude free variables from ZFC?

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?

• No difference; in mathematics, when we asserts a formula, like e.g $x+y=y+x$, we assume that the free vars are implicitly universally quantified. Thus, Axiom of Separation $∃y∀x(x∈y ⟷ (x∈z \land \varphi))$ must be read as $∀z∃y∀x(x∈y⟷(x∈z \land \varphi))$. Oct 4 '18 at 10:51
• @bof It is not an axiom it is an axiom scheme. That is an axiom for each possible formula φ. Oct 4 '18 at 10:54
• @bof Right. I will edit it. Oct 4 '18 at 11:05
• I hope you do appreciate that you need to use formulas with free variables to carry out proofs in the standard presentations of first-order logic. However the inputs (axioms) and outputs (theorems) of proofs can always have their free variables quantified without making any significant difference. Oct 4 '18 at 19:43
• @RobArthan No, I don't. Can you explain it? Can you give an example? Oct 5 '18 at 3:48