Definition:Substitution (Formal Systems)

From ProofWiki
Jump to: navigation, search

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

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)$