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

From ProofWiki
Jump to navigation Jump to search


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