About a step in the proof of Gödel-Rosser Theorem.

I am reading about the Gödel-Rosser Theorem, i.e. the Rosser's refinement of first Gödel's incompleteness Theorem, which states that if $\mathbf{PA}$ is consistent then it is incomplete.
I am posting this question to understand a point in its proof as written in van Dalen "Logic and Structure" 4th Edition.

Just the Foreground (Please, feel free to skip it).

Rosser's trick amounts to consider the wff $\mathscr{R}(x)$ defined by $$\forall y[\overline{\mathrm{Neg}}(x,y)\to\forall z(\overline{\mathrm{Prov}}(z,y)\to\exists w< z\overline{\mathrm{Prov}}(w,x)],$$ where

• the formula $\overline{\mathrm{Neg}}(x,y)$ represents the numeric function $f$ defined by $f(m)=n$ iff there exists a wff $\phi$ such that $m$ and $n$ are the Gödel numers of $\phi$ and $\neg\phi$ respectively; and

• the formula $\overline{\mathrm{Prov}}(z,y)$ represents the numeric relation $R$ such that $(m,n)\in R$ iff there exists a wff $\phi,$ whose Gödel number is $n,$ while $m$ is the Gödel number of a deduction of $\phi.$

Applying the Fixed Point Theorem, we find a sentence $\psi$ such that $$\vdash\psi\leftrightarrow\neg\mathscr R(\overline{g(\psi)}),$$ where we are denoting the Godel numbering with $g,$ and the $n$-th ordinal as $\overline{n}.$

Gödel-Rosser Theorem: If $\mathbf{PA}$ is consistent then $\psi$ is indecidible, therefore $\mathbf{PA}$ is incomplete.

In the step "if $\vdash\psi$ then $\mathbf{PA}$ is inconsistent" (see snapshot below), after having written the assumption as $\vdash\overline{Prov}(\overline{n},\overline{g(\psi)}),$ for some natural number $n,$ I think that we should distinguish between the following two cases: $$\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)}),\tag{a}$$ $$\not\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)}).\tag{b}$$

In the case $(a),$ we would get immediately the inconsistency of $\mathbf{PA},$ precisely $\overline{Prov}(\overline{n},\overline{g(\psi)})$ is indecidible.

In the case $(b),$ $\not\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)})$ implies $$\not\vdash\exists z>\overline{n}(\overline{Prov}(z,\overline{g(\neg\psi)})\wedge\forall w<z\neg\overline{Prov}(w,\overline{g(\psi)})).\tag{*}$$ Observe that $\neg\mathscr R(\overline{g(\psi)})$ is equivalent to $\exists z(\overline{Prov}(z,\overline{g(\neg\psi)})\wedge\forall w<z\neg\overline{Prov}(w,\overline{g(\psi)})).$
Now by $(*)$, $\vdash\psi$ and $\vdash\psi\leftrightarrow\neg\mathscr R(\overline{g(\psi)}),$ we infer $$\vdash\exists z\leq\overline{n}(\overline{Prov}(z,\overline{g(\neg\psi)})\wedge\forall w<z\neg\overline{Prov}(w,\overline{g(\psi)})).$$ Consequently $\vdash\exists z\leq\overline{n}\overline{Prov}(z,\overline{g(\neg\psi)}),$ and so $\vdash\neg\psi.$ Therefore $\psi$ is indecidible and $\mathbf{PA}$ is inconsistent.

-
I'd like to answer but I don't feel I can with the info provided. Could you also include formula (1) (mentioned in the proof) in your question? It may also help if you could explain why you think the two cases are needed. – Carl Mummert Aug 29 '12 at 11:14
Dear Carl Mummert formula (1) is substantially $\vdash\psi\leftrightarrow\neg\mathscr{R}(\overline{g(\psi)}).$ Just a moment, and I will edit the question. – Giuseppe Tortorella Aug 29 '12 at 11:23
Does the exposition at en.wikipedia.org/wiki/Rosser%27s_trick make more sense? I am still not sure why you are thinking of a case where something is not provable. The two broad parts of the proof are to show that $\vdash \psi$ is impossible and that $\vdash \lnot \psi$ is impossible. Since $\not\vdash \psi$ is true (for a consistent theory), we can't get a contradiction by assuming $\psi$ is not provable. – Carl Mummert Aug 29 '12 at 11:37
@CarlMummert I have done the promised edit, shouldn't I consider the case $(b)$ in order to infer $(*)$ in my question? – Giuseppe Tortorella Aug 29 '12 at 13:04
Why do you think that we should break it up into these cases? Do you think there is a flaw in the van Dalen's proof? (Note that your argument in case (b) is extremely similar to the argument given in van Dalen.) – Arthur Fischer Aug 29 '12 at 18:44

I love van Dalen's book in general, but it has to be said that this proof isn't his clearest effort at all. For a start the move from $\vdash (\exists y < \overline{n})\varphi(y)$ to $\vdash\varphi(\overline{0})$ or $\vdash\varphi(\overline{1})$ or ... or $\vdash\varphi(\overline{n - 1})$ doesn't depend on $\varphi$ being $\Delta_0$. It obtains for any $\varphi$ so long as we are working in a theory which is as strong as Robinson Arithmetic $Q$.
Think of it like this, to stand back from the implementation details. We can construct a Rosser-provability predicate, $\mathsf{RProv}$, and then take a fixed point $\psi$ for its negation, so $\vdash \psi \equiv \neg\mathsf{RProv}([\varphi])$ We want to prove (i) $\nvdash \psi$ and (ii) $\nvdash\neg\psi$, assuming we are working in a consistent theory. We are now considering just (i).
So, for reductio, suppose $\vdash\psi$, i.e. suppose $\psi$ is provable, so (A) some number $n$ numbers a proof of $\psi$. By our consistency assumption, (B) no number $m < n$ numbers a proof of $\neg\psi$. Because we are working in a sufficiently strong theory, given (A) and (B) we'll be able to show $\vdash \mathsf{RProv}([\varphi])$, whence $\vdash\neg\psi$, making the theory we are working in inconsistent contrary to hypothesis.
Do we need, to make this argument fly, to explicitly make the assumption that (a) or (b) and then argue by cases? No. For it is a given that we are dealing with a consistent theory. Now once we get to (A), since we are dealing with a sufficiently strong theory, that gives us van Dalen's (2), and the consistency assumption immediately rules out (a). And though (b) is therefore immediate, it doesn't actually get mentioned in the rest of the proof which is concerned with arguing from (B) (which involves $m < n$).