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



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.


Your Answer

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