Actions

Free variables

From Learning Logic for Computer Science

The free variables in a first-order formula are the ones which are important in the sense that the interpretation of the formula under an assignment depends (at most) on the values of these variables. This has also consequences when it comes to term substitution.

Example In the formula $\exists x_0 (f(x_0) \doteq x_1)$ the truth value of the formula under an assignment (in a given structure) does not depend on the value of $x_0$, because every occurrence of $x_0$ is in the scope of a quantification of $x_0$, but it very much depends on the value of $x_1$.

Example A more complicated example is $\exists x_0 f(x_0) \doteq x_1 \wedge x_0 \doteq g(x_1)$. Here, there are two occurrences of $x_0$: the first one is in the scope of a quantification, but the second one is not. So the truth value of the formula depends on the values of $x_0$ and $x_1$.

The last example shows that it is good to distinguish the different occurrences of a variable.

Definition The set of variables occurring free in a first-order formula $\varphi$, denoted $\text{fvars}(\varphi)$, is defined inductively.

Let $\mathcal S$ be any signature.

Base mapping.

  • $\text{fvars}(\top) = \emptyset$ and $\text{fvars}(\bot) = \emptyset$.
  • For all $\mathcal S$-terms $t_0$ and $t_1$, $\text{fvars}(t_0 \doteq t_1) = \text{vars}(t_0) \cup \text{vars}(t_1)$.
  • For all relation symbols $R/n \in \mathcal S$ and $\mathcal S$-terms $t_0, \dots, t_{n-1}$, $\text{fvars}(R(t_0, \dots, t_{n-1})) = \bigcup_{i < n} \text{vars}(t_i)$.

Inductive rule.

  • For every $n$-ary connective $C$ and all $\mathcal S$-formulas $\varphi_0, \dots, \varphi_{n-1}$, $\text{fvars}(C(\varphi_0, \dots, \varphi_{n-1})) = \bigcup_{i < n} \text{fvars}(\varphi_i)$.
  • For every $i \in \mathbf N$ and all $\mathcal S$-formulas $\varphi$, $\text{fvars}(\exists x_i \varphi) = \text{fvars}(\varphi) \setminus \{x_i\}$ and $\text{fvars}(\forall x_i \varphi) = \text{fvars}(\varphi) \setminus \{x_i\}$.

Example \begin{align*} \text{fvars}(\exists x_0 f(x_0) \doteq x_1 \wedge x_0 \doteq g(x_1)) & = \text{fvars}(\exists x_0 f(x_0) \doteq x_1) \cup \text{fvars}(x_0 \doteq g(x_1)) && \text{inductive step, 1st item}\\ & = \text{fvars}(f(x_0) \doteq x_1) \setminus \{x_0\} \cup \text{vars}(x_0) \cup \text{vars}(g(x_1)) && \text{base mapping, 2nd item; inductive step, 2nd item}\\ & = (\text{vars}(f(x_0)) \cup \text{vars}(x_1)) \setminus \{x_0\} \cup \text{vars}(x_0) \cup \text{vars}(g(x_1)) && \text{base mapping, 2nd item}\\ & = (\{x_0\} \cup \{x_1\}) \setminus \{x_0\} \cup \{x_0\} \cup \{x_1\} && \text{}\\ & = \{x_0, x_1\} && \text{properties of set operations}\\ \end{align*}

Example Consider the formula $\varphi$ defined by $\varphi = \exists x_0 f(x_0) \doteq x_1 \wedge x_0 \doteq g(x_1)$. If one wants to know what happens when $x_1$ takes on the value of a constant symbol $c$, then, clearly, one considers the formula $\exists x_0 f(x_0) \doteq c \wedge x_0 \doteq g(c)$.

If, on the other hand, one wants to know what happens when $x_0$ takes on the value of a constant symbol $c$, then the first occurrence of $x_0$ is irrelevant, only the second one is relevant. More precisely, one considers the formula $\exists x_0 f(x_0) \doteq x_1 \wedge c \doteq g(x_1)$.

This is discussed in full generality in the context of term substitution.