THEOREM

*******

 

Let P be a (non-empty) set of pigeons, and H a set of holes. Suppose each pigeon is put in a hole. Suppose

further that there are more pigeons than holes, i.e. that no function mapping holes to pigeons is surjective.

Then at least two pigeons will be in the same hole.

 

Formally:

 

     ALL(pigeons):ALL(holes):[Set(pigeons)

     & Set(holes)

     & EXIST(a):a e pigeons

     => ALL(f):[ALL(a):[a e pigeons => f(a) e holes]

     & ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]

 

     => EXIST(a):EXIST(b):EXIST(c):[a e pigeons & b e pigeons & c e holes

     & [~a=b & f(a)=c & f(b)=c]]]]

 

 

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

 

 

DEFINITIONS

***********

 

Define: Injection

 

1     ALL(f):ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]

      Axiom

 

Define: Surjection

 

2     ALL(f):ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]

      Axiom

 

 

PREVIOUS RESULT

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

 

Lemma 4

 

If there exists a infjective function f1 mapping non-empty set A to set B, then there exists a surjective

function mapping set B to Set A.

 

3     ALL(a):ALL(b):ALL(f1):[Set(a)

     & Set(b)

     & EXIST(c):c e a

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

     & Injection(f1,a,b)

     => EXIST(f2):[ALL(c):[c e b => f2(c) e a] & Surjection(f2,b,a)]]

      Axiom

 

    

     PROOF

     *****

    

     Suppose...

 

      4     Set(pigeons)

          & Set(holes)

          & EXIST(a):a e pigeons

            Premise

 

      5     Set(pigeons)

            Split, 4

 

      6     Set(holes)

            Split, 4

 

     Assume there is at least one pigeon.

 

      7     EXIST(a):a e pigeons

            Split, 4

 

         

          Prove: ALL(f):[ALL(a):[a e pigeons => f(a) e holes]

                 & ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]

         

                 => EXIST(a):EXIST(b):EXIST(c):[a e pigeons & b e pigeons & c e holes

                 & [~a=b & f(a)=c & f(b)=c]]]

         

          Suppose...

 

            8     ALL(a):[a e pigeons => f(a) e holes]

              & ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]

                  Premise

 

          Each pigeon is put into a hole

 

            9     ALL(a):[a e pigeons => f(a) e holes]

                  Split, 8

 

          There are more pigeons than holes

 

            10    ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]

                  Split, 8

 

             

              Prove: EXIST(h):[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

             

                     => EXIST(f2):[ALL(c):[c e holes => f2(c) e pigeons] & Surjection(f2,holes,pigeons)]

             

              Suppose...

 

                  11    EXIST(h):[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

                        Premise

 

                  12    ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)

                        E Spec, 11

 

                  13    ALL(a):[a e pigeons => h(a) e holes]

                        Split, 12

 

                  14    Injection(h,pigeons,holes)

                        Split, 12

 

               Apply Lemma 4

 

                  15    ALL(b):ALL(f1):[Set(pigeons)

                   & Set(b)

                   & EXIST(c):c e pigeons

                   & ALL(c):[c e pigeons => f1(c) e b]

                   & Injection(f1,pigeons,b)

                   => EXIST(f2):[ALL(c):[c e b => f2(c) e pigeons] & Surjection(f2,b,pigeons)]]

                        U Spec, 3

 

                  16    ALL(f1):[Set(pigeons)

                   & Set(holes)

                   & EXIST(c):c e pigeons

                   & ALL(c):[c e pigeons => f1(c) e holes]

                   & Injection(f1,pigeons,holes)

                   => EXIST(f2):[ALL(c):[c e holes => f2(c) e pigeons] & Surjection(f2,holes,pigeons)]]

                        U Spec, 15

 

                  17    Set(pigeons)

                   & Set(holes)

                   & EXIST(c):c e pigeons

                   & ALL(c):[c e pigeons => h(c) e holes]

                   & Injection(h,pigeons,holes)

                   => EXIST(f2):[ALL(c):[c e holes => f2(c) e pigeons] & Surjection(f2,holes,pigeons)]

                        U Spec, 16

 

                  18    Set(pigeons)

                   & Set(holes)

                   & EXIST(a):a e pigeons

                   & ALL(a):[a e pigeons => h(a) e holes]

                        Join, 4, 13

 

                  19    Set(pigeons)

                   & Set(holes)

                   & EXIST(a):a e pigeons

                   & ALL(a):[a e pigeons => h(a) e holes]

                   & Injection(h,pigeons,holes)

                        Join, 18, 14

 

                  20    EXIST(f2):[ALL(c):[c e holes => f2(c) e pigeons] & Surjection(f2,holes,pigeons)]

                        Detach, 17, 19

 

          As Required:

 

            21    EXIST(h):[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

              => EXIST(f2):[ALL(c):[c e holes => f2(c) e pigeons] & Surjection(f2,holes,pigeons)]

                  4 Conclusion, 11

 

         

          Prove: ~Injection(f,pigeons,holes)

 

            22    ~EXIST(f2):[ALL(c):[c e holes => f2(c) e pigeons] & Surjection(f2,holes,pigeons)]

               => ~EXIST(h):[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

                  Contra, 21

 

            23    ~~ALL(f2):~[ALL(c):[c e holes => f2(c) e pigeons] & Surjection(f2,holes,pigeons)]

               => ~EXIST(h):[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

                  Quant, 22

 

            24    ALL(f2):~[ALL(c):[c e holes => f2(c) e pigeons] & Surjection(f2,holes,pigeons)]

               => ~EXIST(h):[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

                  Rem DNeg, 23

 

            25    ALL(f2):~~[ALL(c):[c e holes => f2(c) e pigeons] => ~Surjection(f2,holes,pigeons)]

               => ~EXIST(h):[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

                  Imply-And, 24

 

            26    ALL(f2):[ALL(c):[c e holes => f2(c) e pigeons] => ~Surjection(f2,holes,pigeons)]

               => ~EXIST(h):[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

                  Rem DNeg, 25

 

            27    ALL(f2):[ALL(c):[c e holes => f2(c) e pigeons] => ~Surjection(f2,holes,pigeons)]

               => ~~ALL(h):~[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

                  Quant, 26

 

            28    ALL(f2):[ALL(c):[c e holes => f2(c) e pigeons] => ~Surjection(f2,holes,pigeons)]

               => ALL(h):~[ALL(a):[a e pigeons => h(a) e holes] & Injection(h,pigeons,holes)]

                  Rem DNeg, 27

 

            29    ALL(f2):[ALL(c):[c e holes => f2(c) e pigeons] => ~Surjection(f2,holes,pigeons)]

               => ALL(h):~~[ALL(a):[a e pigeons => h(a) e holes] => ~Injection(h,pigeons,holes)]

                  Imply-And, 28

 

            30    ALL(f2):[ALL(c):[c e holes => f2(c) e pigeons] => ~Surjection(f2,holes,pigeons)]

               => ALL(h):[ALL(a):[a e pigeons => h(a) e holes] => ~Injection(h,pigeons,holes)]

                  Rem DNeg, 29

 

            31    ALL(h):[ALL(a):[a e pigeons => h(a) e holes] => ~Injection(h,pigeons,holes)]

                  Detach, 30, 10

 

            32    ALL(a):[a e pigeons => f(a) e holes] => ~Injection(f,pigeons,holes)

                  U Spec, 31

 

          As Required:

 

            33    ~Injection(f,pigeons,holes)

                  Detach, 32, 9

 

         

          Prove: EXIST(c):EXIST(d):[c e pigeons & d e pigeons & [f(c)=f(d) & ~c=d]]

         

          Apply definition of Injection

 

            34    ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]

                  U Spec, 1

 

            35    ALL(b):[Injection(f,pigeons,b) <=> ALL(c):ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]]

                  U Spec, 34

 

            36    Injection(f,pigeons,holes) <=> ALL(c):ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]

                  U Spec, 35

 

            37    [Injection(f,pigeons,holes) => ALL(c):ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]]

              & [ALL(c):ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]] => Injection(f,pigeons,holes)]

                  Iff-And, 36

 

            38    Injection(f,pigeons,holes) => ALL(c):ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]

                  Split, 37

 

            39    ALL(c):ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]] => Injection(f,pigeons,holes)

                  Split, 37

 

            40    ~Injection(f,pigeons,holes) => ~ALL(c):ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]

                  Contra, 39

 

            41    ~ALL(c):ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]

                  Detach, 40, 33

 

            42    ~~EXIST(c):~ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]

                  Quant, 41

 

            43    EXIST(c):~ALL(d):[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]

                  Rem DNeg, 42

 

            44    EXIST(c):~~EXIST(d):~[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]

                  Quant, 43

 

            45    EXIST(c):EXIST(d):~[c e pigeons & d e pigeons => [f(c)=f(d) => c=d]]

                  Rem DNeg, 44

 

            46    EXIST(c):EXIST(d):~~[c e pigeons & d e pigeons & ~[f(c)=f(d) => c=d]]

                  Imply-And, 45

 

            47    EXIST(c):EXIST(d):[c e pigeons & d e pigeons & ~[f(c)=f(d) => c=d]]

                  Rem DNeg, 46

 

            48    EXIST(c):EXIST(d):[c e pigeons & d e pigeons & ~~[f(c)=f(d) & ~c=d]]

                  Imply-And, 47

 

          As Required:

 

            49    EXIST(c):EXIST(d):[c e pigeons & d e pigeons & [f(c)=f(d) & ~c=d]]

                  Rem DNeg, 48

 

         

          Prove: EXIST(a):EXIST(b):EXIST(c):[a e pigeons & b e pigeons & c e holes & [~a=b & f(a)=c & f(b)=c]]

         

          Apply previous result

 

            50    EXIST(d):[x e pigeons & d e pigeons & [f(x)=f(d) & ~x=d]]

                  E Spec, 49

 

            51    x e pigeons & y e pigeons & [f(x)=f(y) & ~x=y]

                  E Spec, 50

 

            52    x e pigeons

                  Split, 51

 

            53    y e pigeons

                  Split, 51

 

            54    f(x)=f(y) & ~x=y

                  Split, 51

 

            55    f(x)=f(y)

                  Split, 54

 

            56    ~x=y

                  Split, 54

 

            57    f(y)=f(x)

                  Sym, 55

 

            58    f(x)=f(x)

                  Reflex

 

            59    x e pigeons => f(x) e holes

                  U Spec, 9

 

            60    f(x) e holes

                  Detach, 59, 52

 

            61    x e pigeons & y e pigeons

                  Join, 52, 53

 

            62    x e pigeons & y e pigeons & f(x) e holes

                  Join, 61, 60

 

            63    ~x=y & f(x)=f(x)

                  Join, 56, 58

 

            64    ~x=y & f(x)=f(x) & f(y)=f(x)

                  Join, 63, 57

 

            65    x e pigeons & y e pigeons & f(x) e holes

              & [~x=y & f(x)=f(x) & f(y)=f(x)]

                  Join, 62, 64

 

            66    EXIST(c):[x e pigeons & y e pigeons & c e holes

              & [~x=y & f(x)=c & f(y)=c]]

                  E Gen, 65

 

            67    EXIST(b):EXIST(c):[x e pigeons & b e pigeons & c e holes

              & [~x=b & f(x)=c & f(b)=c]]

                  E Gen, 66

 

          As Required:

 

            68    EXIST(a):EXIST(b):EXIST(c):[a e pigeons & b e pigeons & c e holes

              & [~a=b & f(a)=c & f(b)=c]]

                  E Gen, 67

 

    

     As Required:

 

      69    ALL(f):[ALL(a):[a e pigeons => f(a) e holes]

          & ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]

          => EXIST(a):EXIST(b):EXIST(c):[a e pigeons & b e pigeons & c e holes

          & [~a=b & f(a)=c & f(b)=c]]]

            4 Conclusion, 8

 

 

As Required:

 

70    ALL(pigeons):ALL(holes):[Set(pigeons)

     & Set(holes)

     & EXIST(a):a e pigeons

     => ALL(f):[ALL(a):[a e pigeons => f(a) e holes]

     & ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]

     => EXIST(a):EXIST(b):EXIST(c):[a e pigeons & b e pigeons & c e holes

     & [~a=b & f(a)=c & f(b)=c]]]]

      4 Conclusion, 4