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

Definition

Let $\beta, \tau$ be terms of predicate logic.

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

Let $\beta \left({x \gets \tau}\right)$ be the term resulting from $\beta$ by replacing all occurrences of $x$ by $\tau$.

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

Also known as

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

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

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

Also see

• Substitution Instance of Term is Term
• Substitution Theorem for Terms

Sources

• 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\mathrm{II}.8$ Further Semantic Notions: Definition $\mathrm{II.8.6}$