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

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$