Principle of Definition by Structural Induction

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathcal L$ be a formal language.

Let the formal grammar of $\mathcal L$ be a bottom-up grammar with unique parsability.


A definition $D \left({\phi}\right)$ (in the metalanguage of $\mathcal L$) for all well-formed formulas $\phi$ of $\mathcal L$ is uniquely specified by:

  • A definition $D \left({a}\right)$ for each letter $a$ of $\mathcal L$
  • For each rule of formation for $\mathcal L$, a definition $D \left({\phi}\right)$ of the resultant WFF $\phi$ in terms of the constituent WFFs' definitions $D \left({\phi_1}\right), \ldots, D \left({\phi_n}\right)$.


Proof

We apply the Principle of Structural Induction on the following statement $P \left({\phi}\right)$:

The definition is specified for $\phi$


The given hypotheses verify the conditions for the Principle of Structural Induction.

It follows that $D \left({\phi}\right)$ is specified for each WFF $\phi$.


Moreover, by virtue of the unique parsability, it is ensured that each WFF $\phi$ has a unique definition $D \left({\phi}\right)$.

$\blacksquare$