Definition:Substitution (Formal Systems)/Well-Formed Part
This page is about Substitution in the context of Formal System. For other uses, see Substitution.
Definition
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}$.
Note that it is not immediate that $\map {\mathbf B} {\mathbf A' \mathbin {//} \mathbf A}$ is a well-formed formula of $\FF$.
This is either accepted as an axiom or proven as a theorem about the formal language $\FF$.
Example
Let the WFFs of propositional logic $\mathbf A, \mathbf A'$ and $\mathbf B$ be as follows:
\(\ds \mathbf B\) | \(=\) | \(\ds \paren {p \implies q} \iff \paren {\neg q \implies \neg p}\) | ||||||||||||
\(\ds \mathbf A\) | \(=\) | \(\ds p \implies q\) | ||||||||||||
\(\ds \mathbf A'\) | \(=\) | \(\ds \neg p \lor q\) |
Then the substitution of $\mathbf A'$ for $\mathbf A$ in $\mathbf B$ is given by:
- $\map {\mathbf B} {\mathbf A \mathbin {//} \mathbf A'} = \paren {\neg p \lor q} \iff \paren {\neg q \implies \neg p}$
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'}$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.3.2$: Definition $2.32$