Proving Pigeonhole Principle is Unsatisfiable

Question

Consider the resolution rule, that is, I can add a resolvent of any two clauses to the formula.

My question is: From using only this above rule how to show that the pigeon-hole formula for 3 pigeons and 2 holes is unsatisfiable?

Answer 1

To show that the pigeon-hole formula for 3 pigeons and 2 holes is unsatisfiable using the resolution rule, you can create clauses representing the conditions and then derive a contradiction.

Let $P(i, h)$ represent "Pigeon $i$ is in Hole $h$. The pigeon-hole formula constraints are:

1. each pigeon is in at least one hole.
2. no hole contains more than one pigeon.

Now, create the formulas:

1. For each pigeon, there must be a hole they are in: $(P(1, 1) ∨ P(1, 2)) ∧ (P(2, 1) ∨ P(2, 2)) ∧ (P(3, 1) ∨ P(3, 2))$

2. no hole contains more than one pigeon: $(\neg P(1,1)\lor\neg P(2,1))\land$ $(\neg P(1,2)\lor\neg P(2,2))\land$ $(\neg P(1,1)\lor\neg P(3,1))\land$ $(\neg P(1,2)\lor\neg P(3,2))\land$ $(\neg P(2,1)\lor\neg P(3,1))\land$ $(\neg P(2,2)\lor\neg P(3,2))$

Now, apply the resolution rule between all the causes above of formulas (1) and(2),I obtain an empty clause, $\phi$ (representing a contradiction). If you reach an empty clause, it implies that the initial set of clauses is unsatisfiable.

Answer 2

As requested (IIUC):

Not sure if this will help, but here is a non-numeric version of the PHP:

Suppose h: P → H (for non-empty P) and there exists no surjective function mapping H onto P (i.e. more pigeons than holes), then there exists x, y ∈ P such that x≠y and h(x)=h(y) (i.e. distinct pigeons x and y are in the same hole).

Formal proof (29 lines) available on request. Includes link to lemma (381 lines).