Definition:Substitution (Formal Systems)

From ProofWiki
Jump to navigation Jump to search

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'}$