Applied Type Theory
Here is a fun little problem that is kind of related to Russell’s type theory.
100 crocodiles got together for a dinner. And they started to swallow one another. When the feast was over, one could observe that among any 10 of the crocodiles there had been an act of cannibalism. Prove that there exists a chain of 12 nested crocodiles.
Some of the crocodiles were either vegetarian or too slow, so they didn’t eat anyone. Let’s call them Type0 crocodiles. Those who ate only Type0 guys are called Type1. Those who ate only Type0 and Type1 belong to Type2, and so on.
Obviously, if one crocodile swallowed another then the type of the swallower is greater than the type of the swalowee. Therefore, it’s impossible to find 10 crocodiles that belong to the same type. And with the maximum of 9 members per type, and the total number of crocodiles being 100, we need at least 12 different types. (11 is not enough: 11*9=99). So there is at least one Type11 crocodile who earned his title by eating at least one Type10 crocodile, etc. QED.
The animal-friendly formulation is: In a partially ordered set of m*n+1 elements, there either exists a chain of m+1 elements or an anti-chain of n+1 elements. A chain is a subset where any two elements are comparable, and an anti-chain is a subset where no elements are comparable.