Definition:Substitution (Formal Systems)

This page is about substitution in the context of formal systems. 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'}$