THEOREM

*******

 

If we have more pigeons that pigeonholes, and we put each pigeon into one of those pigeonholes, then there will

be at least two pigeons in the same hole.

 

This formal proof makes no use of the numbers, induction or cardinality -- just basic set theory and logic.

There is no requirement that the sets of pigeons and pigeonholes be finite.

 

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

     & EXIST(c):c e pigeons

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

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

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

 

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

 

By Dan Christensen

2022-06-05

 

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

 

 

Previous Result

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

 

For non-empty x and injective f1: x --> y, there exists a surjective f2: y --> x.   Proof Here

 

1     ALL(a):ALL(b):ALL(f1):[Set(a) & EXIST(c):c e a & Set(b)

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

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

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

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

      Axiom

 

   

    PROOF

    *****

 

Suppose we have:

 

      2     Set(pigeons) & Set(holes)

         & EXIST(c):c e pigeons

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

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

            Premise

 

      3     Set(pigeons)

            Split, 2

 

      4     Set(holes)

            Split, 2

 

   

    There is at least one pigeon

 

      5     EXIST(c):c e pigeons

            Split, 2

 

   

    Each pigeon is put into a hole. h(x)=y means pigeon x is put in hole y

 

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

            Split, 2

 

   

    There are more pigeons than holes, i.e. there exists no surjective function

    mapping the set of holes ONTO the set of pigeons.

 

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

            Split, 2

 

        

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

        

         Suppose to the contrary...

 

            8     ~EXIST(c):EXIST(d):[c e pigeons & d e pigeons & [h(c)=h(d) & ~c=d]]

                  Premise

 

         Apply previous result

 

            9     ALL(b):ALL(f1):[Set(pigeons) & EXIST(c):c e pigeons & Set(b)

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

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

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

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

                  U Spec, 1

 

            10   ALL(f1):[Set(pigeons) & EXIST(c):c e pigeons & Set(holes)

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

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

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

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

                  U Spec, 9

 

            11   Set(pigeons) & EXIST(c):c e pigeons & Set(holes)

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

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

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

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

                  U Spec, 10

 

         Change quantifiers in premise

 

            12   ~~ALL(c):~EXIST(d):[c e pigeons & d e pigeons & [h(c)=h(d) & ~c=d]]

                  Quant, 8

 

            13   ALL(c):~EXIST(d):[c e pigeons & d e pigeons & [h(c)=h(d) & ~c=d]]

                  Rem DNeg, 12

 

            14   ALL(c):~~ALL(d):~[c e pigeons & d e pigeons & [h(c)=h(d) & ~c=d]]

                  Quant, 13

 

            15   ALL(c):ALL(d):~[c e pigeons & d e pigeons & [h(c)=h(d) & ~c=d]]

                  Rem DNeg, 14

 

            16   ALL(c):ALL(d):~~[c e pigeons & d e pigeons => ~[h(c)=h(d) & ~c=d]]

                  Imply-And, 15

 

            17   ALL(c):ALL(d):[c e pigeons & d e pigeons => ~[h(c)=h(d) & ~c=d]]

                  Rem DNeg, 16

 

            18   ALL(c):ALL(d):[c e pigeons & d e pigeons => ~~[h(c)=h(d) => ~~c=d]]

                  Imply-And, 17

 

            19   ALL(c):ALL(d):[c e pigeons & d e pigeons => [h(c)=h(d) => ~~c=d]]

                  Rem DNeg, 18

 

        

         h is injective

 

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

                  Rem DNeg, 19

 

         Joining results...

 

            21   Set(pigeons) & EXIST(c):c e pigeons

                  Join, 3, 5

 

            22   Set(pigeons) & EXIST(c):c e pigeons & Set(holes)

                  Join, 21, 4

 

            23   Set(pigeons) & EXIST(c):c e pigeons & Set(holes)

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

                  Join, 22, 6

 

            24   Set(pigeons) & EXIST(c):c e pigeons & Set(holes)

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

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

                  Join, 23, 20

 

            25   EXIST(f2):[ALL(c):[c e holes => f2(c) e pigeons]

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

                  Detach, 11, 24

 

         Obtain the contradiction:

 

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

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

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

                  Join, 7, 25

 

      27   ~~EXIST(c):EXIST(d):[c e pigeons & d e pigeons & [h(c)=h(d) & ~c=d]]

            4 Conclusion, 8

 

    As Required:

 

      28   EXIST(c):EXIST(d):[c e pigeons & d e pigeons & [h(c)=h(d) & ~c=d]]

            Rem DNeg, 27

 

 

As Required:

 

29   ALL(pigeons):ALL(holes):ALL(h):[Set(pigeons) & Set(holes)

    & EXIST(c):c e pigeons

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

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

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

      4 Conclusion, 2