THEOREM

*******

The power set of the natural numbers is not countable.

OUTLINE

*******

Let pn be the power set of the set of natural numbers n.

By Lemma 5, there can exist no injection from pn to n.

By definition, pn is not countable .

(This proof was written 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

2     0 e n

      Axiom

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

      Axiom

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

      Axiom

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

      Axiom

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

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

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

      Axiom

Construct the power set of n

Apply the Power Set axiom

7     ALL(a):[Set(a) => EXIST(b):[Set(b)

     & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e a]]]]

      Power Set

8     Set(n) => EXIST(b):[Set(b)

     & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e n]]]

      U Spec, 7

9     EXIST(b):[Set(b)

     & ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e n]]]

      Detach, 8, 1

10    Set(pn)

     & ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]

      E Spec, 9

Define: pn  (the power set of n)

**********

11    Set(pn)

      Split, 10

12    ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]

      Split, 10

Define: Countable

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

A set x is countable if and only if there exists an injective (one-to-one) mapping

of x to the set of natural numbers.

13    ALL(a):[Countable(a) <=> EXIST(f):[ALL(b):[b e a => f(b) e n] & Injection(f,a,n)]]

      Axiom

PREVIOUS RESULT  (with link to proof)

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

Lemma 5:  Proof

Suppose ps is the power set of s.

Then there can be no injective (one-to-one) mapping of ps to s.

14    ALL(s):ALL(ps):[Set(s)

     & Set(ps)

     & ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]

     => ~EXIST(f):[ALL(c):[c e ps => f(c) e s] & Injection(f,ps,s)]]

      Axiom

PROOF OF THEOREM

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

Apply Lemma 5

15    ALL(ps):[Set(n)

     & Set(ps)

     & ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e n]]

     => ~EXIST(f):[ALL(c):[c e ps => f(c) e n] & Injection(f,ps,n)]]

      U Spec, 14

16    Set(n)

     & Set(pn)

     & ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]

     => ~EXIST(f):[ALL(c):[c e pn => f(c) e n] & Injection(f,pn,n)]

      U Spec, 15

17    Set(n) & Set(pn)

      Join, 1, 11

18    Set(n) & Set(pn)

     & ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]

      Join, 17, 12

From Lemma 5, we have...

19    ~EXIST(f):[ALL(c):[c e pn => f(c) e n] & Injection(f,pn,n)]

      Detach, 16, 18

Apply definition of Countable

20    Countable(pn) <=> EXIST(f):[ALL(b):[b e pn => f(b) e n] & Injection(f,pn,n)]

      U Spec, 13

21    [Countable(pn) => EXIST(f):[ALL(b):[b e pn => f(b) e n] & Injection(f,pn,n)]]

     & [EXIST(f):[ALL(b):[b e pn => f(b) e n] & Injection(f,pn,n)] => Countable(pn)]

      Iff-And, 20

22    Countable(pn) => EXIST(f):[ALL(b):[b e pn => f(b) e n] & Injection(f,pn,n)]

      Split, 21

23    EXIST(f):[ALL(b):[b e pn => f(b) e n] & Injection(f,pn,n)] => Countable(pn)

      Split, 21

Sufficient: For ~Countable(pn)

24    ~EXIST(f):[ALL(b):[b e pn => f(b) e n] & Injection(f,pn,n)] => ~Countable(pn)

      Contra, 22

As Required: pn is not countable

25    ~Countable(pn)

      Detach, 24, 19