# Explanation - Free Term definition

Definition: Free Term

A term $t$ is free for $x_i$ if $x_i$ does not occur free within the scope of any quantifier ($\forall x_j$) where $x_j$ is a variable that enters $t$.

I extremely difficult to understand the definition. For those who have experience in logic, is it possible to clearly explain what the definition means?

An example could be $((\forall x_2) A^1_1(f^1_1(x_2)) \to (\forall x_3)A^3_1(x_1, x_2, x_3))$. $t_1 = f_1^2(x_1, x_2)$ is free for $x_1$ because $x_1$ doesn't occur in the scope of $(\forall x_1)$ and $(\forall x_2)$. $t_2= x_3$ is not free for $x_1$ because $x_1$ occurs free in the scope of $(\forall x_3)$. Answer given by the teacher

An other example could be $((\forall x_2) A^2_1(x_2,f^2_1(x_1,x_2)) \to A^1_1(x_1))$. $t_1 = f_1^2(x_1, x_2)$ doesn't free for $x_1$ because $x_1$ occurs free in the scope of $(\forall x_2)$ Answer given by the teacher

## 2 Answers

Example

Consider the formula :

$\mathcal A := \exists y \ \lnot \ (y = x)$

and consider the term $t:=y$.

What happens if we try to perform the substitution "$t$ in place of $x$" :

$\mathcal A [x \leftarrow t]$ ?

The result is : $\exists y \ \lnot \ (y = y)$, that is not what we expected.

The idea behind the definition of :

"a term $t$ being free for $x$" or “$t$ to be substitutable for $x$” in a formula $\mathcal A$,

is that a "correct" replacement of a free variable $x$ in the formula $\mathcal A$ with a new term $t$ must avoid that some variable $y$ occurring in $t$ being "captured", upon substitution, by some quantifier $\forall y$ or $\exists y$ already present in $\mathcal A$, thus distorting the original meaning of the formula.

More precisely, "$t$ is free for $x_i$ in a formula $A$". It's not really meaningful without reference to a particular formula.

It means that $t$ can be substituted for $x_i$ in $A$ without danger of any of its ($t$'s) variables being captured by quantifiers within $A$.

In the first example, you (or your teacher) mean to say "$x_1$ doesn't occur in the scope of $(\forall x_2)$ and $(\forall x_3)$, and therefore $t_1$ is free for $x_1$ in the formula but $t_2$ is not because $x_3$ would get captured by $(\forall x_3)$ when substituting into the subformula which that quantifier governs.

The second example is fine.