Structural Induction

Structural Induction is the most general form of induction. In Structural Induction, we can have multiple object constants, multiple function constants, and, unlike our other forms of induction, we can have function constants with multiple arguments. Consider a language with two object constants a and b and a single binary function constant h. See below for a list of some of the terms in the language. We do not provide a graphical rendering in this case, as the structure is more complicated than a line or a tree.

The Structural Induction rule for this language is shown below. If we know that φ holds of our base elements a and b and if we know ∀μ.∀ν.((φ[μ] ∧ φ[ν]) ⇒ φ[h(μ,ν)]), then we can conclude ∀ν.φ[ν] in a single step.

As an example of a domain where Structural Induction is appropriate, recall the world of lists and trees introduced in Chapter 9. Let's assume we have two object constants a and b, a binary function constant h, and two unary relation constants p and q. Relation p is true of a structured object if and only if every fringe node is an a. Relation q is true of a structured object if and only if at least one fringe node is an a. The positive and negative axioms defining the relations are shown below.

Now, as an example of Structural Induction in action, let's prove that every object that satisfies p also satisfies q. In other words, we want to prove the conclusion ∀x.(p(x) ⇒ q(x)). As usual, we start with our premises.

To start the induction, we first prove the base cases for the conclusion. In this world, with two object constants, we need to show the result twice - once for each object constant in the language.

Let's start with a. The derivation is simple in this case. We assume p(a), reiterate q(a) from line 6, then use Implication Introduction to prove (p(a) ⇒ q(a)).

Now, let's do the case for b. As before, we assume p(b), and our goal is to derive q(b). This is a little strange. We know that q(b) is false. Still, we should be able to derive it since we have assumed p(b), which is also false. The trick here is to generate contradictory conclusions from the assumption ¬q(b). To this end, we assume ¬q(b) and first prove p(b). Having done so, we use Implication Introduction to get one implication. Then, we assume ¬q(b) again and this time derive ¬p(b) and get an implication. At this point, we can use Negation Introduction to derive ¬¬q(b) and Negation Elimination to get q(b). Finally, we use Implication Introduction to prove (p(b) ⇒ q(b)).

Having dealt with the base cases, the next step is to prove the inductive case. We need to show that, if our conclusion holds of u and v, then it also holds of h(u,v). To this end, we assume the conjunction of our assumptions with placeholders [c] and [d]; and we then use And Elimination to split that conjunction into its two conjuncts. Our inductive conclusion is also an implication; and, to prove it, we assume its antecedent p(h([c],[d])). From this, we derive p([c]); from that, we derive q([c]); and, from that, we derive q(h([c],[d])). We then use Implication Introduction to get the desired implication. A final use of Implication Introduction and a couple of applications of Universal Introduction gives us the inductive case for the induction.

Finally, using the base case on lines 13 and 23 and the inductive case on line 40, we use Structural Induction to give us the conclusion we set out to prove.

Although the proof in this case is longer than in the previous examples, the basic inductive structure is the same. Importantly, using induction, we can prove this result where otherwise it would not be possible.