THEOREM

*******

Strong induction follows from weak (ordinary) induction

Source: http://www.oxfordmathcenter.com/drupal7/node/485

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com

AXIOMS/DEFINITIONS

******************

1 Set(n)

Axiom

2 0 e n

Axiom

3 1 e n

Axiom

Define: +

4 ALL(a):ALL(b):[a e n & b e n => a+b e n]

Axiom

Define: <=

5 ALL(a):ALL(b):[a e n & b e n => [a<=b <=> EXIST(c):[c e n & a+c=b]]]

Axiom

Required Properties of <=

6 ALL(a):[a e n => [a<=0 => a=0]]

Axiom

7 ALL(a):[Set(a) => ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e a]] & b+1 e a

=> ALL(c):[c e n => [c<=b+1 => c e a]]]]]

Axiom

WEAK (ORDINARY) INDUCTION HOLDS (USING +1)

******************************************

8 ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [0 e a & ALL(b):[b e a => b+1 e a]

=> ALL(b):[b e n => b e a]]]

Axiom

Let p be a subset of n

9 Set(p) & ALL(b):[b e p => b e n]

Premise

10 Set(p)

Split, 9

11 ALL(b):[b e p => b e n]

Split, 9

Prove: 0 e p & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] => b+1 e p]]

=> ALL(b):[b e p => b+1 e p]

Suppose...

12 0 e p & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] => b+1 e p]]

Premise

13 0 e p

Split, 12

14 ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] => b+1 e p]]

Split, 12

Prove: ALL(a):[a e n => ALL(b):[b e n => [b<=a => b e p]]] (by ordinary induction)

Construct the set of natural numbers for which this is true.

Apply Subset Axiom

15 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ALL(b):[b e n => [b<=a => b e p]]]]

Subset, 1

16 Set(q) & ALL(a):[a e q <=> a e n & ALL(b):[b e n => [b<=a => b e p]]]

E Spec, 15

Define: q

17 Set(q)

Split, 16

18 ALL(a):[a e q <=> a e n & ALL(b):[b e n => [b<=a => b e p]]]

Split, 16

Apply Ordinary Induction for subset q

19 Set(q) & ALL(b):[b e q => b e n]

=> [0 e q & ALL(b):[b e q => b+1 e q]

=> ALL(b):[b e n => b e q]]

U Spec, 8

Prove: ALL(b):[b e q => b e n]

Suppose...

20 x e q

Premise

Apply definition of q

21 x e q <=> x e n & ALL(b):[b e n => [b<=x => b e p]]

U Spec, 18

22 [x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]]

& [x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q]

Iff-And, 21

23 x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]

Split, 22

24 x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q

Split, 22

25 x e n & ALL(b):[b e n => [b<=x => b e p]]

Detach, 23, 20

26 x e n

Split, 25

As Required:

27 ALL(b):[b e q => b e n]

4 Conclusion, 20

28 Set(q) & ALL(b):[b e q => b e n]

Join, 17, 27

Sufficient: For ALL(b):[b e n => b e q]

29 0 e q & ALL(b):[b e q => b+1 e q]

=> ALL(b):[b e n => b e q]

Detach, 19, 28

BASIS STEP

**********

Prove: 0 e q

Apply definition of q

30 0 e q <=> 0 e n & ALL(b):[b e n => [b<=0 => b e p]]

U Spec, 18

31 [0 e q => 0 e n & ALL(b):[b e n => [b<=0 => b e p]]]

& [0 e n & ALL(b):[b e n => [b<=0 => b e p]] => 0 e q]

Iff-And, 30

32 0 e q => 0 e n & ALL(b):[b e n => [b<=0 => b e p]]

Split, 31

Sufficient: For 0 e q

33 0 e n & ALL(b):[b e n => [b<=0 => b e p]] => 0 e q

Split, 31

Prove: ALL(b):[b e n => [b<=0 => b e p]]

Suppose...

34 x e n

Premise

Prove: x<=0 => x e p

Suppose...

35 x<=0

Premise

Apply property of <=

36 x e n => [x<=0 => x=0]

U Spec, 6

37 x<=0 => x=0

Detach, 36, 34

38 x=0

Detach, 37, 35

39 x e p

Substitute, 38, 13

As Required:

40 x<=0 => x e p

4 Conclusion, 35

As Required:

41 ALL(b):[b e n => [b<=0 => b e p]]

4 Conclusion, 34

42 0 e n & ALL(b):[b e n => [b<=0 => b e p]]

Join, 2, 41

As Required:

43 0 e q

Detach, 33, 42

INDUCTIVE STEP

**************

Prove: ALL(b):[b e q => b+1 e q]

Suppose...

44 x e q

Premise

Apply definition of q for x

45 x e q <=> x e n & ALL(b):[b e n => [b<=x => b e p]]

U Spec, 18

46 [x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]]

& [x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q]

Iff-And, 45

47 x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]

Split, 46

48 x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q

Split, 46

49 x e n & ALL(b):[b e n => [b<=x => b e p]]

Detach, 47, 44

50 x e n

Split, 49

51 ALL(b):[b e n => [b<=x => b e p]]

Split, 49

Apply definition of q for x+1

52 x+1 e q <=> x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]]

U Spec, 18

53 [x+1 e q => x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]]]

& [x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]] => x+1 e q]

Iff-And, 52

54 x+1 e q => x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]]

Split, 53

Sufficient: For x+1 in q

55 x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]] => x+1 e q

Split, 53

Apply definition of +

56 ALL(b):[x e n & b e n => x+b e n]

U Spec, 4

57 x e n & 1 e n => x+1 e n

U Spec, 56

58 x e n & 1 e n

Join, 50, 3

59 x+1 e n

Detach, 57, 58

Apply premise

60 x e n => [ALL(c):[c e n => [c<=x => c e p]] => x+1 e p]

U Spec, 14

61 ALL(c):[c e n => [c<=x => c e p]] => x+1 e p

Detach, 60, 50

62 x+1 e p

Detach, 61, 51

Apply property of <=

63 Set(p) => ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] & b+1 e p

=> ALL(c):[c e n => [c<=b+1 => c e p]]]]

U Spec, 7

64 ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] & b+1 e p

=> ALL(c):[c e n => [c<=b+1 => c e p]]]]

Detach, 63, 10

65 x e n => [ALL(c):[c e n => [c<=x => c e p]] & x+1 e p

=> ALL(c):[c e n => [c<=x+1 => c e p]]]

U Spec, 64

66 ALL(c):[c e n => [c<=x => c e p]] & x+1 e p

=> ALL(c):[c e n => [c<=x+1 => c e p]]

Detach, 65, 50

67 ALL(b):[b e n => [b<=x => b e p]] & x+1 e p

Join, 51, 62

68 ALL(c):[c e n => [c<=x+1 => c e p]]

Detach, 66, 67

69 x+1 e n & ALL(c):[c e n => [c<=x+1 => c e p]]

Join, 59, 68

70 x+1 e q

Detach, 55, 69

As Required:

71 ALL(b):[b e q => b+1 e q]

4 Conclusion, 44

Joining results...

72 0 e q & ALL(b):[b e q => b+1 e q]

Join, 43, 71

73 ALL(b):[b e n => b e q]

Detach, 29, 72

Prove: ALL(a):[a e n => ALL(b):[b e n => [b<=a => b e p]]]

Suppose...

74 x e n

Premise

75 x e n => x e q

U Spec, 73

76 x e q

Detach, 75, 74

Apply definition of q

77 x e q <=> x e n & ALL(b):[b e n => [b<=x => b e p]]

U Spec, 18

78 [x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]]

& [x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q]

Iff-And, 77

79 x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]

Split, 78

80 x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q

Split, 78

81 x e n & ALL(b):[b e n => [b<=x => b e p]]

Detach, 79, 76

82 x e n

Split, 81

83 ALL(b):[b e n => [b<=x => b e p]]

Split, 81

As Required:

84 ALL(a):[a e n => ALL(b):[b e n => [b<=a => b e p]]]

4 Conclusion, 74

Prove: ALL(b):[b e p => b+1 e p]

Suppose...

85 x e p

Premise

86 x e p => x e n

U Spec, 11

87 x e n

Detach, 86, 85

Apply premise

88 x e n => [ALL(c):[c e n => [c<=x => c e p]] => x+1 e p]

U Spec, 14

89 ALL(c):[c e n => [c<=x => c e p]] => x+1 e p

Detach, 88, 87

90 x e n => ALL(b):[b e n => [b<=x => b e p]]

U Spec, 84

91 ALL(b):[b e n => [b<=x => b e p]]

Detach, 90, 87

92 x+1 e p

Detach, 89, 91

As Required:

93 ALL(b):[b e p => b+1 e p]

4 Conclusion, 85

Apply Ordinary Induction for subset p

94 Set(p) & ALL(b):[b e p => b e n]

=> [0 e p & ALL(b):[b e p => b+1 e p]

=> ALL(b):[b e n => b e p]]

U Spec, 8

95 0 e p & ALL(b):[b e p => b+1 e p]

=> ALL(b):[b e n => b e p]

Detach, 94, 9

96 0 e p & ALL(b):[b e p => b+1 e p]

Join, 13, 93

97 ALL(b):[b e n => b e p]

Detach, 95, 96

As Required:

98 0 e p & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] => b+1 e p]]

=> ALL(b):[b e n => b e p]

4 Conclusion, 12

STRONG INDUCTION HOLDS

**********************

As Required:

99 ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [0 e a & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e a]] => b+1 e a]]

=> ALL(b):[b e n => b e a]]]

4 Conclusion, 9