Definition:Substitution (Formal Systems)/Term
Jump to navigation
Jump to search
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$.