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

From ProofWiki
Jump to navigation Jump to search


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