Definition:Substitution (Formal Systems)/Well-Formed Part

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

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