We show some tight results about the tree-resolution complexity of the
Weak Pigeon-Hole Principle,
. We prove that any optimal tree-resolution proof of
is of size
, independently from
, even if it is infinity. So far, the lower bound know has been
. We also show that any, not necessarily optimal, regular tree-resolution
proof
is bounded by
. To best of our knowledge, this is the first time, worst-case proofs have
been considered, and a non-trivial upper bound has been proven. Finally,
we discuss and conjecture some refinements of Riis' Complexity Gap theorem
for tree-resolution complexity of Second Order Existential (
) sentences of predicate logic.