Rosser's corollary proof

Question

I encountered the Rosser's Corollary during my studies and also a proof of it that was highly unsatisfactory for me. So I would like to know how to finish it starting from what I have.

Lemma : Prove $N \vdash (\forall x: x < a \Rightarrow \phi(x)) \Rightarrow (\phi(0) \land \phi(1) \land ... \land \phi(a-1))$

Here is my attempt trying to format the best I can :

1. $\forall x: x < a \Rightarrow \phi(x)$ (assumption 1)
2. $b < a \Rightarrow \phi(b)$ ( $\forall$Elimination )
3. $b < a$ (assumption 2)
4. $\phi(b)$ (Modus ponens 2&3)
5. $(\forall x: x < a \Rightarrow \phi(x))\Rightarrow \phi(b)$ ($\Rightarrow$ introduction)

At this point is seem clear to me that since b is assumed to be inferior than a, we can iterate over each b, and produce the theorem (5) with each b taking values from 0 to a-1. The problem I have is that I can't get rid of the assumption 2.

I had the idea of considering the axiom : $\forall x:\forall y: (x< y) \lor (x == y) \lor (y < x) $ and treating each case separately finishing by ($\lor$ elimination ) but I couldn't do it.

How to do this formally ?

Note : I'm using the non logical axioms of Arithmetic represented by N here.

Difficulties with the following proof : Fix an arbitrary a, then we have :

$N \vdash (\forall x: x < a \Rightarrow \phi(x)) \Rightarrow (b < a \Rightarrow \phi(b)) $ for any b < a.

Then using (PC) we get :

$N \vdash (\forall x: x < a \Rightarrow \phi(x)) \Rightarrow (\phi(0) \land \phi(1) \land ... \land \phi(a-1))$

(PC) is defined as : if $\Lambda$ is a finite set of formulas, $\phi$ a formula, and $\phi$ a propositional consequence of $\Lambda$, then ($\Lambda$, $\phi$) is an inference rule of the type (PC).

Answer 1

Hint: the proof you are looking at is really a proof schema indexed by the natural number $a$: i.e., a family of proofs one for each $a$. In the description of this family of proofs $b$ ranges over natural numbers less than $a$. E.g., consider the specific example $a = 3$, then for $b = 0, 1, 2$, using the provable formulas $0<3$, $1 < 3$ and $2 < 3$, we have

$$ N \vdash (\forall x: x < 3 \Rightarrow \phi(x)) \Rightarrow (\phi(0))\\ N \vdash (\forall x: x < 3 \Rightarrow \phi(x)) \Rightarrow (\phi(1))\\ N \vdash (\forall x: x < 3 \Rightarrow \phi(x)) \Rightarrow (\phi(2))\\ $$

Using the principle (PC), this gives the desired result for $a = 3$:

$$ N \vdash (\forall x: x < 3 \Rightarrow \phi(x)) \Rightarrow (\phi(0) \land \phi(1) \land \phi(2)) $$