Pigeonhole principle formula using Propositonal Logic

According to the Pigeonhole Principle, if we try to place $n+1$ pigeons in $n$ pigeonholes, then at least one pigeonhole must have two or more pigeons. For $i \in \{1, 2, \dots, n+1\}$ and $j \in \{1, 2, . . . , n\}$, let the atomic proposition $p_{i j}$ denote that the $i$-th pigeon is placed in the the $j$-th pigeonhole.

Write down a formula expressing the Pigeonhole Principle. What is the length of formula as a function of $n$?

• if you consider $p[i][j]=1$ iff the $i$ th pigeon is placed in the the $j$ th pigeonhole, then the Pigeonhole Principle is equivalent to saying that $$\forall i \exists j p[i][j]=1\implies \exists j, i_1,i_2 p[i_1][j]=p[i_2][j]=1$$. But I would not write things this way if I want to proof the Pigeonhole Principle. I don't understand the aim of your question also? Commented Nov 13, 2015 at 15:18
• @Elaqqad The aim of the question is probably to serve as a first step in a discussion of proof complexity. The propositional formula $\phi_n$ expressing the pigeonhole principle for $n$ holes is a commonly used test case for the efficiency of deductive systems. The length of $\phi_n$ is bounded by a polynomial function of $n$, but there are questions about whether it has a proof, in certain formal systems, whose length is bounded by a polynomial of $n$. For example, if I remember correctly, resolution proofs of $\phi_n$ require exponential length, but the problem is open for stronger systems. Commented Nov 13, 2015 at 15:32

Although you didn't say so in the question, your title indicates that you want a formula in propositional logic. So I'd express "each pigeon is in a hole" as $$\bigwedge_{i=1}^{n+1}\bigvee_{j=1}^n p[i,j],$$ and I'd express "some hole contains two distinct pigeons" as $$\bigvee_{j=1}^n\bigvee_{1\leq i<k\leq n+1}(p[i,j]\land p[k,j]).$$ Finally, I'd express the pigeonhole principle as the implication from the first of these formulas to the second. HOWEVER, some people understand the pigeonhole principle as including the additional hypothesis that each pigeon is in only one hole, which is formulated as $$\bigwedge_{i=1}^{n+1}\bigwedge_{1\leq j<k\leq n}\neg(p[i,j]\land p[i,k]).$$ As for the length of the formula, that depends not only on whether you include the extra hypothesis but also on the details of the definition of length --- do you count occurrences of atomic formulas, or occurrences of connectives, or both, or something else?