Definition:Substitution (Formal Systems)/Letter

From ProofWiki
Jump to navigation Jump to search

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


Let $\mathcal F$ be a formal language with alphabet $\mathcal A$.

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

Note that it is not immediate that $\mathbf B \left({\mathbf A \mathbin{//} p}\right)$ is a well-formed formula of $\mathcal F$.

This is either accepted as an axiom or proven as a theorem about the formal language $\mathcal F$.