# Buss' Polynomial-Size Frege Proof of the Propositional Pigeonhole Principle

S. Buss described a polynomial-size Frege proof of the propositional pigeonhole principle in the paper Polynomial size proofs of the propositional pigeonhole principle (the definition of the Frege proof system can be found in the paper). I found the proof very abstract, so I want to instantiate the proof in the case that $$n=3$$ (i.e., $$3$$ pigeons fly into $$2$$ holes). Define propositional variables $$a,b,c,d,e,f$$, where

• $$a,b$$ stands for pigeon $$0$$ flies into hole $$0,1$$, repectively;
• $$c,d$$ stands for pigeon $$1$$ flies into hole $$0,1$$, repectively;
• $$e,f$$ stands for pigeon $$2$$ flies into hole $$0,1$$, repectively.

Then the pigeonhole principle, i.e., that there must be some hole containing at least two pigeons can be formulated as

$$\mathrm{PHP}_3=(a\lor b)\land (c\lor d)\land (e\lor f)\to (a\land c)\lor(a\land e)\lor(c\land e)\lor(b\land d)\lor(b\land f)\lor(d\land f)$$

For example, $$c\lor d$$ means pigeon $$1$$ must fly into at least one pigeon, and $$b\land d$$ means hole $$1$$ contains both pigeon $$0$$ and pigeon $$1$$. To prove $$\mathrm{PHP}_3$$ is a tautology is to prove that $$\neg \mathrm{PHP}_3$$ is unsatisfiable. Now

$$\neg \mathrm{PHP}_3=(a\lor b)\land (c\lor d)\land (e\lor f)\land(\neg a\lor\neg c)\land(\neg a\lor\neg e)\land(\neg c\lor\neg e)\land(\neg b\lor\neg d)\land(\neg b\lor\neg f)\land(\neg d\lor\neg f)$$

Define $$r_j^m$$ be the propositional variable indicating that at least one of pigeons $$0,1,\cdots,m$$ occupies hole $$j$$, where $$0\le m\le n-1$$ and $$0\le j\le n-1$$. For example, $$r_0^2=a\lor c\lor e$$, and $$r_1^1=b\lor d$$. Let $$\alpha(m)=\left|\left\{r_j^m=1|j=0,1\right\}\right|$$ be the number of holes that are occupied pigeons $$0,1,\cdots,m$$. The basic idea of Buss' proof is to prove that $$\neg\mathrm{PHP}_n$$ implies $$0<\alpha(0)<\alpha(1)<\cdots<\alpha(n-1)$$, yielding $$\alpha(n-1)\ge n$$, which contradicts the fact that $$\alpha(m)\le n-1,\forall m$$. Numbers are encoded in a Boolean vector. For $$n=3$$, the numbers we concern are less than $$4$$, so a number $$w$$ can be represented by two Boolean variables $$u_1$$ and $$u_0$$, where $$w=2u_1+u_0$$.

Now we formulate the proof in propositional logic. Let $$\alpha(m)=2u_1^m+u_0^m$$, where $$u_1^m$$ and $$u_0^m$$ are propositional variables. It's clear that $$u_1^m=r_0^m\land r_1^m$$, $$u_0^m=r_0^m\oplus r_1^m$$, where $$\oplus$$ denotes exclusive-or.

• For $$m=0$$, $$r_0^0=a$$, $$r_1^0=b$$, so $$u_1^0=a\land b$$, $$u_0^0=a\oplus b$$, so $$\alpha(0)>0$$ is $$u_1^0\lor u_0^0=(a\land b)\lor(\neg a\land b)\lor(a\land\neg b)$$. Since $$\neg \mathrm{PHP}_3\to a\lor b\to (a\land 1)\lor(b\land 1)\to(a\land b)\lor(a\land\neg b)\lor(\neg a\land b)$$, this can be easily proved.
• For $$m=1$$, $$r_0^1=a\lor c$$, $$r_1^1=b\lor d$$, so $$u_1^1=(a\lor c)\land(b\lor d)$$, $$u_0^1=((a\lor c)\land\neg(b\lor d))\lor(\neg(a\lor c)\land(b\lor d))$$. $$\alpha(1)>\alpha(0)$$ can be formulated as $$(\neg u_1^0\land u_1^1)\lor\left((u_1^0\leftrightarrow u_1^1)\land(\neg u_0^0\land u_0^1)\right)$$, that is $$\left(\neg(a\land b)\land(a\lor c)\land(b\lor d)\right)\lor\left(\left(\left((a\land b)\land(a\lor c)\land(b\lor d)\right)\lor\left(\neg(a\land b)\land\neg((a\lor c)\land(b\lor d))\right)\right)\land\left(\neg((\neg a\land b)\lor(a\land\neg b))\land\left(((a\lor c)\land\neg(b\lor d))\lor(\neg(a\lor c)\land(b\lor d))\right)\right)\right)$$But I have difficulty deriving this formula. According to the paper, this formula should be derived by applying Lemma 6, but I can't figure out how is Lemma 6 applied.

Let $$\vec{v}$$ be a Boolean vector, and denote by $$T(\vec{v})$$ the number of true components of $$\vec{v}$$. In my perspective, Lemma 6 states that: for Boolean vectors $$\vec{r}$$ and $$\vec{r}'$$, if for every $$k$$, $$r_k'\to r'$$, and there exists $$h$$ such that $$r_h\land\neg r_h'$$, then $$T\left(\vec{r}\right). I can't see how to apply this lemma.

So my questions are:

1. Is my understanding of the lemma correct?
2. If the lemma is correctly stated, how can we use it to derive the formula I mentioned above?

Thanks!