Dedekind's Pigeons

10 pigeons in 9 pigeonholes.

Photo credit: WikipediaThe 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

finitenumber of objects" and by "asmallernumber of categories." In most textbooks, these concepts are based on the numerical size of a set (thenumberof 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

Xis infinite if and only if there exists a proper subsetYofXand abijectionfmappingXtoY.The negation of infinite defines finiteness:

A set

Xis finite if and only if there exists no proper subsetYofXand bijectionfmappingXtoY.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

xis a setInfinite(x) means

xis infiniteBijection(x,y) means there exists a bijective function mapping set

xto sety.Note: Bijection is an equivalence relation. It is reflexive, symmetry and transitive.Finite(x)means

xis finiteALL(c):[c e a => f(c) e b] means

fis a function mapping setato setb.In the language of pigeons and pigeonholes,ais the set of pigeons, andbis the set of pigeonholes. The functionfassigns 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

gisnota surjective (onto) function and that setais larger than setb. In the language of pigeons and pigeonholes,geffectively 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 thatanypigeon 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

awhich have the same image under functionf.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