The pigeonhole principle is the scheme
$\forall \bar{a},s \{\forall x\!<\!s\!+\!1 \exists y\!<\!s\psi(x,y,\bar{a}) \to \exists x_1,x_2\!<\!s\!+\!1\exists y\!<\!s[x_1\neq x_2 \wedge \psi(x_1,y,\bar{a}) \wedge \psi(x_2,y,\bar{a})]\}$
for all formulas $\psi$. The scheme can be proved in Peano arithmetic using Gödel encoding of finite sequences and induction axioms. However, the scheme is multiplication-free so can also be perfectly stated in Presburger arithmetic. However, though Presburger arithmetic can prove all instances of the scheme (since its a decidable theory), it seems impossible for Presburger arithmetic to prove this scheme. Is there any deeper understanding of this phenomena?