Understanding the definition of free and bound occurrence

Question

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.

Answer 1

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.

Answer 2

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.