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