The pigeonhole problem involves showing that it is impossible to put pigeons
into holes if each pigeon must go into a distinct hole. If we
write for the fact that pigeon is in hole , then a
straightforward axiomatization says that every pigeon must be in at
least one hole:
It is well known that there is no polynomial-sized proof of the unsatisfiability of the axioms (9)-(10) [HakenHaken1985]. The proof is technical, but the essential reason is that the pigeonhole problem is ``all about'' counting. At some point, proving that you can't put pigeons into holes requires saying that you can't put pigeons into the last holes, thus pigeons into the last holes, and so on. Saying this in the language of SAT is awkward, and it is possible to show that no proof of the pigeonhole problem can be completed without, at some point, working with extremely long individual clauses. Once again, we see the connection to expressive efficiency; for readers interested in additional details, Pitassi's Pitassi:complexity explanation is reasonably accessible.