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))$


$\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?

  • 3
    $\begingroup$ 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))$. $\endgroup$ Oct 4 '18 at 10:51
  • $\begingroup$ @bof It is not an axiom it is an axiom scheme. That is an axiom for each possible formula φ. $\endgroup$ Oct 4 '18 at 10:54
  • $\begingroup$ @bof Right. I will edit it. $\endgroup$ Oct 4 '18 at 11:05
  • $\begingroup$ 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. $\endgroup$
    – Rob Arthan
    Oct 4 '18 at 19:43
  • $\begingroup$ @RobArthan No, I don't. Can you explain it? Can you give an example? $\endgroup$ Oct 5 '18 at 3:48

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.

  • 1
    $\begingroup$ So there is not any formal lost getting rid free variable from ZFC, it is just a matter of presentation. Right? $\endgroup$ Oct 4 '18 at 11:02
  • $\begingroup$ Indeed, in Mendelson's Introduction to Mathematical Logic both forms would be formally deducible from each other. $\endgroup$
    – hartkp
    Oct 4 '18 at 11:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.