Show that PA can prove the pigeon-hole principle

Question

So the following exercise is from Richard Kaye's Book exercise 5.12 (Chapter 5)

The pigeon-hole principle is the scheme:

For any formula, $\psi$, in the language of arithmetics,

$\forall s\ ((\forall x<s+1, \exists e<s\ \psi(x,e)) \rightarrow\ \exists x, r < s+1, \exists e<s (x \neq r\ \wedge\psi(x,e) \wedge\psi(r,e)))$

Show that PA can prove (every instances) of the statement.

This statement is so intuitively true, but I'm having some trouble proving it and I dont quite understand the hints given in the book.

Any help or insights is deeply appreciated.

Answer 1

This is trickier than it looks at first. If you try to prove it directly by induction on $s$ you run into the problem that you'll need the induction hypothesis for a different $\psi$ -- which is not allowed because that's a different induction.

I think you need to go "the long way around" and start by replacing the $\psi$ with something you can quantify over, such as Gödel's $\beta$ function: $$ \forall s,b,c: \bigl( \forall x<s+1: (\beta(b,c,x)<s ) \to \exists x,r<s+1: (x\ne r \land \beta(b,c,x) = \beta(b,c,r)) \bigr) $$ Since $\beta$ is a single function whose formula is the same no matter the values of $b$ and $c$, you can prove this by induction on $s$.

Along the way you need a number of lemmas about manipulating $\beta$-encoded sequences. If you already have those lemmas in your toolbox the going is not too bad; otherwise there's a lot of work to do, which will include proving some form of the Chinese Remainder Theorem along the way.

Finally, prove as a metatheorem that for every $\psi$ you can derive $$ \forall s: (\forall x<s+1\,\exists e<s : \psi(x,e)) \to \exists b,c\, \forall x<s+1 : \bigl( (\beta(b,c,x)<s \land \psi(x,\beta(b,c,x)) \bigr) $$ which you can then combine with the above to get the formula you're after.

Answer 2

Since the proof suggested by Kaye is sketched in another answer, I'll mention a more high powered way to prove this. Because the second-order system $\mathsf{ACA}_0$ is conservative over PA for sentences in the language of PA, we can just prove the statement in $\mathsf{ACA}_0$. This is easier because we can work directly with functions from $\mathbb{N}$ to $\mathbb{N}$, and can form any function that is arithmetically definable.

First, we can prove in $\mathsf{ACA}_0$ that if $f$ is any injection from $\mathbb{N}$ to $\mathbb{N}$ then, for all $s$, $f([s+1]) \not \subseteq [s]$. This uses the ordinary proof of the pigeonhole principle.

Then we show that if any of the statements Kaye is considering were to fail, we could use this to construct a injection that contradicts the previous claim. In particular, if the statement fails at $s$, we would let $f(i) = (\mu j \leq s) \psi(i,j)$ for $i \leq s+1$ and $f(i) = i$ for $i > s+1$, which is arithmetically definable.