## 12.1 IntroductionInduction is reasoning from the specific to the general. If various instances of a schema are true and there are no counterexamples, we are tempted to conclude a universally quantified version of the schema.
Here is another example. This one is due to the mathematician Fermat (1601-1665). He looked at values of the expression 2
For us, this is not so good. In Logic, we are concerned with logical entailment. We want to derive only conclusions that are guaranteed to be true when the premises are true. Guesses like these are useful in suggesting possible conclusions, but they are not themselves proofs. In order to be sure of universally quantified conclusions, we must be sure that The technique used for complete induction varies with the structure of the language to which it is applied. We begin this chapter with a discussion of domain closure, a rule that applies when the Herbrand base of our language is finite. We then move on to Linear Induction, i.e. the special case in which the ground terms in the language form a linear sequence. We look at tree induction, i.e. the special case in which the ground terms of the language form a tree. And we look at Structural Induction, which applies to all languages. Finally, we look at two special cases that make inductive reasoning more complicated - Multidimensional Induction and Embedded Induction. ## 12.2 Domain ClosureInduction for finite languages is trivial. We simply use the Domain Closure rule of inference. For a language with object constants σ
Recall that, in our formalization of the Sorority World, we have just four constants -
The following proof shows how we can use this rule to derive an inductive conclusion. Given the premises we considered earlier in this book, it is possible to infer that Abby likes someone, Bess likes someone, Cody likes someone, and Dana likes someone. Taking these conclusions as premises and using our Domain Closure rule, we can then derive the inductive conclusion ∀
Unfortunately, this technique does not work when there are infinitely many ground terms. Suppose, for example, we have a language with ground terms σ
This rule is sound in the sense that the conclusion of the rule is logically entailed by the premises of the rule. However, it does not help us produce a proof of this conclusion. To use the rule, we would need to prove all of the rule's premises. Unfortunately, there are infinitely many premises. So, the rule cannot be used in generating a finite proof. All is not lost. It is sometimes possible to write rules that cover all instances without enumerating them individually. The method depends on the structure of the language. The next sections describe how this can be done for languages with different structures. ## 12.3 Linear InductionImagine an infinite set of dominoes placed in a line so that, when one falls, the next domino in the line also falls. If the first domino falls, then the second domino falls. If the second domino falls, then the third domino falls. And so forth. By continuing this chain of reasoning, it is easy for us to convince ourselves that every domino eventually falls. This is the intuition behind a technique called Linear Induction. Consider a language with a single object constant a → s(a) → s(s(a)) → s(s(s(a))) → ...
In this section, we concentrate on languages that have linear structure of this sort. Hereafter, we call these Although there are infinitely many ground terms in any linear language, we can still generate finite proofs that are guaranteed to be correct. The trick is to use the structure of the terms in the language in expressing the premises of an inductive rule of inference known as
A bit of terminology before we go on. The first premise in this rule is called the For the language introduced above, our rule of inference is sound. Suppose we know that a schema is true of The requirement that the signature consists of no other object constants or function constants is crucial. If this were not the case, say there were another object constant Here is an example of induction in action. Recall the formalization of Arithmetic introduced in Chapter 9. Using the object constant 0 and the unary function constant The following axioms describe
It is easy to see that any table that satisfies these axioms includes all of the usual addition facts. The first axiom ensures that all cases with 0 as first argument are included. From this fact and the second axiom, we can see that all cases with The first axiom above tells us that 0 is a We can use induction to prove this result as shown below. We start with our premises. We use Universal Elimination on the first premise to derive the sentence on line 3. This takes care of the base case of our induction. We then start a subproof and assume the antecedent of the inductive case. We then use three applications of Universal Elimination on the second premise to get the sentence on line 5. We use Implication Elimination on this sentence and our assumption to derive the conclusion on line 6. We then discharge our assumption and form the implication shown on line 7 and then universalize this to get the result on line 8. Finally, we use Linear Induction to derive our overall conclusion.
Most inductive proofs have this simple structure. We prove the base case. We assume the inductive hypothesis; we prove the inductive conclusion; and, based on this proof, we have the inductive case. From the base case and the inductive case, we infer the overall conclusion. ## 12.4 Tree InductionTree languages are a superset of linear languages. While in linear languages the terms in the language form a linear sequence, in tree languages the structure is more tree-like. Consider a language with an object constant
As with linear languages, we can write an inductive rule of inference for tree languages. The tree induction rule of inference for the language just described is shown below. Suppose we know that a schema φ holds of
In order to see an example of tree induction in action, consider the ancestry tree for a particular dog. We use the object constant Now, we write down the fundamental rule of dog breeding - we say that a dog is purebred if and only if both its father and its mother are purebred. See below. (This is a bit oversimplified on several grounds. Properly, the father and mother should be of the same breed. Also, this formalization suggests that every dog has an ancestry tree that stretches back without end. However, let's ignore these imperfections for the purposes of our example.) x.(purebred(x) ⇔ purebred(f(x)) ∧ purebred(g(x)))
Suppose now that we discover the fact that our dog A proof of our conclusion is shown below. We start with the premise that Rex is purebred. We also have our constraint on purebred animals as a premise. We use Universal Elimination to instantiate the second premise, and then we use Biconditional Elimination on the biconditional in line 3 to produce the implication on line 4. On line 5, we start a subproof with the assumption the
## 12.5 Structural InductionStructural 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, b, c(a,a), c(a,b), c(b,a), c(b,b), c(a,c(a,a)), c(c(a,a),a), c(c(a,a),c(a,a)), ...
The Structural Induction rule for this language is shown below. If we know that φ holds of our base elements
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
Now, as an example of Structural Induction in action, let's prove that every object that satisfies
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
Now, let's do the case for
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
Finally, using the base case on lines 13 and 23 and the inductive case on line 38, 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. ## 12.6 Multidimensional InductionIn our look at induction thus far, we have been concentrating on examples in which the conclusion is a universally quantified sentence with just one variable. In many situations, we want to use induction to prove a result with more than one universally quantified variable. This is called In principle, multidimensional induction is straightforward. We simply use ordinary induction to prove the outermost universally quantified sentence. Of course, in the case of multidimensional induction the base case and the inductive conclusion are themselves universally quantified sentences; and, if necessary we use induction to prove these subsidiary results. As an example, consider a language with a single object constanta, a unary function constant s, and a binary relation constant e. The axioms shown below define e.
The relation x.∀y.(e(x,y) ⇒ e(y,x)).
In what follows, we use induction to prove the outer quantified formula and then use induction on each of the inner conclusions as well. This means we have two immediate subgoals - the base case for the outer induction and the inductive case for the outer induction.
As usual, we start with our premises. We then prove the base case of the inner induction. This is easy. We assume
The next step is to prove the inductive case for the inner induction. To this end, we assume the inductive hypothesis and try to prove the inductive conclusion. Since the conclusion is itself an implication, we assume its antecedent and prove the consequent. As shown below, we do this by assuming the consequent is false and proving a sentence and its negation. We then use Negation Introduction and Negation Elimination to derives the consequent. We finish with two applications of Implication Introduction and an application of Universal Introduction.
That's a lot of work just to prove the base case of the outer induction. The inductive case of the outer induction is even more complex, and it is easy to make mistakes. The trick to avoiding these mistakes is to be methodical. In order to prove the inductive case for the outer induction, we assume the inductive hypothesis We start by proving the base case for this inner induction. We start with the inductive hypothesis. We then assume the antecedent of the base case.
Next, we work on the inductive case for the second inner induction. We start by assuming the inductive hypothesis. We then assume the antecedent of the inductive conclusion.
From the results on lines 32 and 45, we can conclude the inductive case for the outer induction.
Finally, from the base case for the outer induction and this inductive case, we can conclude our overall result.
As this proof illustrates, the technique of using induction within induction works just fine. Unfortunately, it is tedious and error-prone. for this reason, many people prefer to use specialized forms of multidimensional induction. ## 12.7 Embedded InductionIn 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 non-inductive methods). As an example, consider a world characterized by a single object constant
A little thought reveals that these axioms logically entail the universal conclusion ∀ 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 ∀
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 Chapter 10, there is no such algorithm. ## RecapInduction is reasoning from the specific to the general. ## ExercisesExercise 12.1: Assume a language with the object constants Exercise 12.2: Assume a language with the object constant Exercise 12.3: Assume a language with object constant Exercise 12.4: Consider a language with object constants
Your job is to show that any object that satisfies Exercise 12.5: Starting with the axioms for Exercise 12.6: Consider a language with a single object constant
Prove ∀ |