Parsing, Substitution, and Substitutability

Defining a function by recursion on a string presumes the string decomposes in exactly one way. The value of a term, satisfaction, and free occurrence 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 needs.

Counting to read terms

Terms use Polish notation: 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.

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$ .

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

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.

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.

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:

\textsc{ParseTerm}(\varepsilon)

— build the formation tree of a term, or reject

1
place $\varepsilon$ at the root as the only vertex
2
repeat
3
if every minimal vertex holds a single symbol then
4
return the tree
each such symbol is a variable or constant
5
select a minimal vertex whose expression has two or more symbols
6
let $f$ be its first symbol
7
if $f$ is not an $n$ -place function symbol with $n > 0$ then reject
8
create $n$ child vertices below it
9
for each child in turn do
10
scan the remaining symbols until the shortest string $t$ with $K(t) = 1$
11
if the expression ends before such $t$ is found then reject
12
label the child with $t$ and remove $t$ from the front of the remainder
13
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

+ (v_{1}, f (S 0, v_{2})) .

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.

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, K ()) = 1, K (\forall) = - 1, K (\neg) = 0, K (\to) = - 1, 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 (α) = 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.

Decomposition of

(\forall v_{1} P v_{1} \to \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.

Every recursion on wffs depends on this theorem.

With freeness established, the recursion theorem 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 α$ infer $α$ with $t$ in place of $x$ . That replacement is an operation on syntax, defined by recursion.

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 $φ_{x}^{x} = φ$ , and $(Q x \to \forall x P x)_{y}^{x} = (Q y \to \forall x P x)$ — the free $x$ becomes $y$ , the bound one does not.

Substituting

t

for

x

(P x \to \forall x P x)

rewrites only the free occurrence; the occurrence bound by

\forall x

is shielded and left unchanged.

Substitutability

Blind substitution can go wrong. Let $α$ 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

α_{y}^{x} = \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 α \to α_{t}^{x}$ is only sound when this cannot happen.

Capture: substituting the term

y

for

x

\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.

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 $α$ is substitutable. Note a terminology trap: even when $t$ is not substitutable, the expression $α_{t}^{x}$ is still formed by replacing free $x$ with $t$ ; substitutable names a property, not a precondition for writing the symbol.

Worked example. Take $α = \neg \forall y x = y$ . Test the proposed axiom $\forall x α \to α_{t}^{x}$ 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 $α$ , it is substitutable, and

α_{z}^{x} = \neg \forall y z = y .

The consequent says $z$ has something unequal to it — true whenever the antecedent is. The axiom instance $\forall x α \to \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 $α$ . Forming $α_{y}^{x}$ anyway replaces the free $x$ and lets the new $y$ fall under $\forall y$ :

α_{y}^{x} = \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 α \to α_{y}^{x}$ 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 $α$ 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.

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$ .

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.

The substitution lemma as a commuting square: satisfying

φ_{t}^{x}

under

s

(top route) and satisfying

φ

under the reassignment

s (x ∣ \overset{s}{ˉ} (t))

(bottom route) always give the same truth value, provided

t

is substitutable for

x

φ

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 $α_{t}^{x}$	instantiate a quantifier	quantifier axiom of the calculus
substitutability	no variable capture	soundness of that axiom
substitution lemma	syntax matches semantics	soundness and completeness

Syntax, structures, satisfaction, definability, and substitution together fix the language of first-order logic as a mathematical object. 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.