Non-numeric Pigeonhole Principle -- Formal proof in DCProof format (revised)

[Dan Christensen]

Some background: https://en.wikipedia.org/wiki/Pigeonhole_principle

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 in pigeons
=> ALL(f):[ALL(a):[a in pigeons => f(a) in holes]
& ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]

=> EXIST(a):EXIST(b):EXIST(c):[a in pigeons & b in pigeons & c in holes
& [~a=b & f(a)=c & f(b)=c]]]]

where

Set(pigeons) means pigeons is as set

Surjection(g,holes, pigeons) means the function g mapping holes to pigeons is surjective

Full text of proof: http://dcproof.com/pigeonhole.htm (70 lines)

Note: Since upgrading to Windows 10, some browsers do not correctly translate special characters, e.g. epsilon is displayed as "e", right triangle displayed as "4". Everything displays properly on MS Edge.


Dan

Download my DC Proof 2.0 software at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[k***@gmail.com]

Post by Dan Christensen
Some background: https://en.wikipedia.org/wiki/Pigeonhole_principle

Do you have a proof of the "numeric" version?

Post by Dan Christensen
snipped

[Dan Christensen]

Post by k***@gmail.com

Post by Dan Christensen
Some background: https://en.wikipedia.org/wiki/Pigeonhole_principle

Do you have a proof of the "numeric" version?

Post by Dan Christensen
snipped

Sorry, no.


Dan

Download my DC Proof 2.0 software at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Dan Christensen]

Post by k***@gmail.com

Post by Dan Christensen
Some background: https://en.wikipedia.org/wiki/Pigeonhole_principle

Do you have a proof of the "numeric" version?

Post by Dan Christensen
snipped

All you would need to prove (assume?) is that if there are numerically more pigeons than holes, then no function mapping holes to pigeons would be surjective.


Dan

Download my DC Proof 2.0 software at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Ross A. Finlayson]

But, a bijection is a surjection.

[Dan Christensen]

Post by Ross A. Finlayson
But, a bijection is a surjection.

A bijection is both a surjection and an injection.


Dan

[g***@aol.com]

Post by Dan Christensen
Some background: https://en.wikipedia.org/wiki/Pigeonhole_principle
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.
ALL(pigeons):ALL(holes):[Set(pigeons)
& Set(holes)
& EXIST(a):a in pigeons
=> ALL(f):[ALL(a):[a in pigeons => f(a) in holes]
& ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]
=> EXIST(a):EXIST(b):EXIST(c):[a in pigeons & b in pigeons & c in holes
& [~a=b & f(a)=c & f(b)=c]]]]
where
Set(pigeons) means pigeons is as set
Surjection(g,holes, pigeons) means the function g mapping holes to pigeons is surjective
Full text of proof: http://dcproof.com/pigeonhole.htm (70 lines)

70 lines seems excessive! How about:

Since P is non-empty, we can select a particular pigeon p1.

Now define a function g: H -> P as follows:

If a hole h contains exactly one pigeon p, then g(h) = p.

Otherwise (ie hole h is empty, or has more than one pigeon) g(h) = p1.

g is not a surjection. So there is at least one pigeon px which is in P but not in g(H).

px can't be in a hole by itself, or in an empty hole, so it must be in with another pigeon. QED.

[Dan Christensen]

Post by g***@aol.com

Post by Dan Christensen
Some background: https://en.wikipedia.org/wiki/Pigeonhole_principle
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.
ALL(pigeons):ALL(holes):[Set(pigeons)
& Set(holes)
& EXIST(a):a in pigeons
=> ALL(f):[ALL(a):[a in pigeons => f(a) in holes]
& ALL(g):[ALL(c):[c e holes => g(c) e pigeons] => ~Surjection(g,holes,pigeons)]
=> EXIST(a):EXIST(b):EXIST(c):[a in pigeons & b in pigeons & c in holes
& [~a=b & f(a)=c & f(b)=c]]]]
where
Set(pigeons) means pigeons is as set
Surjection(g,holes, pigeons) means the function g mapping holes to pigeons is surjective
Full text of proof: http://dcproof.com/pigeonhole.htm (70 lines)

70 lines seems excessive!

It's a formal proof. They can be 10 or more times longer that the usual informal proofs in most textbooks. On the upside, it pretty much eliminates any possibility of hand waving and allows for automated verification of proofs.


Dan

Download my DC Proof 2.0 software at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

Post by g***@aol.com
Since P is non-empty, we can select a particular pigeon p1.
If a hole h contains exactly one pigeon p, then g(h) = p.
Otherwise (ie hole h is empty, or has more than one pigeon) g(h) = p1.
g is not a surjection. So there is at least one pigeon px which is in P but not in g(H).
px can't be in a hole by itself, or in an empty hole, so it must be in with another pigeon. QED.