42.01.03 · mathematical-logic / first-order-logic-completeness

First-Order Languages: Syntax and Unique Readability

shipped3 tiersLean: none

Anchor (Master): Enderton 2001 *A Mathematical Introduction to Logic* 2e Ch. 2 (the full first-order syntax with and without equality, the term algebra, prenex normal form); Shoenfield 1967 *Mathematical Logic* (Addison-Wesley) Ch. 2 §2.1-2.6; Hodges 1993 *Model Theory* (Cambridge) Ch. 1 (signatures, terms, the term algebra as the absolutely free algebra, formulas); Frege 1879 *Begriffsschrift* (the first formal quantificational syntax)

Intuition Beginner

Propositional logic has one kind of atom: a bare statement that is either true or false, like "it is raining." That is too coarse for mathematics. We want to talk about objects — numbers, points, sets — and say things about them and between them: this number is even, that point lies on this line, every number has a successor. First-order logic is the grammar built for exactly this. It adds names for objects, ways to combine names into bigger names, statements about those names, and the two phrases "for-all" and "there-exists."

Think of it as setting up a small formal vocabulary before you say anything. You list your raw materials. Some symbols name fixed objects, like the symbol for zero. Some symbols are operations that take objects and return a new object, like "add" or "successor." Some symbols are relations that take objects and report true or false, like "is less than." Once the vocabulary is fixed, two kinds of expression can be built. A term is a name for an object, built by stacking operations on top of variables and constants. A formula is a statement, built from relations applied to terms and then glued together with "and," "not," "if-then," and the two quantifiers.

The whole point of this unit is to pin down those building rules so precisely that a formula becomes a definite object, with no ambiguity about how it was put together. That precision is what later lets us say what a formula means and what counts as a proof of it. This unit is pure grammar: no truth, no meaning yet — only what counts as a legal sentence.

Visual Beginner

A term is a name built like an arithmetic expression, and it has a tree showing how it was assembled. In the language of arithmetic, with a symbol $S$ for "successor" (add one), the term "successor of (successor of zero)" names the number two. Its tree stacks the operations.

   Term:  S( S( 0 ) )      names the number 2

   Build tree (outermost operation on top):

              S
              |
              S
              |
              0

   A formula puts a relation on top of terms:

   Formula:  ( S(0) < S(S(0)) )      says  1 < 2

                 <
                /  \
              S      S
              |      |
              0      S
                     |
                     0

Read each tree from the bottom. The leaves are constants or variables — here the constant $0$ . Each step up applies one operation symbol. The term tree on the left builds a name and never produces a true-or-false statement. The formula tree on the right puts the relation symbol " $<$ " on top of two finished terms, and only at that top step does it become a statement that could be true or false.

expression	kind	what it is
$0$	term	names a fixed object
$S (0)$	term	names "one more than zero"
$S (0) < S (S (0))$	formula	says one object is below another
$for-all x : x < S (x)$	formula	a statement about every object

Terms name; formulas claim. Keeping the two apart is the first discipline of the subject.

Worked example Beginner

We work inside the language of arithmetic, whose vocabulary has a constant $0$ , a one-place operation $S$ ("successor"), a two-place operation $+$ , and a two-place relation $<$ . The task: build the statement "for every number, that number is less than its successor," step by step, and identify which pieces are terms and which is the final formula.

Step 1. Pick a variable to stand for "every number." Use $x$ . A lone variable is the simplest term — it is a name (for an as-yet-unspecified object).

Step 2. Build the successor of $x$ . Apply the operation $S$ to the term $x$ , getting the term $S (x)$ . This is again a term: a name for "one more than $x$ ."

Step 3. Make a statement comparing the two terms. Apply the relation $<$ to the terms $x$ and $S (x)$ . This gives the atomic formula $x < S (x)$ — the smallest kind of statement, a relation applied to finished names.

Step 4. Quantify. We want this to hold for every number, so attach the for-all quantifier binding $x$ : the formula becomes "for-all $x$ , $x < S (x)$ ."

Step 5. Check what each piece is. The names $x$ and $S (x)$ are terms. The comparison $x < S (x)$ is a formula. Putting "for-all $x$ " in front keeps it a formula, now one that mentions no leftover unspecified object.

What this tells us: every legal statement bottoms out in terms (names) fed into a relation, then wrapped with connectives and quantifiers. The variable $x$ started out free — a genuine blank — and the quantifier "for-all $x$ " closed that blank, turning the statement into one with a fixed meaning. The next sections make "free," "bound," and "the reach of a quantifier" exact.

Check your understanding Beginner

Formal definition Intermediate+

A first-order language (signature, vocabulary) $L$ is given by its parameters: a set of constant symbols $c$ ; for each $n \geq 1$ a set of $n$ -place function symbols $f$ ; and for each $n \geq 1$ a set of $n$ -place relation (predicate) symbols $P$ . The logical symbols, common to every language, are a countable supply of variables $v_{1}, v_{2}, \dots$ , the connectives $\neg$ and $\to$ (with $\land, \lor, \leftrightarrow$ defined), the universal quantifier $\forall$ , the parentheses, and — for a language with equality — the binary relation symbol $=$ counted as logical ^{[Enderton §2.1]}. The arity function recording each symbol's number of places is part of the data; we write $L = {0, S, +, \cdot, <}$ for the language of arithmetic, ${\cdot,^{- 1}, e}$ for groups, ${\in}$ for set theory, and ${<, +, \cdot, 0, 1}$ for ordered fields, each with the indicated arities.

The terms of $L$ form the smallest set $T$ of strings containing every variable and every constant symbol and closed under: for each $n$ -place function symbol $f$ and terms $t_{1}, \dots, t_{n}$ , the string $F_{f} (t_{1}, \dots, t_{n}) = f t_{1} \dots t_{n}$ is a term. Equivalently $T = ⋃_{k} T_{k}$ with $T_{0}$ the variables and constants and $T_{k + 1}$ adjoining all $F_{f}$ -images of members of $T_{k}$ . A term is closed (a ground term) if no variable occurs in it. The atomic formulas are the strings $= t_{1} t_{2}$ (when $L$ has equality) and $P t_{1} \dots t_{n}$ for an $n$ -place relation symbol $P$ and terms $t_{i}$ . The well-formed formulas (wffs) form the smallest set $W$ containing the atomic formulas and closed under $$ \mathcal{E}{\neg}(\alpha) = (\neg \alpha), \qquad \mathcal{E}{\rightarrow}(\alpha,\beta) = (\alpha \rightarrow \beta), \qquad \mathcal{Q}_i(\alpha) = (\forall v_i, \alpha). $$ The existential quantifier is the abbreviation $(\exists v_{i} α) := (\neg\forall v_{i} (\neg α))$ ^{[Enderton §2.1]}.

An occurrence of a variable $x$ in a wff is bound if it lies within (the scope of) a quantifier $\forall x$ — formally, the scope of the quantifier $\forall v_{i}$ in $(\forall v_{i} α)$ is the subformula $α$ , and an occurrence is bound iff it sits inside the scope of some quantifier on that same variable; otherwise it is free. A wff with no free occurrences of any variable is a sentence (closed formula); only sentences acquire a truth value once a structure is fixed, which is the business of the semantics unit. The substitution $α_{t}^{x}$ replaces every free occurrence of $x$ in $α$ by the term $t$ , defined by recursion on $α$ . The term $t$ is substitutable for $x$ in $α$ (Shoenfield: free for) when, for every variable $y$ occurring in $t$ , no free occurrence of $x$ in $α$ lies inside the scope of a quantifier $\forall y$ ^{[Shoenfield §2.4]}. This side condition is what stops variable capture below.

Counterexamples to common slips Intermediate+

"A term and a formula are the same kind of object." They are disjoint. A term names an object and never carries a truth value; a formula makes a claim. In the language of arithmetic, $S (0) + S (0)$ is a term, while $S (0) + S (0) = S (S (0))$ is a formula. The grammar keeps the two sorts separate, and the parsing theorems are proved separately for each.
"Substituting a term for a free variable is always harmless." Substitute $t = y$ for $x$ in $α = (\exists y (x < y))$ — "some object exceeds $x$ ." The naive replacement yields $(\exists y (y < y))$ , "some object exceeds itself," changing a satisfiable claim into an unsatisfiable one. The variable $y$ of $t$ was captured by the quantifier $\exists y$ . Here $t$ is not substitutable for $x$ in $α$ , so $α_{t}^{x}$ is not formed; one first renames the bound $y$ .
"Free and bound is a property of the variable." It is a property of each occurrence. In $(x < S (x)) \to (\forall x (x < S (x)))$ the same variable $x$ occurs free in the antecedent and bound in the consequent. Freeness is read occurrence by occurrence against the quantifiers whose scope encloses it.
"Dropping parentheses is innocent." Without the convention that each quantifier and connective wraps in parentheses, the string $\forall x α \to β$ is ambiguous between $((\forall x α) \to β)$ and $(\forall x (α \to β))$ . The official grammar's parentheses are exactly what unique readability needs; informal omissions are licensed only by a fixed precedence convention.

Key theorem with proof Intermediate+

The signature theorem of the syntax layer is unique readability: the inductive definitions of terms and of formulas are genuine definitions by recursion, because every compound term and every compound formula decomposes in exactly one way. Without it, the free-variable function, the substitution operation, and — downstream — the satisfaction relation would be ill-defined.

Theorem (Unique readability for terms and formulas). Each term is exactly one of: a variable; a constant symbol; or $f t_{1} \dots t_{n}$ for a unique $n$ -place function symbol $f$ and unique terms $t_{1}, \dots, t_{n}$ . Each wff is exactly one of: an atomic formula $P t_{1} \dots t_{n}$ or $= t_{1} t_{2}$ with the symbol and terms unique; $(\neg α)$ for a unique wff $α$ ; $(α \to β)$ for unique wffs $α, β$ ; or $(\forall v_{i} α)$ for a unique variable $v_{i}$ and unique wff $α$ . In every case no term (resp. wff) is a proper initial segment of another, and the leading symbol together with its constituents is determined by the string alone ^{[Enderton §2.2]}.

Proof. Take terms first. Use the polish (prefix) presentation $f t_{1} \dots t_{n}$ with no parentheses, and assign to each symbol a weight: a variable or constant counts $+ 1$ , an $n$ -place function symbol counts $1 - n$ . Define the weight of a string as the sum of its symbols' weights. A first induction on the construction of terms shows every term has weight $+ 1$ , and every proper nonempty initial segment of a term has weight $\leq 0$ . The base case is immediate: a variable or constant is a single symbol of weight $+ 1$ with no proper nonempty initial segment. For the step, $f t_{1} \dots t_{n}$ has weight $(1 - n) + n \cdot 1 = 1$ ; reading left to right, after the leading $f$ the running weight is $1 - n \leq 0$ , and it climbs back to $+ 1$ only after the last symbol of $t_{n}$ , because each completed $t_{i}$ contributes $+ 1$ and a proper segment stops inside some $t_{j}$ with the earlier $t_{i}$ completed, giving a running total $\leq 0$ .

This weight invariant gives the no-segment claim: a term has weight $+ 1$ , so it cannot be a proper initial segment of another term, whose proper initial segments have weight $\leq 0$ . For uniqueness, a compound term begins with a function symbol $f$ of some arity $n$ , and the constituents are recovered greedily: $t_{1}$ is the shortest initial segment of the remainder having weight $+ 1$ (a complete term), then $t_{2}$ the next such segment, and so on; the weight invariant shows each $t_{i}$ is determined and that exactly $n$ of them are consumed. Hence $f$ and $t_{1}, \dots, t_{n}$ are unique.

For formulas, atomic formulas inherit the term result: $P t_{1} \dots t_{n}$ and $= t_{1} t_{2}$ parse uniquely because the leading relation symbol fixes the arity and the term-parsing recovers the arguments. For compound wffs, run the parenthesis-balance argument of the propositional case 42.01.01 pending: each left parenthesis counts $+ 1$ , each right parenthesis $- 1$ , all other symbols $0$ ; every wff has total balance $0$ while every proper nonempty initial segment has balance $\geq 1$ . A non-atomic wff therefore begins with "(", and the symbol immediately after the "(" is $\neg$ , the matrix of an arrow, or $\forall$ , exclusively. For $(\forall v_{i} α)$ the variable $v_{i}$ is the symbol after $\forall$ and $α$ is the wff filling up to the matching ")"; for $(α \to β)$ the substring $α$ is the shortest balanced wff after the opening "(", which marks the connective and leaves $β$ . Each constituent is determined, so the decomposition is unique. $□$

Corollary (recursion on terms and formulas). Given target data — a value on variables and constants and an operation $h_{f}$ per function symbol — there is a unique function on terms respecting them; likewise on formulas with clauses for atomic formulas, $\neg$ , $\to$ , and $\forall$ . This is what makes the free-variable function $FV$ , the substitution $α_{t}^{x}$ , and the satisfaction relation of the next unit well defined.

Bridge. Unique readability is the foundational reason every syntactic operation on terms and formulas is well defined, and this is exactly the parsing fact that lets the satisfaction relation be built by recursion in the semantics unit. It builds toward the term algebra of the Master tier, where the same uniqueness reappears as the statement that the algebra of terms is absolutely free on the variables, so a variable assignment extends uniquely to a homomorphism — this is exactly the recursion corollary read algebraically. The argument generalises the propositional balance lemma of 42.01.01 pending from connectives alone to a full signature of function and relation symbols with arities, and it appears again wherever an inductively presented syntax must support definition by recursion. The central insight is that an inductive syntax admits recursion precisely when its constructors are injective with pairwise-disjoint ranges; unique readability is that condition made concrete for first-order terms and formulas. Putting these together, the syntax fixed here is the common substrate on which the Tarskian semantics 42.01.04 pending and the deductive calculus 42.01.05 pending are both defined, and the substitutability condition introduced above is the single hinge on which the soundness of the quantifier rules will turn.

Exercises Intermediate+

Exercise 2 (easy, multiple choice).

In the wff $(\forall v_{1} (v_{1} < v_{2})) \to (v_{1} = v_{1})$ , which variable occurrence is free?

A. the $v_{1}$ inside $\forall v_{1} (v_{1} < v_{2})$

B. $v_{2}$

C. neither — both are bound

D. both $v_{2}$ and the $v_{1}$ in the antecedent

Hint

The quantifier $\forall v_{1}$ binds only the occurrences inside its scope $(v_{1} < v_{2})$ . Check each occurrence against the quantifiers whose scope encloses it.

Answer

B and the $v_{1}$ in $(v_{1} = v_{1})$ are free; among the listed options, B. The quantifier $\forall v_{1}$ binds the $v_{1}$ in its scope $(v_{1} < v_{2})$ but never the $v_{2}$ (a different variable) nor the $v_{1}$ in the consequent $(v_{1} = v_{1})$ , which lies outside its scope. So $v_{2}$ is free, and the consequent's $v_{1}$ is free; option A's occurrence is bound. The same variable name can occur both bound and free in one formula.

Exercise 4 (medium, short-answer).

Exhibit a formula $α$ , a variable $x$ , and a term $t$ for which $t$ is not substitutable for $x$ in $α$ , and show that the naive replacement changes the meaning. Then repair it.

Hint

Make $t$ contain a variable that a quantifier of $α$ binds at the position where $x$ occurs free.

Answer

Take $α = (\exists y (y < x))$ — "something is below $x$ " — with $x$ free, and $t = y$ . The naive replacement of $x$ by $y$ gives $(\exists y (y < y))$ , "something is below itself," which no ordering satisfies, though $α$ is satisfiable. The free $x$ sits inside the scope of $\exists y$ and $t = y$ , so $t$ is not substitutable for $x$ in $α$ ; $α_{t}^{x}$ is undefined. Repair by renaming the bound variable: $α \equiv (\exists z (z < x))$ , after which $t = y$ is substitutable and $α_{t}^{x} = (\exists z (z < y))$ has the intended meaning. Rubric: full credit for a genuine capture, the meaning change, and the bound-renaming fix.

Exercise 7 (hard, symbolic).

Prove by induction on terms that for every term $t$ , the number of variable-and-constant symbols in $t$ exceeds the number of argument places supplied by its function symbols by exactly one — equivalently, $# (leaves) = 1 + \sum_{f} n_{f}$ taken over function-symbol occurrences $f$ of arity $n_{f}$ counted with multiplicity minus the function-symbol count. State the clean invariant and prove it.

Hint

This is the weight invariant in disguise. Let $L$ = number of variable/constant occurrences and, for each function-symbol occurrence of arity $n$ , charge $n - 1$ . Show $L - \sum (n - 1) = 1$ .

Answer

Define the invariant $W (t) = (# variable/constant occurrences in t) - \sum_{f occ.} (n_{f} - 1) = \sum_{symbols} w (symbol)$ with $w (var) = w (const) = 1$ and $w (f) = 1 - n_{f}$ . Claim $W (t) = 1$ for every term. Base: a variable or constant is one symbol of weight $1$ , so $W = 1$ . Step: for $t = f t_{1} \dots t_{n}$ with $f$ of arity $n$ , $W (t) = w (f) + \sum_{i = 1}^{n} W (t_{i}) = (1 - n) + n \cdot 1 = 1$ by the inductive hypothesis $W (t_{i}) = 1$ . Hence $W (t) = 1$ for all terms, which rearranges to $# leaves = 1 + \sum_{f} (n_{f} - 1)$ . Rubric: full credit for stating the additive invariant $W$ , the base case, and the arithmetic $(1 - n) + n = 1$ in the step.

Exercise 8 (hard, symbolic).

Prove the substitution lemma at the syntactic level: if $t$ is substitutable for $x$ in $α$ and $u$ is any term, then $(α_{t}^{x})$ is a well-formed formula and $FV (α_{t}^{x}) = (FV (α) ∖ {x}) \cup (if x \in FV (α) then FV (t) else \emptyset)$ . Proceed by induction on $α$ and isolate where substitutability is used.

Hint

The only delicate clause is $\forall y β$ : substitutability guarantees either $y = x$ (substitution stops) or $y \in / FV (t)$ (no capture), so $FV$ behaves.

Answer

Induct on $α$ . Atomic $α = P s_{1} \dots s_{n}$ : $α_{t}^{x}$ replaces $x$ by $t$ throughout each $s_{i}$ , yielding a wff with $FV = (FV (α) ∖ {x}) \cup (FV (t)$ if $x$ occurred $)$ , by the analogous term-level fact. Connective clauses $\neg β$ and $(β \to γ)$ are immediate from the inductive hypothesis, since substitution and $FV$ both distribute over them and substitutability is inherited by subformulas. Quantifier clause $α = (\forall y β)$ : if $y = x$ , then $x$ is not free in $α$ , substitution does nothing, $α_{t}^{x} = α$ , and the formula holds with the "else" branch. If $y \neq = x$ , substitutability of $t$ for $x$ in $α$ forces $y \in / FV (t)$ whenever $x \in FV (β)$ (otherwise $y$ would capture a variable of $t$ ); then $α_{t}^{x} = (\forall y β_{t}^{x})$ and by the inductive hypothesis $FV (α_{t}^{x}) = FV (β_{t}^{x}) ∖ {y} = ((FV (β) ∖ {x}) \cup FV (t)) ∖ {y}$ , which equals $(FV (α) ∖ {x}) \cup FV (t)$ because $y \in / FV (t)$ and $y \in / FV (α)$ . Substitutability is used exactly once, in the $y \neq = x$ quantifier step, to keep $y$ out of $FV (t)$ . Rubric: full credit for the induction, the two quantifier subcases, and pinpointing the single use of substitutability.

Advanced results Master

The syntax fixed in the Formal definition supports three developments: a universal property exhibiting terms as a free algebra, a normal form trading quantifier nesting for a quantifier prefix, and the precise capture-avoidance calculus on which the deductive rules rest.

Theorem 1 (the term algebra is absolutely free). Fix a signature $L$ and a set $X$ of variables. The set $Tm_{L} (X)$ of terms carries an $L$ -algebra structure: each $n$ -place function symbol $f$ acts by $(t_{1}, \dots, t_{n}) \mapsto f t_{1} \dots t_{n}$ and each constant by itself. This algebra is absolutely free on $X$ : for every $L$ -structure $A$ and every assignment $s : X \to A$ of the variables into the carrier $A$ , there is a unique homomorphism $\overset{s}{ˉ} : Tm_{L} (X) \to A$ extending $s$ and commuting with all function symbols ^{[Hodges Ch. 1]}. Existence is the recursion corollary of unique readability; uniqueness is its injectivity-with-disjoint-ranges content. This universal property is unique readability, restated categorically, and it is precisely the recursive clause $\overset{s}{ˉ} (f t_{1} \dots t_{n}) = f^{A} (\overset{s}{ˉ} t_{1}, \dots, \overset{s}{ˉ} t_{n})$ that the next unit promotes to the term-evaluation half of Tarski's satisfaction definition.

Theorem 2 (prenex normal form). Every wff $φ$ is logically equivalent (in the deductive calculus of 42.01.05 pending, and under every structure in 42.01.04 pending) to a prenex wff $Q_{1} x_{1} \dots Q_{k} x_{k} ψ$ with each $Q_{i} \in {\forall, \exists}$ and $ψ$ quantifier-free ^{[Enderton Ch. 2]}. The prenex operations push quantifiers outward across connectives, governed by the freeness side conditions: $\neg\forall x α \equiv \exists x \neg α$ and $\neg\exists x α \equiv \forall x \neg α$ ; $(\forall x α) \to β \equiv \exists x (α \to β)$ and $α \to (\forall x β) \equiv \forall x (α \to β)$ when $x$ is not free in the stationary side, achieved after renaming bound variables apart. The matrix $ψ$ is unique up to propositional equivalence; the quantifier prefix is not unique, but its alternation pattern controls the quantifier-complexity classification ( $Σ_{n} / Π_{n}$ of the arithmetical hierarchy) used downstream in definability and computability.

Theorem 3 (capture-avoiding substitution and the renaming lemma). For any wff $α$ , variable $x$ , and term $t$ , there is a wff $α^{'}$ obtained from $α$ by renaming bound variables (an alphabetic variant, $α \equiv_{α} α^{'}$ ) such that $t$ is substitutable for $x$ in $α^{'}$ ; the capture-avoiding substitution $α [t / x] := (α^{'})_{t}^{x}$ is well defined up to alphabetic variance ^{[Shoenfield §2.4]}. Alphabetic variants are logically indistinguishable: $α \equiv_{α} α^{'}$ implies $α \leftrightarrow α^{'}$ is valid and provable. The substitutability condition is exactly the hypothesis under which the quantifier-instantiation axiom $\forall x α \to α_{t}^{x}$ is sound; without it the axiom fails, as the capture example $(\exists y (y < x))$ shows. This is the single syntactic hinge that makes the quantifier rules of 42.01.05 pending correct.

Theorem 4 (induction and recursion on the syntax). Unique readability yields two reasoning principles used pervasively. Induction on terms (resp. formulas): a property holding of variables and constants (resp. atomic formulas) and preserved by each function symbol (resp. by $\neg$ , $\to$ , $\forall$ ) holds of all terms (resp. formulas). Recursion on terms (resp. formulas): a function is determined by its values on the base cases and a rule per constructor. The free-variable function $FV$ , the height function, substitution $α_{t}^{x}$ , the Gödel numbering used in incompleteness 42.01.08 pending, and the satisfaction relation of 42.01.04 pending are all defined by this recursion, and their basic laws are proved by this induction.

Synthesis. The unique-readability theorem is the foundational reason the entire apparatus is well posed, and putting these together it controls all four downstream developments: it is exactly the freeness of the term algebra, so that a variable assignment extends uniquely to a homomorphism — the central insight that becomes term evaluation in Tarski's satisfaction definition 42.01.04 pending; it underwrites the induction and recursion principles that define $FV$ , substitution, and Gödel numbering; and it makes the substitutability condition statable, which is the bridge from pure grammar to the soundness of the quantifier instantiation axiom in the deductive calculus 42.01.05 pending. The prenex normal form generalises the propositional normal forms of 42.01.01 pending to the quantified setting and is dual, across the negation laws $\neg\forall \equiv \exists\neg$ , to the alternation that the arithmetical hierarchy will measure. This is exactly the architecture promised at the Beginner tier: a grammar so precisely fixed that meaning and proof can both be defined on top of it without ambiguity, with semantics and deduction as the two parallel theories built next over this one shared syntax.

Full proof set Master

Proposition 1 (unique readability for terms). Every term is a variable, a constant symbol, or $f t_{1} \dots t_{n}$ for a unique $n$ -place function symbol $f$ and a unique sequence of terms $t_{1}, \dots, t_{n}$ ; and no term is a proper initial segment of another.

Proof. Weight a variable or constant $+ 1$ and an $n$ -place function symbol $1 - n$ ; the weight of a string is the sum over its symbols. By induction on the construction of terms, every term has weight $+ 1$ : a variable/constant is a single $+ 1$ symbol; and $f t_{1} \dots t_{n}$ has weight $(1 - n) + \sum_{i = 1}^{n} 1 = 1$ . Next, every proper nonempty initial segment of a term has weight $\leq 0$ . For a variable/constant there is no such segment. For $f t_{1} \dots t_{n}$ , a proper initial segment is $f$ followed by $t_{1}, \dots, t_{j - 1}$ in full and a proper initial segment $u$ of $t_{j}$ (possibly empty), with the remaining $t_{j + 1}, \dots, t_{n}$ absent. Its weight is $(1 - n) + (j - 1) + W (u)$ where, by a sub-induction, $W (u) \leq 0$ for a proper initial segment and $W (u) \leq 1$ otherwise; since $j - 1 \leq n - 1$ and $W (u) \leq 1$ , the total is $\leq (1 - n) + (n - 1) + 1 - 1 = 0$ in the boundary case and $\leq 0$ throughout. Thus proper initial segments have weight $\leq 0$ while complete terms have weight $+ 1$ , so no term is a proper initial segment of another. Uniqueness of the decomposition follows: a compound term starts with a unique function symbol $f$ of known arity $n$ ; reading the remainder, $t_{1}$ is the unique shortest initial segment of weight $+ 1$ (the first complete subterm), and inductively $t_{2}, \dots, t_{n}$ are determined, consuming the string exactly. $□$

Proposition 2 (unique readability for formulas). Every wff is, exclusively, an atomic formula with unique relation symbol (or $=$ ) and unique argument terms, or $(\neg α)$ , $(α \to β)$ , or $(\forall v_{i} α)$ with unique constituents.

Proof. Atomic case: an atomic formula begins with a relation symbol $P$ of arity $n$ (or with $=$ ), and the arguments are $n$ (resp. $2$ ) consecutive terms, each parsed uniquely by Proposition 1; the leading symbol fixes which clause applies and the term-parsing fixes the arguments. Compound case: assign parenthesis-balance weights ( $+ 1$ to "(", $- 1$ to ")", $0$ otherwise). By induction every wff has balance $0$ , while every proper nonempty initial segment has balance $\geq 1$ : atomic formulas carry no parentheses, while $(\neg α)$ , $(α \to β)$ , $(\forall v_{i} α)$ each open with "(" raising the balance to $1$ , closed only by the final ")". A compound wff thus begins with "(", and the next symbol is $\neg$ , $\forall$ , or the start of $α$ in an arrow. If $\neg$ : the remainder up to the matching ")" is the unique $α$ . If $\forall$ : the next symbol is the unique bound variable $v_{i}$ and the rest up to ")" is the unique $α$ . Otherwise it is $(α \to β)$ : scanning after the opening "(", the first point at which the running balance returns to $0$ ends the unique wff $α$ , whereupon $\to$ and the wff $β$ are forced. Exclusivity holds because the symbol after "(" cannot belong to two of the distinct classes $\neg$ , $\forall$ , leading-symbol-of-a-wff at once. $□$

Proposition 3 (the recursion principle on formulas). Let $V$ be a set, $h_{at}$ a function on atomic formulas, and $h_{\neg} : V \to V$ , $h_{\to} : V \times V \to V$ , $h_{\forall} : (variables) \times V \to V$ . There is a unique $\overset{ˉ}{h} : W \to V$ with $\overset{ˉ}{h} (atomic) = h_{at}$ , $\overset{ˉ}{h} ((\neg α)) = h_{\neg} (\overset{ˉ}{h} (α))$ , $\overset{ˉ}{h} ((α \to β)) = h_{\to} (\overset{ˉ}{h} (α), \overset{ˉ}{h} (β))$ , and $\overset{ˉ}{h} ((\forall v_{i} α)) = h_{\forall} (v_{i}, \overset{ˉ}{h} (α))$ .

Proof. Define $\overset{ˉ}{h}$ by recursion on the height $n$ of a wff (the length of the longest construction branch), which is well defined because by Proposition 2 each non-atomic wff has uniquely determined immediate constituents of strictly smaller height. Set $\overset{ˉ}{h}$ on atomic formulas to $h_{at}$ ; given $\overset{ˉ}{h}$ on all wffs of height $< n$ , extend to a height- $n$ wff $γ$ by applying the clause matching $γ$ 's unique outermost constructor to the already-defined values on its constituents. This yields a total function. For uniqueness, suppose $\overset{ˉ}{h}, \overset{ˉ}{h}^{'}$ both satisfy the clauses; a structural induction on $γ$ (legitimate by Proposition 2, which supplies the unique decomposition at each step) gives $\overset{ˉ}{h} (γ) = \overset{ˉ}{h}^{'} (γ)$ : equal on atomic formulas by $h_{at}$ , and equal on each compound by the matching clause applied to equal constituent values. Hence $\overset{ˉ}{h}$ is the unique such function. Applying this with the appropriate $V$ and clauses defines $FV$ , the substitution $α_{t}^{x}$ , and (in 42.01.04 pending) the satisfaction relation. $□$

Proposition 4 (the substitutability condition blocks capture). If $t$ is substitutable for $x$ in $α$ , then in $α_{t}^{x}$ no occurrence of a variable of $t$ introduced by the substitution is bound by a quantifier of $α$ ; if $t$ is not substitutable, some such capture occurs.

Proof. Induct on $α$ . For atomic $α$ there are no quantifiers, so every introduced occurrence of a variable of $t$ is free — no capture, and substitutability is vacuous. The connective cases $\neg β$ and $(β \to γ)$ follow from the inductive hypothesis, as quantifiers and free occurrences distribute over them. For $α = (\forall y β)$ : if $y = x$ , then $x$ has no free occurrence in $α$ , the substitution is vacuous, and there is nothing to capture. If $y \neq = x$ and $x \in FV (β)$ , then by definition $t$ is substitutable for $x$ in $α$ iff $y \in / FV (t)$ and $t$ is substitutable for $x$ in $β$ . Under this hypothesis the introduced occurrences of variables of $t$ are those produced inside $β_{t}^{x}$ , none of which is the variable $y$ (since $y \in / FV (t)$ ), so the quantifier $\forall y$ binds none of them; by the inductive hypothesis no quantifier inside $β$ captures them either. Conversely, if $t$ is not substitutable, the failure occurs at some quantifier $\forall y$ with $y \in FV (t)$ enclosing a free occurrence of $x$ ; substituting places that $y$ inside the scope of $\forall y$ , a capture. $□$

Connections Master

Propositional logic as a formal system 42.01.01 pending is the warm-up whose architecture this unit lifts to quantifiers. The parenthesis-balance argument proving unique readability for sentential formulas is re-run here, extended to a full signature of function and relation symbols with arities (the polish-notation weight argument for terms) and to the quantifier constructor $\forall v_{i}$ . The propositional unit owns the connective layer and its recursion principle; this unit owns terms, atomic formulas, quantifiers, free and bound variables, and substitution, on which the first-order semantics and deduction are defined.
The semantics of first-order logic — Tarskian satisfaction in a structure — is co-produced as 42.01.04 pending and is defined by recursion on the syntax fixed here. The term-algebra universal property (Theorem 1) becomes term evaluation $t^{A} [s]$ , the atomic clause reads off the interpreted relations, and the recursion principle (Proposition 3) supplies the satisfaction clauses for $\neg, \to, \forall$ . The substitution lemma of this unit is exactly what makes Tarski's quantifier clause agree with substitution of witnesses. Without unique readability the satisfaction relation would not be well defined.
The deductive calculus for first-order logic is co-produced as 42.01.05 pending and is likewise defined over this syntax. Its quantifier-instantiation axiom $\forall x α \to α_{t}^{x}$ is sound precisely when $t$ is substitutable for $x$ in $α$ (Theorem 3, Proposition 4), so the substitutability condition introduced here is the single hinge of the quantifier rules; the completeness theorem 42.01.06 pending then matches this calculus to the semantics of 42.01.04 pending.
Axiomatic set theory 42.03.01 is presented in the first-order language ${\in}$ defined by this unit's grammar: the ZFC axioms are sentences of that language, the Separation and Replacement schemas are infinite families indexed by the formulas defined here, and the proper-class notation ${x : φ (x)}$ is read off the free-variable apparatus. Likewise the Gödel numbering of incompleteness 42.01.08 pending is a recursion on exactly this syntax.

Historical & philosophical context Master

Quantificational syntax begins with Gottlob Frege's Begriffsschrift (1879), the first formal language with nested quantifiers and bound variables, in which generality was expressed by a notation for "for all" governing a scope — the conceptual ancestor of the $\forall v_{i}$ constructor and of the free/bound distinction ^{[Frege 1879]}. Charles Sanders Peirce and his student Oscar Howard Mitchell independently developed quantifier notation in the 1880s, and Giuseppe Peano's notation (1889) supplied the $\exists$ and $\forall$ -style symbols that, refined by Russell and Whitehead in Principia Mathematica (1910-13), became standard.

The separation of a language (a signature of symbols) from its interpretations is due to the model-theoretic tradition: Leopold Löwenheim (1915) and Thoralf Skolem (1920) treated first-order formulas as syntactic objects evaluated in varying domains, and David Hilbert and Wilhelm Ackermann's Grundzüge der theoretischen Logik (1928) codified the engere Funktionenkalkül (the restricted, i.e. first-order, predicate calculus) with its precise formation rules. The unique-readability theorem and the induction/recursion principles it licenses were made explicit in the textbook tradition — Stephen Cole Kleene's Introduction to Metamathematics (1952), Joseph Shoenfield's Mathematical Logic (1967) ^{[Shoenfield §2.1]}, and Herbert Enderton's text ^{[Enderton §2.2]}. The capture problem in substitution, and the free for condition that resolves it, were isolated as the soundness-critical side condition for the quantifier axioms; the term algebra as the absolutely free algebra on its variables is the universal-algebra and model-theoretic reading given by Wilfrid Hodges ^{[Hodges Ch. 1]} and traced to Birkhoff's free-algebra constructions.

Bibliography Master

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@book{shoenfield1967logic,
  author    = {Shoenfield, Joseph R.},
  title     = {Mathematical Logic},
  publisher = {Addison-Wesley},
  year      = {1967}
}

@book{hodges1993modeltheory,
  author    = {Hodges, Wilfrid},
  title     = {Model Theory},
  series    = {Encyclopedia of Mathematics and its Applications},
  volume    = {42},
  publisher = {Cambridge University Press},
  year      = {1993}
}

@book{frege1879begriffsschrift,
  author    = {Frege, Gottlob},
  title     = {Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens},
  publisher = {Louis Nebert, Halle},
  year      = {1879}
}

@book{hilbertackermann1928,
  author    = {Hilbert, David and Ackermann, Wilhelm},
  title     = {Grundz\"{u}ge der theoretischen Logik},
  publisher = {Springer},
  year      = {1928}
}

@book{kleene1952metamathematics,
  author    = {Kleene, Stephen Cole},
  title     = {Introduction to Metamathematics},
  publisher = {North-Holland},
  year      = {1952}
}

@article{skolem1920,
  author  = {Skolem, Thoralf},
  title   = {Logisch-kombinatorische Untersuchungen \"{u}ber die Erf\"{u}llbarkeit oder Beweisbarkeit mathematischer S\"{a}tze},
  journal = {Skrifter utgit av Videnskapsselskapet i Kristiania},
  year    = {1920}
}

@article{lowenheim1915,
  author  = {L\"{o}wenheim, Leopold},
  title   = {\"{U}ber M\"{o}glichkeiten im Relativkalk\"{u}l},
  journal = {Mathematische Annalen},
  volume  = {76},
  year    = {1915},
  pages   = {447--470}
}

Prerequisites

none — this is a leaf unit

Tier anchors

beginner: Enderton 2001 *A Mathematical Introduction to Logic* 2e (Harcourt/Academic Press) §2.0-2.1 (the symbols of a first-order language read informally — constants, function symbols, relation symbols, variables, the connectives, and the two quantifiers — and the idea of a term as a name built from those pieces and a formula as a statement built over terms, before any induction); reading and writing small terms and atomic statements in the language of arithmetic by hand
intermediate: Enderton 2001 *A Mathematical Introduction to Logic* 2e §2.1-2.2 (a first-order language as a signature of parameters with arities, the inductive definition of terms and of well-formed formulas, the unique-readability / parsing theorem for terms and formulas, free and bound occurrences of variables, the scope of a quantifier, sentences, substitution of a term for a free variable, and the substitutability / free-for condition that blocks variable capture)
master: Enderton 2001 *A Mathematical Introduction to Logic* 2e Ch. 2 (the full first-order syntax with and without equality, the term algebra, prenex normal form); Shoenfield 1967 *Mathematical Logic* (Addison-Wesley) Ch. 2 §2.1-2.6; Hodges 1993 *Model Theory* (Cambridge) Ch. 1 (signatures, terms, the term algebra as the absolutely free algebra, formulas); Frege 1879 *Begriffsschrift* (the first formal quantificational syntax)

References

Enderton, H. B. — A Mathematical Introduction to Logic · 2nd edition, Harcourt/Academic Press (2001), Chapter 2. §2.0-2.1 fixes a first-order language by its parameters: a (possibly empty) set of constant symbols, for each positive arity a set of n-place function symbols, and for each positive arity a set of n-place relation (predicate) symbols, together with the logical symbols common to every language — a countable list of variables v_1, v_2, ..., the connectives ¬ and → (the others defined), the universal quantifier ∀, parentheses, and optionally the equality symbol =. Terms are defined inductively as the smallest set containing every variable and every constant symbol and closed under the term-building operations F_f(t_1,...,t_n) = f t_1 ... t_n for each n-place function symbol f. Atomic formulas are equalities t_1 = t_2 (when = is present) and predications P t_1 ... t_n for an n-place relation symbol P. Well-formed formulas (wffs) are the smallest set containing the atomic formulas and closed under E_¬(α) = (¬α), E_→(α,β) = (α→β), and Q_i(α) = (∀v_i α). §2.2 proves unique readability for terms and for formulas (the parsing theorems): every term is a variable, a constant, or f t_1 ... t_n for a unique function symbol f and unique terms t_1,...,t_n; every wff is atomic, or (¬α), (α→β), or (∀v_i α) for unique constituents — so the recursion principle applies. Free and bound occurrences of a variable are defined by recursion (an occurrence of v_i in (∀v_i α) is bound, the quantifier ∀v_i has scope α); a sentence is a formula with no free variables. The substitution α^x_t of a term t for the variable x is defined by recursion on α, and t is substitutable for x in α (t is 'free for x in α') when no variable of t becomes bound by a quantifier of α at the position of substitution; the substitution lemma underlying the quantifier axioms requires this condition. Prenex normal form (a string of quantifiers followed by a quantifier-free matrix) is obtained by the prenex operations.
Shoenfield, J. R. — Mathematical Logic · Addison-Wesley (1967), Chapter 2 ('First-Order Theories'), §2.1-2.6. Defines a first-order language by its non-logical symbols (constants, function symbols, predicate symbols with their arities) over the logical symbols; gives the inductive definitions of term and of formula, proves the formation (unique-readability) results that license definition and proof by induction on terms and formulas, and develops free and bound variables, the substitution t[x] of a term for a variable, and the condition that t be substitutable (Shoenfield's 'free for') so that the quantifier axiom ∀x A → A[t] is sound. Treats designators and the distinction between syntax (the formal language) and the interpretations supplied later by structures.
Hodges, W. — Model Theory · Cambridge University Press (1993), Chapter 1. Presents a signature (vocabulary) as a set of constant, function, and relation symbols with an arity function, and builds the term algebra over a signature and a set of variables as the absolutely free (initial) algebra on the variables: the carrier is the set of terms, each n-place function symbol is interpreted by the syntactic operation t_1,...,t_n ↦ f(t_1,...,t_n), and unique readability is exactly the freeness — every assignment of the variables into an arbitrary algebra of the signature extends uniquely to a homomorphism out of the term algebra. Atomic and first-order formulas are then defined over the terms, with free variables, scope, and substitution treated as syntactic operations on this algebra.

Estimated time

beginner: 18m
intermediate: 50m
master: 85m