Definition:Substitution (Formal Systems)/Term

Definition

Substitution of Term in Term

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

Substitution of Term in WFF

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