M(1) for all n in N: M(n) -> M(n+1) --------------------------------------- for all n in N: M(n)Here N is the set of natural numbers: {1,2,3,4,....}
Example (cf. page 51): We want to prove M(n) where
M(n): 1 + ... + n = n(n+1)/2The proof is as follows:
1 = 1(1+1)/2which is trivial.
1 + ... + n+1 = 1 + ... + n + n+1 = n(n+1)/2 + n+1 since M(n) holds by our induction hypothesis = (n(n+1) + 2(n+1))/2 = (n+1)(n+2)/2
M(0) and for all n >= 0: M(n) -> M(n+1) ------------------------------------------ for all n >= 0: M(n)or by some other value.
for all n in N: M(1) /\ ... /\ M(n-1) -> M(n) --------------------------------------------- for all n in N: M(n)Note that for n = 1, the conjunction in the premise is empty, so we can rewrite the rule as
M(1) and for all n >= 2: M(1) /\ ... /\ M(n-1) -> M(n) ------------------------------------------------------ for all n in N: M(n)Example: Consider the Fibonacci numbers given by
fib(1) = 1 fib(2) = 1 fib(n) = fib(n-1) + fib(n-2) for n >= 3Theorem: If
Proof: We shall employ course-of-values induction; there is thus no base step but "only" the inductive step for which we have to do a case analysis. In all cases, we can assume that the result hold for all m < n.
Theorem: Mathematical induction implies Course-of-values induction.
Proof: Given some property M, and assume that for all n in N
M(1) /\ ... /\ M(n-1) -> M(n).Our goal is to prove, using the principle of mathematical induction, that M(n) holds for all n in N. For that purpose, we define a new property M':
M'(n) : M(1) /\ ... /\ M(n).As M(1) clearly holds, we have
M'(1).Also, it is easy to see that for n in N,
M'(n) = M(1) /\ ... /\ M(n) -> M(1) /\ ... /\ M(n) /\ M(n+1) = M'(n+1).So by the principle of mathematical induction, M'(n) holds for all n in N. But then also M(n) holds for all n in N, as desired. This concludes the proof.
Theorem: Course-of-values induction implies Mathematical induction.
Proof: Given some property M, and assume that
M(1) and for all n in N: M(n) -> M(n+1)Our goal is to prove, using the principle of course-of-values induction, that M(n) holds for all n in N. But since for n > 1 we have M(n-1) -> M(n) it in fact holds for all n in N that
M(1) /\ ... /\ M(n-1) -> M(n).So by the principle of course-of-values induction, M(n) holds for all n in N. This is as desired, and thus concludes the proof.
lst ::= nil | (c :: lst)where c can be arbitrary (though we shall often think of c as being an integer). That is, a list is either empty (nil) or an element c in front of a list.
Example: Consider a list with the elements 5,7,4 (note that the order matters). This list is in our syntax written as
(5 :: (7 :: (4 :: nil)))or graphically
:: / \ 5 :: / \ 7 :: / \ 4 nilIn the spirit of Definition 1.31 (page 55), we define a function computing the height of a list:
height(nil) = 1 height(c :: x) = 1 + height(x)
append nil y = y append (c :: x) y = (c :: (append x y))Example:
append (5 :: (7 :: nil)) (8 :: (4 :: nil)) = (5 :: (append (7 :: nil) (8 :: (4 :: nil)))) = (5 :: (7 :: (append nil (8 :: (4 :: nil))))) = (5 :: (7 :: (8 :: (4 :: nil))))
M(nil) for all lists x: M(x) -> M((c :: x)) --------------------------------------------- for all lists x: M(x)So in order to show that a property holds for all lists, you must show that it holds for the empty list, and that the property holds for a non-empty list provided it holds for its "tail".
Theorem: For all x, we have M(x) where
M(x): append x nil = xProof: Structural induction.
append nil nil = nilwhich is trivial from the definition of append.
append (c :: x) nil = (c :: (append x nil)) definition of append = (c :: x) the induction hypothesis
Theorem: For all x, we have M(x) where
M(x): append (append x y) z = append x (append y z)Proof: Structural induction.
append (append nil y) z = append nil (append y z)which is trivial since both LHS and RHS reduce to
append y z.
append (append (c :: x) y) z = append (c :: (append x y)) z definition of append = (c :: (append (append x y) z)) definition of append = (c :: (append x (append y z))) induction hypothesis = append (c :: x) (append y z) definition of append
Theorem: Mathematical induction implies Structural induction.
Proof: Given some property M on lists, and assume that
M(nil) and for all lists x: M(x) -> M(c :: x)Our goal is to prove, using the principle of mathematical induction, that M(x) holds for all lists x. For that purpose, we define a new property M' on natural numbers:
M'(n): for all lists x with height(x) = n, M(x) holdsAs nil is the only list with height 1, we have
M'(1).Now assume that M'(n). Let y be a list with height(y) = n+1. We can clearly write y on the form (c :: x) with height(x) = n. From M'(n) we infer that M(x) holds, and from our assumption we conclude M(c :: x), that is M(y). As y was arbitrary with height(y) = n+1, this shows that M'(n+1). We have thus established
M'(n) -> M'(n+1).Mathematical induction thus enables us to infer that M'(n) holds for all n in N. As all lists have a height which is a natural number, this shows that M(x) holds for all lists x. This concludes the proof.
Theorem: Structural induction implies Mathematical induction.
Proof: Given some property M on natural numbers, and assume that
M(1) and for all n in N: M(n) -> M(n+1)Our goal is to prove, using the principle of structural induction, that M(n) holds for all n in N. For that purpose, we define a new property M' on lists:
M'(x) = M(height(x))Since height(nil) = 1, we have
M'(nil).Now assume that we have M'(x), that is M(height(x)). By our assumption, this implies M(height(x) + 1), which is the same as M(height(c :: x)). But this shows that M'(c :: x) holds. We have thus established
M'(x) -> M'(c :: x).Structural induction thus enables us to infer that M'(x) holds for all lists x. Since for all n in N there exists a list x with height(x) = n, this shows that M(n) holds for all n in N. This concludes the proof.
phi ::= p | (~ phi) | (phi /\ phi) | (phi \/ phi) | (phi -> phi)where we can use Convention 1.3 (page 5) to eliminate some of the brackets.
Recall that the BNF grammar for lists
x ::= nil | (c :: x)gives rise to the induction principle
M(nil) M(x) -> M((c :: x)) --------------------- for all lists x: M(x)Similarly, the BNF grammar for well-formed formulas gives rise to the induction principle (the generalization to other BNF grammars is straightforward)
M(p) M(phi) -> M((~ phi)) M(phi1) /\ M(phi2) -> M((phi1 /\ phi2)) M(phi1) /\ M(phi2) -> M((phi1 \/ phi2)) M(phi1) /\ M(phi2) -> M((phi1 -> phi2)) --------------------------------------- for all formulas phi: M(phi)We can use that principle to give a slightly alternative proof of Theorem 1.32 on page 55: Let
M(phi): LBS(phi) = RBS(phi)where LBS(phi) is the the number of left brackets in phi, and RBS(phi) is the number of right brackets in phi.
Our task is then to prove that M(phi) holds for all well-formed formulas phi. We do that by structural induction, and must establish several properties:
LBS((~phi)) = 1 + LBS(phi) = 1 + RBS(phi) = RBS((~phi))
LBS((phi1 /\ phi2)) = 1 + LBS(phi1) + LBS(phi2) = 1 + RBS(phi1) + RBS(phi2) = RBS((phi1 /\ phi2))
M(phi) can be proven, assuming that M(phi') holds for all phi' "smaller than" phi ---------------------------------------------- M(phi) holds for all formulas phiThe unspecific "smaller than" can be instantiated in several ways:
M(phi) can be proven, assuming that M(phi') holds for all phi' that are proper subtrees of phi ----------------------------------------------------------- M(phi) holds for all formulas phior, similar to the approach on page 55,
M(phi) can be proven, assuming that M(phi') holds for all phi' with height(phi') < height(phi) ----------------------------------------------------------- M(phi) holds for all formulas phiWe can now do part of Exercise 1.14(7), page 84.
Theorem: Assume that phi does not contain implications. Then [[NNF(phi)]] = [[phi]].
(Recall that [[phi]] denotes the semantics of the formula phi, that is a mapping which given truth values for the atoms in phi returns the corresponding truth value of phi.)
Proof: We shall perform structural induction in the definition of NNF, presented page 80. Different cases:
[[NNF(phi)]] = [[NNF(phi1) /\ NNF(phi2)]] = [[NNF(phi1)]] /\ [[NNF(phi2)]] = [[phi1]] /\ [[phi2]] = [[phi]]
[[NNF(phi)]] = [[NNF(phi1)]] = [[phi1]] = [[phi]]
[[NNF(phi)]] = [[NNF(~phi1 \/ ~phi2)]] = [[NNF(~phi1)]] \/ [[NNF(~phi2)]]and by applying de Morgan's laws we see that
[[phi]] = [[~phi1]] \/ [[~phi2]]Our claim that [[NNF(phi)]] = [[phi]] would therefore follow if we could establish
[[NNF(~phi1)]] = [[~phi1]] and [[NNF(~phi2)]] = [[~phi2]].But this follows from the induction hypothesis applied to ~phi1 and ~phi2. Of course, for this to be a valid inference, we need to show that height(~phi1) (and also height(~phi_2)) is smaller than height(phi). But this follows from the calculation
height(~phi1) = 1 + height(phi1) <= 1 + max(height(phi1),height(phi2)) = height(phi1 /\ phi2) < 1 + height(phi1 /\ phi2) = height(phi).