Definition:Substitution (Formal Systems)/Well-Formed Part/Example
Jump to navigation
Jump to search
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}$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.3.2$: Example $2.33$