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