THEOREM

*******

 

The principle of backwards induction:

 

  ALL(a):[a e n

  => [P(a) & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]

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

 

where

 

  n is the set of natural numbers

  s is the successor function on n

  P is any unary predicate

 

We can use the principle of backwards induction to prove that for all b in {0, 1, 2, ... a}, we have P(b). To do so, we need only prove:

 

(1) P(a)

(2) For all b in n and b<a and P(s(b)), we have P(b)

 

Informally, we start at the "end point" and work backwards to the "beginning."

 

Outline

*******

 

Line No.  Description

 

  1-6     Peano's Axioms

  7-11    Properties of the < and <= relations used here

  4-15    Define subset n' of n such that:

 

            ALL(a):[a e n' <=> a e n & [P(a) & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]

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

 

 16-26    Apply Induction Principle (PA5) from Peano's Axioms

 27-46    Base case: Prove 0 e n'

 47-114   Inductive step: Prove for all x e n', we also have s(x) e n'

115-End   Generalizing, n'=n

 

 

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

 

 

PEANO'S AXIOMS

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

 

1     Set(n)

      Axiom

 

PA1

 

2     0 e n

      Axiom

 

PA2

 

3     ALL(a):[a e n => s(a) e n]

      Axiom

 

PA3  (not used)

 

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

      Axiom

 

PA4  (not used)

 

5     ALL(a):[a e n => ~s(a)=0]

      Axiom

 

PA5

 

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

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

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

      Axiom

 

 

Properties of < and <= relations used here

 

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

      Axiom

 

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

      Axiom

 

9     ALL(a):ALL(b):[a e n & b e n => [a<b => a<s(b)]]

      Axiom

 

10    ALL(a):ALL(b):[a e n & b e n => [a<s(b) => a<=b]]

      Axiom

 

11    ALL(a):[a e n => a<s(a)]

      Axiom

 

 

Construct subset n' of n

 

Apply Subset Axiom

 

12    EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & [P(a)

     & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]

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

      Subset, 1

 

13    Set(n') & ALL(a):[a e n' <=> a e n & [P(a)

     & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]

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

      E Spec, 12

 

 

Define: n'

 

14    Set(n')

      Split, 13

 

15    ALL(a):[a e n' <=> a e n & [P(a)

     & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]

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

      Split, 13

 

Apply Principle of Mathematical Induction from Peano's Axioms

 

16    Set(n') & ALL(b):[b e n' => b e n]

     => [0 e n' & ALL(b):[b e n' => s(b) e n']

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

      U Spec, 6

 

    

     Prove: n' is a subset n

    

     Suppose...

 

      17    x e n'

            Premise

 

     Apply definition of n'

 

      18    x e n' <=> x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            U Spec, 15

 

      19    [x e n' => x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

          & [x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=x => P(b)]] => x e n']

            Iff-And, 18

 

      20    x e n' => x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            Split, 19

 

      21    x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=x => P(b)]] => x e n'

            Split, 19

 

      22    x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            Detach, 20, 17

 

      23    x e n

            Split, 22

 

As Required:

 

24    ALL(b):[b e n' => b e n]

      4 Conclusion, 17

 

Joining results...

 

25    Set(n') & ALL(b):[b e n' => b e n]

      Join, 14, 24

 

 

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

 

26    0 e n' & ALL(b):[b e n' => s(b) e n']

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

      Detach, 16, 25

 

 

BASE CASE

*********

 

Prove: 0 e n'

 

Apply definition of n'

 

27    0 e n' <=> 0 e n & [P(0)

     & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

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

      U Spec, 15

 

28    [0 e n' => 0 e n & [P(0)

     & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

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

     & [0 e n & [P(0)

     & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

     => ALL(b):[b e n & b<=0 => P(b)]] => 0 e n']

      Iff-And, 27

 

29    0 e n' => 0 e n & [P(0)

     & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

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

      Split, 28

 

Sufficient: For 0 e n'

 

30    0 e n & [P(0)

     & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

     => ALL(b):[b e n & b<=0 => P(b)]] => 0 e n'

      Split, 28

 

    

     Prove: P(0) & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

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

    

     Suppose...

 

      31    P(0)

          & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

            Premise

 

      32    P(0)

            Split, 31

 

      33    ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

            Split, 31

 

         

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

         

          Suppose...

 

            34    x e n & x<=0

                  Premise

 

            35    x e n

                  Split, 34

 

            36    x<=0

                  Split, 34

 

            37    x e n

                  Split, 34

 

            38    x<=0

                  Split, 34

 

          Apply property of <= relation

 

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

                  U Spec, 7

 

            40    x<=0 => x=0

                  Detach, 39, 35

 

            41    x=0

                  Detach, 40, 38

 

            42    P(x)

                  Substitute, 41, 32

 

     As Required:

 

      43    ALL(b):[b e n & b<=0 => P(b)]

            4 Conclusion, 34

 

As Required:

 

44    P(0)

     & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

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

      4 Conclusion, 31

 

Joining results...

 

45    0 e n

     & [P(0)

     & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]

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

      Join, 2, 44

 

As Required:

 

46    0 e n'

      Detach, 30, 45

 

     INDUCTIVE STEP

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

    

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

    

     Suppose...

 

      47    x e n'

            Premise

 

     Apply definition of n'

 

      48    x e n' <=> x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            U Spec, 15

 

      49    [x e n' => x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

          & [x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=x => P(b)]] => x e n']

            Iff-And, 48

 

      50    x e n' => x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            Split, 49

 

      51    x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=x => P(b)]] => x e n'

            Split, 49

 

      52    x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            Detach, 50, 47

 

      53    x e n

            Split, 52

 

      54    P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            Split, 52

 

     Apply definition of n'

 

      55    s(x) e n' <=> s(x) e n & [P(s(x))

          & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=s(x) => P(b)]]

            U Spec, 15

 

      56    [s(x) e n' => s(x) e n & [P(s(x))

          & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=s(x) => P(b)]]]

          & [s(x) e n & [P(s(x))

          & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=s(x) => P(b)]] => s(x) e n']

            Iff-And, 55

 

      57    s(x) e n' => s(x) e n & [P(s(x))

          & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=s(x) => P(b)]]

            Split, 56

 

     Sufficient: For s(x) e n'

 

      58    s(x) e n & [P(s(x))

          & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=s(x) => P(b)]] => s(x) e n'

            Split, 56

 

     Prove: s(x) e n

    

     Apply PA2

 

      59    x e n => s(x) e n

            U Spec, 3

 

     As Required:

 

      60    s(x) e n

            Detach, 59, 53

 

         

          Prove: P(s(x))

                 & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

                 => ALL(b):[b e n & b<=s(x) => P(b)]

         

          Suppose...

 

            61    P(s(x))

              & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

                  Premise

 

            62    P(s(x))

                  Split, 61

 

            63    ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

                  Split, 61

 

          Prove: P(x)

         

          Apply premise

 

            64    x e n & x<s(x) => [P(s(x)) => P(x)]

                  U Spec, 63

 

          Apply property of < relation

 

            65    x e n => x<s(x)

                  U Spec, 11

 

            66    x<s(x)

                  Detach, 65, 53

 

            67    x e n & x<s(x)

                  Join, 53, 66

 

            68    P(s(x)) => P(x)

                  Detach, 64, 67

 

          As Required:

 

            69    P(x)

                  Detach, 68, 62

 

             

              Prove: ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

             

              Suppose...

 

                  70    y e n & y<x

                        Premise

 

                  71    y e n

                        Split, 70

 

                  72    y<x

                        Split, 70

 

              Apply premise

 

                  73    y e n & y<s(x) => [P(s(y)) => P(y)]

                        U Spec, 63

 

                  74    ALL(b):[y e n & b e n => [y<b => y<s(b)]]

                        U Spec, 9

 

                  75    y e n & x e n => [y<x => y<s(x)]

                        U Spec, 74

 

                  76    y e n & x e n

                        Join, 71, 53

 

                  77    y<x => y<s(x)

                        Detach, 75, 76

 

                  78    y<s(x)

                        Detach, 77, 72

 

                  79    y e n & y<s(x)

                        Join, 71, 78

 

                  80    P(s(y)) => P(y)

                        Detach, 73, 79

 

          As Required:

 

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

                  4 Conclusion, 70

 

          Joining results...

 

            82    P(x) & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

                  Join, 69, 81

 

          As Required:

 

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

                  Detach, 54, 82

 

             

              Prove: ALL(b):[b e n & b<=s(x) => P(b)]

             

              Suppose...

 

                  84    z e n & z<=s(x)

                        Premise

 

                  85    z e n

                        Split, 84

 

                  86    z<=s(x)

                        Split, 84

 

              Apply property of < and <= relations

 

                  87    ALL(b):[z e n & b e n => [z<=b <=> z<b | z=b]]

                        U Spec, 8

 

                  88    z e n & s(x) e n => [z<=s(x) <=> z<s(x) | z=s(x)]

                        U Spec, 87

 

                  89    z e n & s(x) e n

                        Join, 85, 60

 

                  90    z<=s(x) <=> z<s(x) | z=s(x)

                        Detach, 88, 89

 

                  91    [z<=s(x) => z<s(x) | z=s(x)]

                   & [z<s(x) | z=s(x) => z<=s(x)]

                        Iff-And, 90

 

                  92    z<=s(x) => z<s(x) | z=s(x)

                        Split, 91

 

                  93    z<s(x) | z=s(x) => z<=s(x)

                        Split, 91

 

              Two cases to consider:

 

                  94    z<s(x) | z=s(x)

                        Detach, 92, 86

 

                   Case 1

                  

                   Prove: z<s(x) => P(z)

                  

                   Suppose...

 

                        95    z<s(x)

                              Premise

 

                   Apply previous result

 

                        96    z e n & z<=x => P(z)

                              U Spec, 83

 

                   Apply property of < and <= relations

 

                        97    ALL(b):[z e n & b e n => [z<s(b) => z<=b]]

                              U Spec, 10

 

                        98    z e n & x e n => [z<s(x) => z<=x]

                              U Spec, 97

 

                        99    z e n & x e n

                              Join, 85, 53

 

                        100  z<s(x) => z<=x

                              Detach, 98, 99

 

                        101  z<=x

                              Detach, 100, 95

 

                        102  z e n & z<=x

                              Join, 85, 101

 

                        103  P(z)

                              Detach, 96, 102

 

              Case 1

             

              As Required:

 

                  104  z<s(x) => P(z)

                        4 Conclusion, 95

 

                   Case 2

                  

                   Prove: z=s(x) => P(z)

                  

                   Suppose...

 

                        105  z=s(x)

                              Premise

 

                        106  P(z)

                              Substitute, 105, 62

 

              Case 2

             

              As Required:

 

                  107  z=s(x) => P(z)

                        4 Conclusion, 105

 

              Joining results for Cases Rule

 

                  108  [z<s(x) => P(z)] & [z=s(x) => P(z)]

                        Join, 104, 107

 

                  109  P(z)

                        Cases, 94, 108

 

          As Required:

 

            110  ALL(b):[b e n & b<=s(x) => P(b)]

                  4 Conclusion, 84

 

     As Required:

 

      111  P(s(x))

          & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=s(x) => P(b)]

            4 Conclusion, 61

 

     Joining results...

 

      112  s(x) e n

          & [P(s(x))

          & ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=s(x) => P(b)]]

            Join, 60, 111

 

      113  s(x) e n'

            Detach, 58, 112

 

As Required:

 

114  ALL(b):[b e n' => s(b) e n']

      4 Conclusion, 47

 

Joining results...

 

115  0 e n' & ALL(b):[b e n' => s(b) e n']

      Join, 46, 114

 

As Required:

 

116  ALL(b):[b e n => b e n']

      Detach, 26, 115

 

    

     Prove: ALL(a):[a e n

            => [P(a) & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]

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

    

     Suppose...

 

      117  x e n

            Premise

 

      118  x e n => x e n'

            U Spec, 116

 

      119  x e n'

            Detach, 118, 117

 

      120  x e n' <=> x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            U Spec, 15

 

      121  [x e n' => x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

          & [x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=x => P(b)]] => x e n']

            Iff-And, 120

 

      122  x e n' => x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            Split, 121

 

      123  x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

          => ALL(b):[b e n & b<=x => P(b)]] => x e n'

            Split, 121

 

      124  x e n & [P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            Detach, 122, 119

 

      125  x e n

            Split, 124

 

      126  P(x)

          & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]

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

            Split, 124

 

As Required:

 

127  ALL(a):[a e n

     => [P(a)

     & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]

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

      4 Conclusion, 117