# Definition:Substitution (Formal Systems)

*This page is about substitution in the context of formal systems. For other uses, see Definition:Substitution.*

## Contents

## Definition

### Substitution for Well-Formed Part

Let $\mathcal F$ be a formal language with alphabet $\mathcal A$.

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

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 $\mathbf B \left({\mathbf A' \mathbin{//} \mathbf A}\right)$.

### Substitution for Letter

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

Let $p$ be a letter of $\mathcal F$.

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 $\mathbf B \left({\mathbf A \mathbin{//} p}\right)$.

### 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 $\mathbf B \left({\mathbf A' \mathbin{//} \mathbf A}\right)$.

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 \left\{{\mathbf A \gets \mathbf A'}\right\}$
- $\mathbf B \left[{\mathbf A' \mathbin{//} \mathbf A}\right]$
- $\mathbf B \left({\mathbf A \leadsto \mathbf A'}\right)$