I am struggling to understand the following definitions.

$\textbf{Definition}$. Let $x$ be a variable symbol and let $F$ be a formula. For each occurrence of the symbol $x$, which does not immediately follow a quantifier, in the formula $F$, we define whether the occurrence of $x$ is $\textbf{free}$ or $\textbf{bound}$ inductively as follows.

(1) If $F$ is a formula of one of the forms $y = z$ or $y \in z$, where $y$ and $z$ are variable symbols (possibly equal to $x$), then every occurrence of $x$ in $F$ is free, and no occurrence is bound.

(2) If $F$ is a formula of one of the forms $\neg G, (G \land H), (G \lor H), (G \rightarrow H), (G \iff H)$, where $G$ and $H$ are formulas, then each occurrence of the symbol $x$ is either an occurrence in the formula $G$ or an occurrence in the formula $H$, and each free (respectively, bound) occurrence of $x$ in $G$ remains free (respectively, bound) in $F$, and similarly for each free (or bound) occurrence of $x$ in $H$.

$\textbf{Question}.$ These two last paragraphs are completely vague to me. Can someone please explain to me what these two notions (free and bound occurrence) mean, preferably with an example or two?

$\textbf{PS}$. I can read the set notations like $\neg G, (G \land H), (G \lor H), (G \rightarrow H), (G \iff H)$. I just don't understand the notion of free and bound.

  • $\begingroup$ You have to know the syntax of FOL. $\endgroup$ – Mauro ALLEGRANZA Dec 14 '17 at 13:18
  • $\begingroup$ We have atomic formulas, like: $P(x), x=y, x \in y$ where every occurrence of variables is free. $\endgroup$ – Mauro ALLEGRANZA Dec 14 '17 at 13:19
  • $\begingroup$ And we have "complex" formulas, built-up using conncetives and quantifiers: they may have both free and bound occurrences of variables. In e.g. $\forall x \lnot (x \in y)$ the occurrence of $y$ is free while the occurrences of $x$ are bound. $\endgroup$ – Mauro ALLEGRANZA Dec 14 '17 at 13:20
  • $\begingroup$ @MauroALLEGRANZA What do you mean when you say the occurrence of a variable is free? $\endgroup$ – Teodorism Dec 14 '17 at 13:20
  • $\begingroup$ Think of a quantifier $\forall$ or $\exists$ as a set of handcuffs, or leg shackles, or a straightjacket. It binds the variable, it inhibits the variable, it enslaves the variable. A variable which has not been bound, or inhibited, or enslaved in that manner is a "free" variable. $\endgroup$ – Lee Mosher Dec 14 '17 at 13:26

Consider a variable $x$ and a formula $A$.

We say that an occurrence of the variable $x$ in $A$ is free when:

1) $A$ is atomic (like: $x=y$ and $x \in y$); i.e. in an atomic formula every occurrence of a variable is free.

2) an occurrence of $x$ in $(¬ A)$ is free iff $x$ occurs free in $A$.

3) an occurrence of $x$ in $(A \to B)$ is free iff $x$ occurs free in $A$ or in $B$ (and the same for the other binary connectives).

4) $x$ occurs free in $∀ y A$ iff $x$ occurs free in $A$ and $x \ne y$.

An occurrence of $x$ in a formula $A$ that is not free is a bound occurrence.

Some examples.

In the formula $(x \in y)$ the occurrences of $x$ and $y$ are both free.

In the formula $(x \in y) \land (y \in x)$ the occurrences of $x$ and $y$ are free.

In the formula $\forall x \ \lnot (x \in y)$ the occurrence of $y$ is free while both occurrences of $x$ are bound.

The "gist" of point (2) is that the connectives do not change the "status" (free or bound) of variables; only the quantifiers do it.


Those paragraphs are (roughly, see below) describing an algorithm for calculating whether $x$ is free in a formula $F$. This is a situation where formalism (or "code") is preferable to text. (Imagine trying to tell someone how to multiply polynomials with just words. There's a reason why mathematicians need a chalkboard around.)

Let $\mathsf{freeIn}(x, F)$ be a relation that holds exactly when $x$ occurs free in $F$. $\mathsf{freeIn}$ is inductively defined as follows: $$\mathsf{freeIn}(x, F) = \begin{cases} x= y \text{ or }x = z, & F \in\{y \in z, y = z\} \\ \mathsf{freeIn}(x,G)\text{ or }\mathsf{freeIn}(x,H), & F\in\{G\land H, G\lor H,G\to H, G\iff H\} \\ \mathsf{freeIn}(x, G), & F = \neg G \\ \mathsf{freeIn}(x,G)\text{ and }x\neq y, & F\in\{\forall y.G,\exists y.G\} \end{cases}$$ This is a bit different from what the paragraphs describe (besides adding the quantifier case) because it simply tells you whether a variable is free in a formula, not whether an occurrence is. To talk about occurrences would require having some way to refer to specific parts of a formula, e.g. a root-to-leaf path in the abstract syntax tree or something like "the third $x$ in the string representing the formula". If occurrences were represented by root-to-leaf paths, it would be easy to change the above definition into a definition of a function that returns the set of all free occurrences of a variable. Alternatively, you could define a similar function by structural recursion on the root-to-leaf path.


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.