---
title: Parsing, Substitution, and Substitutability
module: First-Order Languages and Structures
moduleNumber: 3
lessonNumber: 4
order: 304
summary: >
  Every recursion on first-order syntax rests on unique readability. A
  parenthesis-counting function proves that terms and formulas decompose in
  exactly one way, and a parsing algorithm recovers the decomposition.
  Substituting a term for a free variable can capture it under a quantifier;
  the substitutability condition rules that out, and the substitution lemma
  trades syntactic substitution for a change of assignment.
topics: [First-Order Languages and Structures]
sources:
  - book: Enderton
    ref: "Ch. 2 — First-Order Logic; §2.3 A Parsing Algorithm; §2.4 substitution and substitutability"
draft: false
---

Defining a function by recursion on a string presumes the string decomposes in
exactly one way. The
[value of a term, satisfaction](/logic/first-order-languages/structures-truth-and-satisfaction),
and [free occurrence](/logic/first-order-languages/first-order-languages) are
all defined this way, and each would be ill-posed if a single expression
admitted two decompositions returning different answers. **Unique readability**
is the theorem that rules this out. A parsing algorithm recovers the
decomposition of any string, and the **substitution** operation together with
its **substitutability** side condition supply the quantifier axiom the
[deductive calculus](/logic/deductive-calculus/a-deductive-calculus) needs.

## Counting to read terms

Terms use [Polish notation](/logic/first-order-languages/first-order-languages):
a function symbol precedes its arguments, with no parentheses or commas. The
tool for analyzing such strings is a weight function that scores how many terms
a symbol still needs behind it.

> **Definition (The function $K$).** Assign to each symbol $K(s) = 1 - n$,
> where $n$ is the number of terms that must follow $s$ to complete a term:
> $K(x) = K(c) = 1$ for variables and constants, and $K(f) = 1 - n$ for an
> $n$-place function symbol. Extend $K$ additively to expressions:
> $K(s_1 \cdots s_m) = K(s_1) + \cdots + K(s_m)$.

Because no symbol is a sequence of others, the extension is unambiguous, and
$K$ was chosen as the unique symbol-weighting for which whole terms score $1$.

> **Lemma (Term count).** For any term $t$, $\ K(t) = 1$. If $\varepsilon$ is a
> concatenation of $m$ terms, then $K(\varepsilon) = m$.

> **Proof.** Induction on $t$: a variable or constant scores $1$, and for $f
> t_1 \cdots t_n$ the count is $(1 - n) + \underbrace{(1 + \cdots + 1)}_{n} = 1$.

Two consequences restrict where a term can begin and end inside a longer string.

> **Lemma (Terminal segments).** Any terminal segment of a term is a
> concatenation of one or more terms, so its $K$-value is at least $1$.

> **Corollary (No initial segment is a term).** If $t_1$ is a proper initial
> segment of a term $t$, then $K(t_1) < 1$; in particular $t_1$ is not itself a
> term.

> **Proof.** Split $t$ into an initial segment $t_1$ and terminal segment
> $t_2$: since $1 = K(t) = K(t_1) + K(t_2)$ and $K(t_2) \ge 1$, the initial part
> scores below $1$.

Reading $K$ as a running total left to right, the count dips below $1$
throughout a term and reaches $1$ only at the very last symbol.

$$
% caption: Running total of $K$ across the term $+\, v_1\, f\, S\, 0\, v_2$
% ($f$ a two-place function symbol); every proper initial segment stays below
% the dashed threshold, which the count reaches only at the final symbol, so no
% prefix is itself a term.
\begin{tikzpicture}[font=\small]
  \definecolor{acc}{HTML}{4A6FA5}
  % axes
  \draw[->, black] (-0.3,0) -- (7.4,0);
  \draw[black, dashed] (-0.3,0.9) -- (7.2,0.9);
  \node[font=\footnotesize, black, anchor=east] at (-0.3,0.9) {$K=1$};
  \node[font=\footnotesize, black, anchor=east] at (-0.3,0) {$K=0$};
  % running totals: +:-1, +v1:0, f:-1, fS:-1, fS0:0, v2:1  (scaled by 0.9)
  \coordinate (p1) at (0.6,-0.9);
  \coordinate (p2) at (1.8, 0.0);
  \coordinate (p3) at (3.0,-0.9);
  \coordinate (p4) at (4.2,-0.9);
  \coordinate (p5) at (5.4, 0.0);
  \coordinate (p6) at (6.6, 0.9);
  \draw[acc, thick] (p1) -- (p2) -- (p3) -- (p4) -- (p5) -- (p6);
  \foreach \p in {p1,p2,p3,p4,p5} \fill[acc] (\p) circle (2pt);
  \fill[acc] (p6) circle (3pt);
  % symbol labels
  \foreach \x/\lab in {0.6/$+$, 1.8/$v_1$, 3.0/$f$, 4.2/$S$, 5.4/$0$, 6.6/$v_2$}
    \node[font=\footnotesize, anchor=north] at (\x,-1.15) {\lab};
  \node[acc, font=\footnotesize, anchor=south] at (6.6,0.95) {complete};
\end{tikzpicture}
$$

## The parsing algorithm

The counting lemmas turn into a procedure that both decides whether an
expression is a term and, if so, builds its unique formation tree. It grows a
tree downward, splitting each compound expression at its leading function
symbol into the arguments that symbol requires.

```algorithm
caption: $\textsc{ParseTerm}(\varepsilon)$ — build the formation tree of a term, or reject
place $\varepsilon$ at the root as the only vertex
repeat
  if every minimal vertex holds a single symbol then
    return the tree // each such symbol is a variable or constant
  select a minimal vertex whose expression has two or more symbols
  let $f$ be its first symbol
  if $f$ is not an $n$-place function symbol with $n > 0$ then reject
  create $n$ child vertices below it
  for each child in turn do
    scan the remaining symbols until the shortest string $t$ with $K(t) = 1$
    if the expression ends before such $t$ is found then reject
    label the child with $t$ and remove $t$ from the front of the remainder
until the tree is complete
```

The split is forced. At each function symbol we take the _first_ string $t$
with $K(t) = 1$: a shorter string would not yet be a term, and a longer one
would contain $t$ as a proper initial segment that is already a complete term,
contradicting the corollary above. No step ever had a second option, so the
decomposition is unique.

> **Worked example.** Parse the term $+\, v_1\, f\, S\, 0\, v_2$, with $+$ and
> $f$ two-place and $S$ one-place, by scanning for the first prefix of $K$-value
> $1$ at each function symbol.
>
> The root $+\, v_1\, f\, S\, 0\, v_2$ leads with the two-place $+$, so it needs
> two argument terms. Scan the remainder $v_1\, f\, S\, 0\, v_2$ left to right,
> reading $K$ as a running total:
> $$
> K(v_1) = 1.
> $$
> The count reaches $1$ at once, so the first argument is $v_1$. The second
> argument is the rest, $f\, S\, 0\, v_2$; its running totals are $-1, -1, 0, 1$,
> reaching $1$ only at the end, so the whole string is one term.
>
> Recurse into $f\, S\, 0\, v_2$: the two-place $f$ needs two arguments. Scanning
> $S\, 0\, v_2$ gives $K(S) = 0$ then $K(S\,0) = 1$, so the first argument is $S\,
> 0$ and the second is $v_2$. Recurse into $S\, 0$: the one-place $S$ takes the
> single term $0$. Every leaf now holds one symbol, so the string is a term, and
> its tree is
> $$
> +\bigl(v_1,\ f(S\,0,\ v_2)\bigr).
> $$
> At each split the first $K = 1$ prefix was the only legal cut, since a shorter
> prefix scores below $1$ and a longer one would swallow a complete term. The
> decomposition is unique.

> **Theorem (Unique readability for terms).** The set of terms is freely
> generated from the variables and constant symbols by the operations $F_f$.

> **Proof.** Freeness has two halves. The ranges of distinct $F_f$ are disjoint,
> and both are disjoint from the atoms, because the first symbol identifies which
> operation (if any) was applied last. Each $F_f$ is one-to-one on terms: if
> $f t_1 t_2 = f t_3 t_4$ then $t_1 t_2 = t_3 t_4$, and were $t_1 \neq t_3$ one
> would be a proper initial segment of the other, impossible for terms.

## Parsing formulas

Formulas use parentheses, so $K$ extends to the remaining symbols by the same
"how many things must follow" principle — counting right parentheses, terms, or
formulas as the objects still required.

$$
K(\,{(}\,) = -1,\quad K(\,{)}\,) = 1,\quad K(\forall) = -1,\quad
K(\neg) = 0,\quad K(\rightarrow) = -1,\quad K(=) = -1,
$$

with $K(P) = 1 - n$ for an $n$-place predicate symbol. The same three lemmas
recur with the same proofs: every wff scores $K(\alpha) = 1$, and every proper
initial segment of a wff scores below $1$, so no proper initial segment of a
formula is a formula.

Parsing formulas mirrors parsing terms, with atomic formulas at the leaves. A
non-atomic wff begins with $\forall v_i$ (one subformula follows) or with a
left parenthesis, after which the next symbol is $\neg$ (one subformula) or the
start of an implication (two subformulas, split by counting parentheses or by
$K$). Both methods locate the split uniquely.

$$
% caption: Decomposition of $(\forall v_1\, P v_1 \rightarrow \neg\, Q v_2)$; the
% outermost operation is the implication, recovered by the counting rule, and
% each subformula decomposes the same way down to the atomic leaves.
\begin{tikzpicture}[font=\small, level distance=12mm,
  level 1/.style={sibling distance=38mm},
  level 2/.style={sibling distance=24mm},
  every node/.style={draw, inner sep=3pt, align=center, font=\footnotesize},
  edge from parent/.style={draw, black}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[draw=acc] {implies}
    child {node {for all $v_1$}
      child {node {$P\, v_1$}}}
    child {node {not}
      child {node {$Q\, v_2$}}};
\end{tikzpicture}
$$

> **Theorem (Unique readability for formulas).** The set of wffs is freely
> generated from the atomic formulas by $\mathcal{E}_\neg$,
> $\mathcal{E}_\rightarrow$, and the $\mathcal{Q}_i$.

Every recursion on wffs depends on this theorem.

> **Proof.** The unary operations are visibly injective; $\mathcal{E}_\rightarrow$
> restricted to wffs is one-to-one by the initial-segment corollary; and the
> ranges are pairwise disjoint because the first one or two symbols reveal the
> outermost operation.

With freeness established, the [recursion theorem](/logic/sentential-logic/induction-and-recursion)
guarantees that the value of a term, the satisfaction relation, and the
free-variable function are each well defined.

## Substitution

The deductive calculus will need to instantiate a universally quantified
variable: from $\forall x\, \alpha$ infer "$\alpha$ with $t$ in place of $x$."
That replacement is an operation on syntax, defined by recursion.

> **Definition (Substitution).** For a variable $x$ and term $t$, the
> expression $\alpha^{x}_{t}$ replaces every _free_ occurrence of $x$ in
> $\alpha$ by $t$:
>
> - atomic $\alpha$: replace $x$ by $t$ throughout;
> - $(\neg\, \alpha)^{x}_{t} = (\neg\, \alpha^{x}_{t})$;
> - $(\alpha \rightarrow \beta)^{x}_{t} = (\alpha^{x}_{t} \rightarrow
>   \beta^{x}_{t})$;
> - $(\forall y\, \alpha)^{x}_{t} = \forall y\, \alpha$ if $x = y$, and
>   $\forall y\, (\alpha^{x}_{t})$ if $x \neq y$.

The quantifier clause is the point: a prefix $\forall x$ shields its variable,
so substitution stops at bound occurrences and touches only free ones. Thus
$\varphi^{x}_{x} = \varphi$, and $(Q x \rightarrow \forall x\, P x)^{x}_{y} =
(Q y \rightarrow \forall x\, P x)$ — the free $x$ becomes $y$, the bound one
does not.

$$
% caption: Substituting $t$ for $x$ in $(P x \rightarrow \forall x\, P x)$
% rewrites only the free occurrence; the occurrence bound by $\forall x$ is
% shielded and left unchanged.
\begin{tikzpicture}[font=\small, node distance=0pt]
  \definecolor{acc}{HTML}{4A6FA5}
  \definecolor{red}{HTML}{C0392B}
  \node (lp) {$($};
  \node[right=1mm of lp, acc] (px) {$P\,x$};
  \node[right=3mm of px] (imp) {implies};
  \node[right=3mm of imp] (fa) {for all $x$};
  \node[right=3mm of fa, black] (px2) {$P\,x$};
  \node[right=1mm of px2] (rp) {$)$};
  \draw[acc, ->] (px.south) .. controls +(0,-0.7) and +(0,-0.7) .. ([yshift=-3mm]px.south);
  \node[acc, font=\footnotesize, anchor=north] at ([yshift=-4mm]px.south) {free: replaced by $t$};
  \draw[black, ->] (px2.south) .. controls +(0,-0.4) and +(0,-0.4) .. ([yshift=-3mm]px2.south);
  \node[black, font=\footnotesize, anchor=north] at ([yshift=-4mm]px2.south) {bound: untouched};
\end{tikzpicture}
$$

## Substitutability

Blind substitution can go wrong. Let $\alpha$ be $\neg\, \forall y\; x = y$,
true in any structure with two or more elements (there is _something_ unequal
to $x$). Instantiating with the term $y$ produces

$$
\alpha^{x}_{y} = \neg\, \forall y\; y = y,
$$

which is false in every structure. The substituted $y$ landed inside the
$\forall y$ and was **captured**, turning a satisfiable formula into a
contradiction. The axiom $\forall x\, \alpha \rightarrow \alpha^{x}_{t}$ is only
sound when this cannot happen.

$$
% caption: Capture: substituting the term $y$ for $x$ in $\neg\, \forall y\, x
% = y$ pushes $y$ under the $\forall y$ quantifier, which binds it; the term's
% variable is swallowed and the meaning is destroyed.
\begin{tikzpicture}[font=\small, node distance=0pt]
  \definecolor{acc}{HTML}{4A6FA5}
  \definecolor{red}{HTML}{C0392B}
  \node (n) {not};
  \node[right=3mm of n] (fa) {for all $y$};
  \node[right=3mm of fa, red] (eq) {$y = y$};
  \draw[red, ->] (fa.south) .. controls +(0.2,-0.7) and +(-0.2,-0.7) .. ([xshift=-3pt]eq.south west);
  \node[red, font=\footnotesize, anchor=north] at (3.3,-0.85) {captures the substituted $y$};
\end{tikzpicture}
$$

> **Definition (Substitutable).** "$t$ is substitutable for $x$ in $\alpha$"
> (also read "$t$ is free for $x$ in $\alpha$") is defined by recursion:
>
> - atomic $\alpha$: always;
> - $t$ is substitutable in $\neg\, \alpha$ iff in $\alpha$, and in $\alpha
>   \rightarrow \beta$ iff in both;
> - $t$ is substitutable for $x$ in $\forall y\, \alpha$ iff either $x$ does not
>   occur free in $\forall y\, \alpha$, or else $y$ does not occur in $t$ and
>   $t$ is substitutable for $x$ in $\alpha$.

The condition guarantees that no variable of $t$ is captured by a quantifier
it passes under. Special cases: $x$ is always substitutable for itself, and any
$t$ whose variables do not occur in $\alpha$ is substitutable. Note a
terminology trap: even when $t$ is _not_ substitutable, the expression
$\alpha^{x}_{t}$ is still formed by replacing free $x$ with $t$; "substitutable"
names a property, not a precondition for writing the symbol.

> **Worked example.** Take $\alpha = \neg\, \forall y\; x = y$. Test the
> proposed axiom $\forall x\, \alpha \rightarrow \alpha^{x}_{t}$ with two terms,
> $t = z$ and $t = y$, and see how substitutability is what keeps it
> sound.
>
> The antecedent $\forall x\, \neg\, \forall y\; x = y$ says every element has
> something unequal to it; it is true in every structure with at least two
> elements.
>
> With $t = z$: since $z$ does not occur in $\alpha$, it is substitutable, and
> $$
> \alpha^{x}_{z} = \neg\, \forall y\; z = y.
> $$
> The consequent says $z$ has something unequal to it — true whenever the
> antecedent is. The axiom instance $\forall x\, \alpha \rightarrow \neg\,
> \forall y\; z = y$ is valid.
>
> With $t = y$: here $y$ occurs in the quantifier $\forall y$, so $y$ is **not**
> substitutable for $x$ in $\alpha$. Forming $\alpha^{x}_{y}$ anyway replaces the
> free $x$ and lets the new $y$ fall under $\forall y$:
> $$
> \alpha^{x}_{y} = \neg\, \forall y\; y = y.
> $$
> The consequent $\neg\, \forall y\; y = y$ is false in every structure, since
> $y = y$ always holds. So $\forall x\, \alpha \rightarrow \alpha^{x}_{y}$ has a
> true antecedent and a false consequent in any two-element structure — not
> valid. The substituted $y$ was captured, and requiring $t$ substitutable for
> $x$ in $\alpha$ is what forbids the instance.

## The substitution lemma

Substitution is a syntactic operation; its semantic meaning is a change of
assignment. The link is proved first for terms, then for formulas.

> **Lemma (Term substitution).** $\ \overline{s}(u^{x}_{t}) = \overline{s(x
> \mid \overline{s}(t))}(u)$.

Substituting $t$ for $x$ inside the term $u$ has the same value as leaving $u$
alone and instead reassigning $x$ to the value of $t$.

> **Proof.** Induction on $u$: for $u = x$ both sides are $\overline{s}(t)$, for
> other atoms both are $\overline{s}(u)$, and the function-symbol step is
> mechanical.

> **Lemma (Substitution lemma).** If $t$ is substitutable for $x$ in $\varphi$,
> then
> $$
> \models_{\fA} \varphi^{x}_{t}\,[s]
> \quad\text{iff}\quad
> \models_{\fA} \varphi\,[\,s(x \mid \overline{s}(t))\,].
> $$

The two routes from a formula-and-assignment to a truth value agree: substitute
the term and then evaluate, or reassign the variable and then evaluate the
original.

> **Proof.** Induction on $\varphi$. The atomic case is the term lemma.
> Connectives are immediate. For $\forall y\, \psi$ with $x$ not free, both
> sides reduce to satisfaction of $\varphi$ itself. The remaining case, $\forall
> y\, \psi$ with $x$ free, is where substitutability is needed: it forces
> $y \notin t$ and $t$ substitutable in $\psi$, so reassigning $x$ never
> disturbs the value fed to $y$, and the inductive hypothesis applies under each
> $s(y \mid d)$.

$$
% caption: The substitution lemma as a commuting square: satisfying
% $\varphi^{x}_{t}$ under $s$ (top route) and satisfying $\varphi$ under the
% reassignment $s(x \mid \bar{s}(t))$ (bottom route) always give the same truth
% value, provided $t$ is substitutable for $x$ in $\varphi$.
\begin{tikzpicture}[font=\small, >=stealth,
  n/.style={draw, align=center, inner sep=4pt, font=\footnotesize}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[n] (tl) at (0,1.7) {a formula and\\an assignment};
  \node[n] (tr) at (6.4,1.7) {evaluate the\\substituted formula};
  \node[n] (br) at (6.4,-0.3) {evaluate the original\\under the reassignment};
  \node[acc, font=\footnotesize, align=center] (v) at (10.2,0.7) {same\\verdict};
  \draw[->, black] (tl) -- (tr) node[midway, above, font=\footnotesize] {substitute t for x};
  \draw[->, black] (tl) -- (br) node[midway, below, sloped, font=\footnotesize] {reassign x to the value of t};
  \draw[acc, thick, <->] (tr) -- (br);
  \draw[acc, dashed, ->] (tr) -- (v);
  \draw[acc, dashed, ->] (br) -- (v);
\end{tikzpicture}
$$

## Where the syntax is used

Each result here is invoked by name later; the table records where.

| Result | Guarantees | Used in |
| --- | --- | --- |
| unique readability | recursions are well defined | value of a term, satisfaction, free variables |
| parsing algorithm | structure is effectively recoverable | decidability of "is a wff" |
| substitution $\alpha^{x}_{t}$ | instantiate a quantifier | quantifier axiom of the calculus |
| substitutability | no variable capture | soundness of that axiom |
| substitution lemma | syntax matches semantics | [soundness](/logic/deductive-calculus/soundness) and [completeness](/logic/deductive-calculus/completeness-and-consistency) |

Syntax, structures, satisfaction, definability, and substitution together fix
the language of first-order logic as a mathematical object. A
[deductive calculus](/logic/deductive-calculus/a-deductive-calculus) built over
it defines a purely syntactic notion of proof; the substitution lemma is what
makes that notion match logical consequence in the soundness and completeness
theorems.