A variation of propositional pigeonhole principle

Question

Let $n$ be the number of pigeons, and $x_{i,j}$ denote the Boolean variable indicating that pigeon #$i$ is mapped to hole #$j$. Then the propositional pigeonhole principle (PHP) is the conjunction of following clauses:

1. $x_{i1}\lor x_{i2}\lor\cdots\lor x_{i,n-1}$, $\forall 1\le i\le n$ (a pigeon must be mapped to at least one hole)
2. $\neg x_{ik}\lor\neg x_{jk}$, $\forall 1\le i<j\le n,1\le k\le n-1$ (two pigeons $i,j$ cannot be mapped to the same hole $k$)

We know that the PHP formula is unsatisfiable. The reason why we can use "a pigeon must be mapped to at least one hole" instead of "a pigeon must be mapped to exactly one hole" is that, if a pigeon occupies multiple holes, then the remaining pigeons are even "less" likely to be accommodated. Now we consider replacing each $\neg x_{i1}\lor\neg x_{j1}$ with $\neg x_{i1}\lor\bigvee\limits_{t=2}^{n-1}x_{it}\lor\neg x_{j1}\lor\bigvee\limits_{u=2}^{n-1}x_{ju}$ (Note that the loosened constraints only apply to hole #1; otherwise the formulas would be satisfiable). After this, the formula is still unsatisfiable, since albeit the conditions are loosen, those $x_{it}$'s and $x_{ju}$'s can't be really set to true, because otherwise there will be no enough holes for the remaining pigeons. More intuitively, the replacement allows us to map pigeons #$i,j$ to the same hole #$k$ at the expense of mapping at least one of #$i,j$ simultaneously to another hole. Since a pigeon occupies at least two holes, the number of holes is still not enough so the contradiction still persists.

We know that the original PHP has a polynomial-size Frege proof saying that "from condition #1 we can infer that at least $n$ variables are satisfied, but from #2 we infer that at most $n-1$ variables are satisfied, which leads to contradiction". My question is, in this case, can we still construct a polynomial-size Frege proof for the modified formula?

update: I found that the constraints can be furthur loosened while preserving unsatisfiability. In this case we replace each $\neg x_{ik}\lor\neg x_{jk}$ with $\neg x_{ik}\lor\bigvee\limits_{t=k+1}^{n-1}x_{it}\lor\neg x_{jk}\lor\bigvee\limits_{u=k+1}^{n-1}x_{ju}$ (this time constraints for all holes for loosened, unlike in the first case where only constraints for hole #1 is loosened). This makes the formulas even harder to prove, since now the problem will not degenerate to vanilla PHP when we set some variables to true. The intuitive reason for the unsatisfiability is similar: if we let two pigeons occupy the same hole, at least one of them must also occupy another hole whose index is greater than the current one, so that the the number of holes is still not sufficient (this ordering constraint rules out the counterexample given by Joshua). Also, I used Python and PySAT to verify the unsatisfiability of these formulas and it turned out that they're still unsatisfiable up to $n=10$.

Answer 1

Even the “further loosened” version has short Frege (in fact, $\mathrm{TC}^0$-Frege) refutations.

Why is the principle unsatisfiable in the first place? Because if you map each pigeon to the hole with maximal index to which it is assigned by the original assignment, the “loosened clause” guarantees that the mapping is injective, hence it violates standard PHP.

This argument is straightforward to formalize in Frege. Let $$\let\LOR\bigvee\xi_{ij}=x_{ij}\land\neg\LOR_{k>j}x_{ik}.$$ There are polynomial-size constant-depth Frege proofs of $$\tag{$*$}\LOR_jx_{ij}\to\LOR_j\xi_{ij}.$$ Indeed, putting $\delta_{ij}=\bigvee_{k\ge j}x_{ik}$, a simple manipulation of the definition of $\xi_{ij}$ yields $$\delta_{ij}\to\delta_{i,j+1}\lor\xi_{ij}.$$ Chaining these proofs together gives $$\delta_{i1}\to\delta_{in}\lor\LOR_j\xi_{ij},$$ which yields $(*)$ as $\delta_{in}$ is a falsity (empty disjunction).

Now, using $(*)$, clause 1 of your pigeonhole principle yields $$\LOR_j\xi_{ij}$$ for each $i$, and the “loosened” clause 2 gives $$\neg\xi_{ik}\lor\neg\xi_{jk}$$ for each $i\ne j$ and $k$. Thus, we can derive a contradiction using a substitution instance of the usual pigeonhole principle.