
Introduction to Logic

Tools for Thought

In all of the examples in this chapter thus far, induction is used to prove the overall result. While this approach works nicely in many cases, it is not always successful. In some cases, it is easier to use induction on parts of a problem or to prove alternative conclusions and then use these intermediate results to derive the overall conclusions (using inductive or noninductive methods).

As an example, consider a world characterized by a single object constant a, a single unary function constant s, and a single unary relation constant p. Assume we have the set of axioms shown below.
∀x.(p(x) ⇒ p(s(s(x)))) 
p(a) 
p(s(a)) 
A little thought reveals that these axioms logically entail the universal conclusion ∀x.p(x). Unfortunately, we cannot derive this conclusion directly using Linear Induction. The base case is easy enough. And, from p(x) we can easily derive p(s(s(x))). However, it is not so easy to derive p(s(x)), which is what we need for the inductive case of Linear Induction.

The good news is that we can succeed in cases like this by proving a slightly more complicated intermediate conclusion and then using that conclusion to prove the result. One way to do this is shown below. In this case, we start by using Linear Induction to prove ∀x.(p(x) ∧ p(s(x)). The base case p(a) ∧ p(s(a)) is easy, since we are given the two conjuncts as axioms. The inductive case is straightforward. We assume p(x) ∧ p(s(x)). From this hypothesis, we use And Elimination to get p(x) and p(s(x)). We then use Universal Elimination and Implication Elimination to derive p(s(s(x))). We then conjoin these results, use Implication Introduction and Universal Introduction to get the inductive case for our induction. From the base case and the inductive case, we get our intermediate conclusion. Finally, starting with this conclusion, we use Universal Elimination, And Elimination, and Universal Introduction to get the overall result.
1. 

∀x.(p(x) ⇒ p(s(s(x)))) 

Premise 
2. 

p(a) 

Premise 
3. 

p(s(a)) 

Premise 
4. 

p(a) ∧ p(s(a)) 

And Introduction 
5. 

p(x) ∧ p(s(x)) 

Assumption 
6. 

p(x) 

And Elimination 
7. 

p(s(x)) 

And Elimination 
8. 

p(x) ⇒ p(s(s(x))) 

Universal Elimination: 1 
9. 

p(s(s(x))) 

Implication Elimination: 8, 6 
10. 

p(s(x)) ∧ p(s(s(x))) 

And Introduction: 7, 9 
11. 

p(x) ∧ p(s(x)) ⇒ p(s(x)) ∧ p(s(s(x))) 

Implication Introduction: 5, 10 
12. 

∀x.(p(x) ∧ p(s(x)) ⇒ p(s(x)) ∧ p(s(s(x)))) 

Universal Introduction: 11 
13. 

∀x.(p(x) ∧ p(s(x))) 

Induction: 4, 12 
14. 

p(x) ∧ p(s(x)) 

Universal Elimination: 13 
15. 

p(x) 

And Elimination: 14 
16. 

p(s(x)) 

And Elimination: 14 
17. 

∀x.p(x) 

Universal Introduction: 15 

In this case, we are lucky that there is a useful conclusion that we can prove with standard Linear Induction. Things are not always so simple; and in some cases we need more complex forms of induction. Unfortunately, there is no finite collection of approaches to induction that covers all cases. If there were, we could build an algorithm for determining logical entailment for Herbrand Logic in all cases; and, as we discussed in Lesson 10, there is no such algorithm.

Use the arrow keys to navigate.
