# Principle of Structural Induction

## Theorem

Let $\mathcal L$ be a formal language.

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

Let $P \left({\phi}\right)$ be a statement (in the metalanguage of $\mathcal L$) about well-formed formulas $\phi$ of $\mathcal L$.

Then $P$ is true for all WFFs of $\mathcal L$ iff both:

- $P \left({a}\right)$ is true for all letters $a$ of $\mathcal L$,

and, for each rule of formation of $\mathcal L$, if $\phi$ is a WFF resulting from WFFs $\phi_1, \ldots, \phi_n$ by applying that rule, then:

- $P \left({\phi}\right)$ is true as soon as $P \left({\phi_1}\right), \ldots, P \left({\phi_n}\right)$ are all true.

## Proof

Let $\phi$ be a WFF of $\mathcal L$.

Then $\phi$ is the result of applying finitely many rules of formation of $\mathcal L$.

If we can show that the result of each rule of formation satisfies $P$, we will have finished.

Suppose now that for a rule of formation $\mathbf R$, all preceding rules have produced WFFs satisfying $P$.

By the bottom-up nature of the formal grammar of $\mathcal L$, $\mathbf R$ either:

The two given hypotheses precisely ensure that the WFF resulting from $\mathbf R$ must also satisfy $P$.

For the first rule of formation applied, all preceding rules have vacuously produced WFFs satisfying $P$.

But now we see that any subsequent rule of formation will satisfy this premise.

In particular, it applies to the final rule of formation, and hence $P \left({\phi}\right)$ is true.

$\blacksquare$

## Remark

Although the proof is strongly reminiscent of the Principle of Mathematical Induction, it can be seen to be a *finite*, *algorithmic* procedure:

- Given any WFF $\phi$, we have a definite procedure for verifying $P \left({\phi}\right)$, which involves only finitely many operations.

The assumptions of the theorem ensure that each of these operations will affirm the truth of $P \left({\phi}\right)$.

It is therefore justifiable to accept this proof in the metalanguage.

## Sources

- 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 2.1.4$: Theorem $2.12$