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