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