Free variables and free-for substitution

An occurrence is a token position in the parsed finite word. A variable occurrence is free when it is in a term field and no ancestor quantifier binds that variable. The variable field of a quantifier is a binder, not a free occurrence. Write $\mathrm{FV}(e)$ for the finite set of variables with free occurrences in $e$, and $\mathrm{Var}(e)$ for all variables appearing anywhere. A sentence is a formula with empty $\mathrm{FV}$.

The recursive rules are $\mathrm{FV}(v)=\{v\}$, $\mathrm{FV}(c)=\mathrm{\varnothing }$, union over the arguments for function and atomic relation/equality expressions, unchanged under negation, union for conjunction, and $\mathrm{FV}(\mathrm{\exists }y\psi )=\mathrm{FV}(\psi )\setminus \{y\}$. Structural recursion justifies these set-valued definitions, with targets $\mathcal{P}(\omega )$ after identifying variables with their indices.

Raw substitution $e[t\mathrm{/}x]$ replaces just the free occurrences of variable $x$ by term $t$. On terms it replaces $x$ by $t$, keeps other variables and constants, and acts on each argument. It commutes with atoms and Boolean constructors. At $\mathrm{\exists }y\psi$ it leaves the whole expression unchanged if $y=x$; otherwise it gives $\mathrm{\exists }y(\psi [t\mathrm{/}x])$.

The term $t$ is free for $x$ in $e$ if, at every replaced occurrence, the path to the root crosses no binder for a member of $\mathrm{FV}(t)$. Thus at $\mathrm{\exists }y\psi$ with $y\mathrm{\ne }x$ and $x\in \mathrm{FV}(\psi )$ it requires both $y\mathrm{\notin }\mathrm{FV}(t)$ and that $t$ be free for $x$ in $\psi$. If no free $x$ occurs, the condition is vacuous. Simultaneous substitution replaces the original free occurrences once; it does not perform substitutions inside inserted terms. It need not equal sequential substitution.

Conventions and prerequisites: Structural induction and recursion on syntax.