THEOREM

*******

 

There exists infinitely many exponent-like functions starting at exponent 2.

 

 

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

 

Dan Christensen

2019-10-16

 

 

PREVIOUS RESULTS

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

 

There exists infinitely many exponent-like functions starting at exponent zero.      Proof

 

1     ALL(x0):[x0 e n

    => EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

    & exp(0,0)=x0

    & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

    & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]

      Axiom

 

 

Starting at exponent zero is equivalent to starting at exponent two.                  Proof

 

2     ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

    => [ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

    => [ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

    <=> ALL(a):[a e n => exp(a,2)=a*a]]]]

      Axiom

 

   

    PROOF

    *****

   

    Suppose...

 

      3     x0 e n

            Premise

 

    Apply previous result

 

      4     x0 e n

         => EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]

            U Spec, 1

 

      5     EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]

            Detach, 4, 3

 

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

         & exp(0,0)=x0

         & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

            E Spec, 5

 

   

    Define: exp

 

      7     ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

            Split, 6

 

      8     exp(0,0)=x0

            Split, 6

 

      9     ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

            Split, 6

 

      10   ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

            Split, 6

 

   

    Apply previous result

 

      11   ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         => [ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

         => [ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         <=> ALL(a):[a e n => exp(a,2)=a*a]]]

            U Spec, 2

 

      12   ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

         => [ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         <=> ALL(a):[a e n => exp(a,2)=a*a]]

            Detach, 11, 7

 

      13   ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         <=> ALL(a):[a e n => exp(a,2)=a*a]

            Detach, 12, 10

 

      14   [ALL(a):[a e n => [~a=0 => exp(a,0)=1]] => ALL(a):[a e n => exp(a,2)=a*a]]

         & [ALL(a):[a e n => exp(a,2)=a*a] => ALL(a):[a e n => [~a=0 => exp(a,0)=1]]]

            Iff-And, 13

 

      15   ALL(a):[a e n => [~a=0 => exp(a,0)=1]] => ALL(a):[a e n => exp(a,2)=a*a]

            Split, 14

 

      16   ALL(a):[a e n => exp(a,2)=a*a] => ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

            Split, 14

 

      17   ALL(a):[a e n => exp(a,2)=a*a]

            Detach, 15, 9

 

    Joining results...

 

      18   ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

            Join, 7, 8

 

      19   ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => exp(a,2)=a*a]

            Join, 18, 17

 

      20   ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => exp(a,2)=a*a]

         & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

            Join, 19, 10

 

 

As Required:

 

21   ALL(x0):[x0 e n

    => EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

    & exp(0,0)=x0

    & ALL(a):[a e n => exp(a,2)=a*a]

    & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]

      4 Conclusion, 3