What is the purpose of free variables in first order logic?

Question

I understand the difference between free and bound variables, but what are free variables actually useful for? Can't you use quantifiers to express everything that you would want to express with both bound and free variables? I am a little frustrated that the ever-present possibility of free variables complicates introducing quantifiers into FOL statements, while I can't find any motivation for the free variables.

Say you have a relation $R$, arity $2$. If you want to express that, for every x and for every y, $R(x,y)$, I guess you would write:

$$\forall_x\forall_yR(x,y)$$

Maybe you could also formulate this as:

$$R(x,y)$$

Since it seems that in order for this to be a valid proposition in FOL, you would have to capture all free variables with a universal quantifier. But this means that formulae with free variables are equivalent to closed formulae where these free variables have been captured by universal quantifiers, if you want to find out the validity of that formula. So what is the purpose of free variables when it comes to proving formulae in FOL?

Answer 1

Consider the informal argument 'Everyone loves pizza. Anyone who loves pizza loves ice-cream. So everyone loves ice-cream.' Why is that valid?

Roughly: Pick someone, whoever you like. Then, s/he loves pizza. And so s/he loves ice-cream. But sh/e was arbitrarily chosen. So everyone loves ice-cream.

This informal argument can be spelt out with plodding laboriousness with explicit commentary like this:

1. Everyone loves pizza. (That's given)

2. Anyone who loves pizza loves ice-cream. (That's given too)

3. Take some arbitrary person, call her Alice. Then Alice loves pizza (From 1)

4. If Alice loves pizza, she loves ice-cream (From 2)

5. Alice loves ice-cream (From 3, 4, by modus ponens)

6. But Alice was an arbitrary representative person, so what applies to her applies to anyone: so everyone loves ice-cream.

Now consider the formal analogue of this proof (using $F$ for 'loves pizza" etc.)

1. $\forall xFx\quad\quad\quad\quad$ Premiss

2. $\forall x(Fx \to Gx)\quad$ Premiss

3. $Fa\quad\quad\quad\quad\quad$ From 1., Univ. Instantiation

4. $(Fa \to Ga)\quad\quad$ From 2., Univ. Instantiation

5. $Ga\quad\quad\quad\quad\quad$ From 3, 4 by MP

6. $\forall xGx\quad\quad\quad\quad$ From 5, Univ. Generalization

(UG on $a$ is legimitate as $a$ appears in no assumption on which (5) depends, so can be thought of as indicating an arbitrary representative member of the domain.)

So note, that we need here some symbol playing the role of $a$, not a true constant with a fixed interpretation, not a bound variable, but (as common jargon has it) a parameter which stands in, in some sense, for an arbitrary element of the domaain.

Now, in some syntaxes, variables $x$, $y$ etc. only ever appear bound, as part of quantified sentences. And parameters are typographically quite distinct, $a$ and $b$, etc. This is the usage in Gentzen, for example.

But another tradition (probably more common, but not for that reason to be preferred), we are typographically economical, and re-cycle the same letters as both true variables and as parameters. In other words, we allow the same letters to appear both as "bound" variables and as "free" variables. Then the formal proof will look like this:

1. $\forall xFx\quad\quad\quad\quad$ Premiss

2. $\forall x(Fx \to Gx)\quad$ Premiss

3. $Fx\quad\quad\quad\quad\quad$ From 1., Univ. Instantiation

4. $(Fx \to Gx)\quad\quad$ From 2., Univ. Instantiation

5. $Gx\quad\quad\quad\quad\quad$ From 3, 4 by MP

6. $\forall xGx\quad\quad\quad\quad$ From 5, Univ. Generalization

This is a superficial difference, however: the role of the free (unbound) variable is as a parameter. And we've seen, even in informal arguments, we use expressions like "s/he" or even "Alice" as parameters. Looked at in that light, there should be no mystery about why we need parameters in a formal logic too. And in one syntax, unbound variables play the role of parameters.

Answer 2

"What the difference between a free variable and the usage of $∃x$ ? I mean, isn't $∃x$ the same as some random variable?"

So the issue is:

"What are free variables actually useful for ?"

I think that it may be usefulto start from:

"What are quantifiers useful for ?"

Consider an example from elementary algebra :

$(x + y)^2 = x^2 + 2xy + y^2$.

Usually, we do not use quantifiers to state this "law", but it is implicitly universally quantified; i.e. tha "intended" meaning of the law is :

for every two numbers $x$ and $y$, the above identity holds; i.e.

$\forall x \ \forall y \ [(x + y)^2 = x^2 + 2xy + y^2]$.

Thus, we may think that, in the usual mathematical practice, we may dispense with the universal quantifier.

But we can consider a different algebraic example:

$x^2-2x +1=0$.

In this case we are not asserting that the equation holds for all values of $x$.

When we ask for the solutions (if any) of equations, we are asking if the existential quantification of the equation holds, i.e. if

$\exists x \ (x^2-2x +1=0)$.

The conclusion is that free variables in "usual" mathematical contexts can be treated as implicitly universally quantified.

In other words, it is not possible to express all the "interesting" facts we want to express simply with universal quantifiers upfront.

---

About:

"$\exists x$ is the same as some random variable",

we have that the existential quantifier is needed in order to express the fact that in a certain "domain of discourse" there are some objects (at least one) which satisfy a certain property.

For example, we have that in the domain $\mathbb N$ of natural numebrs, there is an object (a number) which satisfy the identity : $x = 0$. Precisely, the number $0$.

Thus, we are licensed to state the following true fact about $\mathbb N$ :

$\exists x \ (x = 0)$.

Of course, bound variables can be replaced without changing the meaning of the formula; thus we can write: $\exists y \ (y = 0)$, and the two formulae express the same fact about $\mathbb N$.

But we have to take care of "interactions" between quantifiers; we cannot start from $\exists x \ (x = 0)$, "existentially instantiate" it (incorrectly) to derive e.g. $(y = 0)$ and then apply UG to conclude with: $\forall y \ (y = 0)$, that is clearly false.

This kind of details are formalized with the rules of the proof system, and different "styles" of proof system can differ on the details, but all must formalize our "intuitive" understanding of what typs of inference are "correct".

Peter Smith's answer above gives a beautiful explanation of the role of free variables in first-order logic proofs.

Answer 3

Categorical logic implies a very natural way to think of free variables: they're just another kind of element.

There is a notion of a "generalized element" of an object $X$ in a category, which is simply any morphism whose codomain is $X$. Ordinary elements of sets can be viewed as generalized elements, by identifying an element $a \in X$ with the function

$$ f : \{ \varnothing \} \to X : \varnothing \mapsto a $$

The identity map on $X$, interpreted as a generalized element, turns out to be an excellent way to capture the notion of an "indeterminate variable" or a "generic element".

When we have a collection of free variables $x_1, \ldots, x_n$ of our domain of discourse, and we make an interpretation into the set $U$, we interpret them as the generalized elements corresponding to the projection maps $U^n \to U$.

We can correspondingly interpret the relation $R$ as being a particular map

$$ R : U^2 \to \{ \text{true}, \text{false} \} $$

and $R(x,y)$ is the corresponding generalized element of $\{ \text{true}, \text{false} \}$.

Answer 4

If one does not consider formulas with free variables, then one cannot write a proof by induction on the formation of formulas. Every first-order formula is constructed from primitive formulas by either putting a quantifier in front of a formula with a free variable, thereby binding the variable, or applying operations like "and", "or", "not", "if...then...", etc., to other formulas. In the inductive step in a proof by induction you show that if the thing you're trying to prove is true of two formulas $A$ and $B$ then it's true of $[A\text{ or }B]$ and it's true of $\exists x\ B$, and so on.

Łos's theorem says that if a first-order statement is true in "almost every" factor in an ultraproduct, then it's true in the ultraproduct. Łos's theorem is proved by induction on the formation of first-order formulas.