Definition:Substitution (Formal Systems)/Term/In WFF

Definition

Let $\mathbf A$ be a WFF of predicate logic.

Let $\tau$ be a term of predicate logic.

Let $x \in \mathrm{VAR}$ be a variable.

Let $\mathbf A \left({x \gets \tau}\right)$ be the WFF resulting from $\mathbf A$ by replacing all free occurrences of $x$ by $\tau$.

Then $\mathbf A \left({x \gets \tau}\right)$ is called the substitution instance of $\mathbf A$ substituting $\tau$ for $x$.

Also known as

Some sources write $\mathbf A \left({x \leadsto \tau}\right)$ instead of $\mathbf A \left({x \gets \tau}\right)$.

If the correspondence between variables and terms is clear, $\mathbf A \left({\tau}\right)$ is also often seen.

Similarly, iterated substitution is denoted $\mathbf A \left({x_1 \gets \tau_1, \ldots, x_n \gets \tau_n}\right)$ or simply $\mathbf A \left({\tau_1, \ldots, \tau_n}\right)$.

Also see

• Definition:Alphabetic Substitution

• Substitution Instance of WFF is WFF
• Substitution Theorem for Well-Formed Formulas

Sources

• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.3$
• 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\mathrm{II}.8$ Further Semantic Notions: Definition $\mathrm{II.8.8}$