# Definition:Substitution (Formal Systems)

*This page is about Substitution in the context of Formal System. For other uses, see Substitution.*

## Definition

### Substitution for Well-Formed Part

Let $\FF$ be a formal language with alphabet $\AA$.

Let $\mathbf B$ be a well-formed formula of $\FF$.

Let $\mathbf A$ be a well-formed part of $\mathbf B$.

Let $\mathbf A'$ be another well-formed formula.

Then the **substitution of $\mathbf A'$ for $\mathbf A$ in $\mathbf B$** is the collation resulting from $\mathbf B$ by replacing all occurrences of $\mathbf A$ in $\mathbf B$ by $\mathbf A'$.

It is denoted as $\map {\mathbf B} {\mathbf A' \mathbin {//} \mathbf A}$.

### Substitution for Letter

Let $\mathbf B$ be a well-formed formula of $\FF$.

Let $p$ be a letter of $\FF$.

Let $\mathbf A$ be another well-formed formula.

Then the **substitution of $\mathbf A$ for $p$ in $\mathbf B$** is the collation resulting from $\mathbf B$ by replacing all occurrences of $p$ in $\mathbf B$ by $\mathbf A$.

It is denoted as $\map {\mathbf B} {\mathbf A \mathbin {//} p}$.

### Substitution of Term for Variable

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

### Substitution for Metasymbol

Let $S_1$ be a statement form.

Let $p$ be a metasymbol which occurs one or more times in $S_1$.

Let $T$ be a statement.

Let $S_2$ be the string formed by replacing *every* occurrence of $p$ in $S_1$ with $T$.

Then $S_2$ results from the **substitution of $p$ by $T$ in $S_1$**.

$S_2$ is called a **substitution instance** of $S_1$.

## Notation

There are many alternative notations for $\map {\mathbf B} {\mathbf A' \mathbin {//} \mathbf A}$.

These mainly concern the style of the brackets, and sometimes an alternative symbol (usually $\gets$ or a single $/$) for the slashes $//$.

For example:

- $\mathbf B \set {\mathbf A \gets \mathbf A'}$
- $\mathbf B \sqbrk {\mathbf A' \mathbin {//} \mathbf A}$
- $\map {\mathbf B} {\mathbf A \leadsto \mathbf A'}$