Dedekind's Pigeons
10 pigeons in 9 pigeonholes.
Photo credit:
Wikipedia
The Pigeonhole Principle states that if you have more pigeons than pigeonholes, then at least two pigeons will end up in the same hole (see photo, 2 pigeons in top left corner).
More generally, if a finite number of objects are put into a smaller number of categories, then there would have to be least 2 of those objects in the same category.
In a formal proof using the Pigeonhole Principle, we would have to be explicit about what you meant by "a finite number of objects" and by "a smaller number of categories." In most textbooks, these concepts are based on the numerical size of a set (the number of objects in the set). In a formal proof based on this notion, all of the machinery of natural number arithmetic would have to be constructed and the results included in the proof as well.
Alternatively, we can can use Richard Dedekind's elegant definition of the infinite:
A set X is infinite if and only if there exists a proper subset Y of X and a bijection f mapping X to Y.
The negation of infinite defines finiteness:
A set X is finite if and only if there exists no proper subset Y of X and bijection f mapping X to Y.
We have the following formalisms in DC Proof notation:
The definition of infinite:
ALL(a):[Set(a) => [Infinite(a)
<=> EXIST(b):[Set(b)
& ALL(c):[c
e b => c
e a]
& EXIST(c):[c
e a & ~c
e b]
& Bijection(a,b)]]]
The definition of bijection:
ALL(a):ALL(b):[Set(a)
& Set(b) => [Bijection(a,b)
<=>
EXIST(f):[ALL(c):[c e
a => f(c)
e b]
& [ALL(c):ALL(d):[c
e a & d
e a => [f(c)=f(d) =>
c=d]]
& ALL(c):[c
e b => EXIST(d):[d
e a & f(d)=c]]]]]]
The definition of finite:
ALL(a):[Set(a) => [Finite(a) <=> ~Infinite(a)]]
The Pigeonhole Principle:
ALL(a):ALL(b):ALL(f):ALL(g):[Set(a)
& Set(b)
& Finite(a)
& ALL(c):[c
e a => f(c)
e b]
& ALL(c):[c e
b => g(c)
e a]
& ALL(c):ALL(d):[c e
b & d
e b => [g(c)=g(d) =>
c=d]]
& EXIST(c):[c e
a & ALL(d):[d
e b => ~g(d)=c]]
=> EXIST(c):EXIST(d):[c
e a & d
e a & [f(c)=f(d) &
~c=d]]]
where
Set(x) means x is a set
Infinite(x) means x is infinite
Bijection(x,y) means there exists a bijective function mapping set x to set y. Note: Bijection is an equivalence relation. It is reflexive, symmetry and transitive.
Finite(x)means x is finite
ALL(c):[c e a => f(c) e b] means f is a function mapping set a to set b. In the language of pigeons and pigeonholes, a is the set of pigeons, and b is the set of pigeonholes. The function f assigns each pigeon to a unique hole.
ALL(c):ALL(d):[c e b & d e b => [g(c)=g(d) => c=d]] means g is a injective (one-to-one) function.
EXIST(c):[c e a & ALL(d):[d e b => ~g(d)=c]] means g is not a surjective (onto) function and that set a is larger than set b. In the language of pigeons and pigeonholes, g effectively names each hole after a pigeon. In a sense, it converts the set of holes into a set of pigeons. This is necessary if we want to apply the definition of Dedekind-finiteness. Since there are more pigeons than holes, at least one pigeon will not have a hole named after it. Note that any pigeon may or may not be assigned to the hole named after it.
EXIST(c):EXIST(d):[c e a & d e a & [f(c)=f(d) & ~c=d]]] means there exists at least two distinct elements of set a which have the same image under function f. In the language of pigeons and pigeonholes, there exists at least two pigeons that will be assigned to same hole.
For a formal development of the pigeonhole principle using the definition of Dedekind-infinity, see pigeonhole.htm
