# On the polynomial-size Frege proof of the propositional pigeonhole principle

I'm reading a lecture note on the proof of PHP, which mentioned that a "basic fact" $$\left(\sum\limits_{i=1}^{s-1} A_i\ge a\right) \land A_s \to \sum\limits_{i=1}^s A_i\ge a$$ is necessary in the proof, where $$A_i$$'s are propositional formulas (which are added together as if they're integers). Here addition is expressed with carry-save addition, which is a technique that gives log-depth polynomial-size Boolean formulas for counting. It's a divide-and-conquer approach that divide the input variables into two parts, compute two numbers that represents the sum for each part, and then combine them together. The lecture note left the proof of the fact as an exercise, but I can't figure out how exactly to prove it. The formulas representing the sum vary between $$\sum\limits_{i=1}^{s-1} A_i$$ and $$\sum\limits_{i=1}^{s} A_i$$, in the sense that the ways to divide the variables can be totally different. I considered the two cases where $$A_s=0$$ and $$A_s=1$$, but the binary tree for $$\sum\limits_{i=1}^{s-1} A_i$$ produced in the carry-save addition technique can be different even if $$A_s$$ is assigned a value in $$\sum\limits_{i=1}^{s} A_i$$. This may require us to prove the commutativity of addition first, which is a lot more complicated. Is there an elegant way to solve this?

• Don't do it this way. Fix $t$ such that all sums needed in the proof have at most $t$ terms, fix carry-save addition formulas for $\sum_{i=1}^tx_i$, and interpret all sums $\sum_{i=1}^sA_i$ as $\sum_{i=1}^tA'_i$ where $A'_i=A_i$ for $i\le s$, and $A'_i=0$ otherwise. Then the variables are always divided in the same way. Feb 15 at 14:50