Definition:Substitution (Formal Systems)/Letter
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 $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}$.
Note that it is not immediate that $\map {\mathbf B} {\mathbf A \mathbin {//} p}$ is a well-formed formula of $\FF$.
This is either accepted as an axiom or proven as a theorem about the formal language $\FF$.
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.6$: Truth Tables and Tautologies