Induction without integers (aka Structural Induction)

$\def\p{{\mathscr R}}$If you are uncomfortable with the idea of doing induction directly on the structure, or if you want to reduce the question to one of induction on the integers, you can proceed by induction on the size of the WFF, for some suitable definition of "size". One typical definition is that the size of the WFF is the number of logical operators it contains.

Then to prove that $\p(W)$ holds for every WFF $W$, you proceed as follows:

1. Show that $\p(W)$ holds for each $W$ of the smallest possible size. (1, if you are counting atoms, or 0, if you are counting operators.)
2. Show that if $\p(W)$ holds for all $W$ of size less than $n$, then it must hold for all $W$ of size $n$, as follows: Let $W$ be a WFF of size $n$. Then it must have the form $\sim A$ for some wff $A$ of size $n-1$, or the form $A\oplus B$ for some operator $\oplus$ and some wffs $A$ and $B$ each of size at most $n-1$. Fill in the inductive argument for the two or more cases.

Formulated in this way, the induction is just a regular strong induction on integers, where instead of proving the statement "$\p(W)$ holds for all wffs $W$", you reformulate it as "For all numbers $n$, $\p(W)$ holds for each wff of size $n$".

But this sort of transformation should not really be necessary. The induction principle can be stated more generally. Suppose $S$ is any set, and $\prec$ is a well-founded order on $S$; this means that every subset of $S$ is either empty, or contains a $\prec$-minimal element, which is an element $m\in S$ such that no other element $m'\in S$ has $m'\prec m$.

A typical example would be that wffs can be ordered by an ordering that says that $a\prec b$ whenever $a$ is a subformula of $b$. For example, $(x\land y)$ is a subformula of $\lnot(x\land y)\lor z$, so $(x\land y)\prec \lnot(x\land y)\lor z$.

The ordering $\prec$ need not be total, which means that it is possible that none of $a\prec b, a=b, $ and $b\prec a$ need be true. For the $\prec$ of the previous paragraph, we have neither $a\land b \prec a\lor b$ nor $a\lor b \prec a\land b$. That is quite all right.

Then you can use well-founded induction as follows:

1. Let $F$ be the set of wffs for which $\p$ is false. Suppose $F$ is nonempty. Then by the well-foundedness of $\prec$, it has a $\prec$-minimal element $m$.
2. Show that $m$ cannot have any subformulas, as follows. Show that if $m$ does have subformulas, then, using some properties of $\p$, show that $\p$ must hold for one of the subformulas. But then this subformula is an element of $F$, contradicting the minimality of $m$, which rules out this case.
3. So $m$ has no subformulas. Rule out this case using some property of $\p$.

This rules out the possibility that $F$ actually contains a $\prec$-minimal element $m$, and the only remaining possibility is that $F$ is empty, and so $\p$ holds for every wff.

Ordinary induction is a special case of well-founded induction which uses the well-founded relation $\lt$ on the natural numbers. The well-foundedness of $\lt$ is equivalent to the so-called well-ordering principle of the natural numbers, which states that every subset of $\Bbb N$ either contains a $\lt$-minimal element, or is empty.