[HN Gopher] The undeserved status of the pigeon-hole principle (...
___________________________________________________________________
The undeserved status of the pigeon-hole principle (1991)
Author : rutenspitz
Score : 28 points
Date : 2020-07-03 19:02 UTC (1 days ago)
(HTM) web link (www.cs.utexas.edu)
(TXT) w3m dump (www.cs.utexas.edu)
| wizzwizz4 wrote:
| This isn't exclusive to the Pigeon-hole Principle, either. Many
| named conjectures are pointlessly used, just because they're
| named, even when it makes the proof longer.
|
| This isn't just exclusive to mathematics. It's similar to the
| reason people bring in single-line Node.JS packages; a fear of
| re-inventing the wheel when they don't actually need a wheel in
| the first place, or when the wheel is trivial to re-state in a
| more natural form for the proof / program.
| morelisp wrote:
| A couple thoughts:
|
| a) The history of mathematics is littered with examples of
| assumed "obvious" results that turned out to have drastic
| implications. This is especially true of combinatorics, which was
| blissfully ignorant to the axiom of choice for so long and now
| must wrestle with it forever. Strict adherence to some formalism
| may be justifiably understood, and it's a little shocking to find
| EWD of all people arguing otherwise for such a pragmatic reason
| as pedagogical clarity.
|
| b) Comparing 0) and 1) as EWD suggests, the first thing I notice
| is the sudden appearance of the word "finite" which never appears
| again in the article (nor in negation; also the inelegant but
| mostly harmless introduction of "nonempty"). The generalization
| of the principle to support reals costs it its trivial
| generalization over infinite bags, which is also often valuable
| (a classic example being Siegel's lemma).
| ogogmad wrote:
| How does combinatorics use the axiom of choice? Doesn't
| combinatorics deal with discrete and finite objects?
| jmount wrote:
| I feel this is an instance of prof.dr. Edsger W.Dijkstra just
| being mean. If one works more on pigeon-hole principles you end
| up with Ramsey Theory, which covers some amazing results.
| joe_the_user wrote:
| Yeah, this feel like a comment that might have been OK at a
| cocktail party or made offhand in the middle of an essay on
| something else.
|
| Sure, maybe, in some instances, some people, might, perhaps
| make a little too much out of using the pigeon hole principle.
| But here, _he_ make too much out of that situation.
| pinewurst wrote:
| It wouldn't be the only one. Review his archived papers and
| they're well salted with snark.
| neel_k wrote:
| This note represents a rare misstep by Dijkstra: the pigeonhole
| principle actually is a special and important principle worthy of
| a special name of its own. For example:
|
| 1. When you formulate the pigeonhole principle in propositional
| logic, its resolution proofs are exponentially large. Since
| modern SAT solvers are basically very fancy propositional
| resolution provers, this gives you a nice way to find hard
| instances for them. It also makes the question of when
| propositional proof systems can be more succinct than one another
| is also a fundamental question in complexity theory.
|
| 2. It also arises in geometry: a compactness for metric spaces is
| essentially the statement that the pigeonhole principle applies
| to the space.
|
| I don't have a unified perspective of these two facts, but either
| one of them is really striking. As a result I'm okay with giving
| the pigeonhole principle its own natural language name.
| ogogmad wrote:
| Do you have a reference for 2? Thanks.
| tprice7 wrote:
| The fact that every infinite sequence of points in a compact
| metric space has a cluster point is sort of like the
| pigeonhole principle. The grandparent comment in my opinion
| makes much more sense if the phrase "a compactness for metric
| spaces" is replaced by "sequential compactness for metric
| spaces".
| neel_k wrote:
| Willie Wong wrote a nice blog post about this a while ago:
|
| https://williewong.wordpress.com/2010/03/18/compactness-
| part...
___________________________________________________________________
(page generated 2020-07-04 23:00 UTC)