Induction on Well-Formed Formulas

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathcal F$ be a formal language with a bottom-up grammar.

Let $\Phi$ be a proposition about the well-formed formulas of $\mathcal F$.


Suppose that $\Phi$ is true for all letters of $\mathcal F$.

Suppose further that every rule of formation preserves $\Phi$, i.e. when fed well-formed formulas satisfying $\Phi$, it yields new well-formed formulas satisfying $\Phi$.


Then all well-formed formulas of $\mathcal F$ satisfy $\Phi$.


Proof

By definition of bottom-up grammar, the well-formed formulas of $\mathcal F$ comprise:

letters of $\mathcal F$;
expressions resulting from rules of formation.


Either case is dealt with by the assumptions on $\Phi$.

Hence the result, from Proof by Cases.

$\blacksquare$