THEOREM

*******

The null (empty) set is finite

Finite(null)

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

Dan Christensen

2019-12-09

DEFINITIONS

***********

Define: Finite set

A set X is said to be finite if and only if, for all functions f: X --> X, if f is injective (1-1) then it must be surjective.

1 ALL(a):[Set(a) => [Finite(a) <=> ALL(f):[ALL(b):[b e a => f(b) e a]

=> [ALL(b):ALL(c):[b e a & c e a => [f(b)=f(c) => b=c]]

=> ALL(b):[b e a => EXIST(c):[c e a & f(c)=b]]]]]]

Axiom

Define: Null (empty) set

2 Set(null)

Axiom

3 ALL(a):~a e null

Axiom

PROOF

*****

Apply definition of Finite set for the null set

4 Set(null) => [Finite(null) <=> ALL(f):[ALL(b):[b e null => f(b) e null]

=> [ALL(b):ALL(c):[b e null & c e null => [f(b)=f(c) => b=c]]

=> ALL(b):[b e null => EXIST(c):[c e null & f(c)=b]]]]]

U Spec, 1

5 Finite(null) <=> ALL(f):[ALL(b):[b e null => f(b) e null]

=> [ALL(b):ALL(c):[b e null & c e null => [f(b)=f(c) => b=c]]

=> ALL(b):[b e null => EXIST(c):[c e null & f(c)=b]]]]

Detach, 4, 2

6 [Finite(null) => ALL(f):[ALL(b):[b e null => f(b) e null]

=> [ALL(b):ALL(c):[b e null & c e null => [f(b)=f(c) => b=c]]

=> ALL(b):[b e null => EXIST(c):[c e null & f(c)=b]]]]]

& [ALL(f):[ALL(b):[b e null => f(b) e null]

=> [ALL(b):ALL(c):[b e null & c e null => [f(b)=f(c) => b=c]]

=> ALL(b):[b e null => EXIST(c):[c e null & f(c)=b]]]] => Finite(null)]

Iff-And, 5

Sufficient: For Finite(null)

7 ALL(f):[ALL(b):[b e null => f(b) e null]

=> [ALL(b):ALL(c):[b e null & c e null => [f(b)=f(c) => b=c]]

=> ALL(b):[b e null => EXIST(c):[c e null & f(c)=b]]]] => Finite(null)

Split, 6

Suppose...

8 ALL(b):[b e null => f(b) e null]

Premise

Suppose...

9 ALL(b):ALL(c):[b e null & c e null => [f(b)=f(c) => b=c]]

Premise

Suppose...

10 y e null

Premise

Apply definition of null set

11 ~y e null

U Spec, 3

12 ~y e null => EXIST(c):[c e null & f(c)=y]

Arb Cons, 10

13 EXIST(c):[c e null & f(c)=y]

Detach, 12, 11

As Required:

14 ALL(b):[b e null => EXIST(c):[c e null & f(c)=b]]

4 Conclusion, 10

As Required:

15 ALL(b):ALL(c):[b e null & c e null => [f(b)=f(c) => b=c]]

=> ALL(b):[b e null => EXIST(c):[c e null & f(c)=b]]

4 Conclusion, 9

As Required:

16 ALL(f):[ALL(b):[b e null => f(b) e null]

=> [ALL(b):ALL(c):[b e null & c e null => [f(b)=f(c) => b=c]]

=> ALL(b):[b e null => EXIST(c):[c e null & f(c)=b]]]]

4 Conclusion, 8

As Required:

17 Finite(null)

Detach, 7, 16