3
$\begingroup$

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.


My Question about the Proof

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}$$

enter image description here

My thoughts about

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 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$\psi$ is indecidible and $\mathbf{PA}$ is inconsistent.

  • 0
    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.2012-08-29
  • 0
    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.2012-08-29
  • 0
    Does the exposition at http://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.2012-08-29
  • 0
    @CarlMummert I have done the promised edit, shouldn't I consider the case $(b)$ in order to infer $(*)$ in my question?2012-08-29
  • 0
    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.)2012-08-29
  • 0
    @ArthurFischer No, no, surely van Dalen's proof is correct. I am taking my first course in Mathematical Logic. So I am not able to understand an argument without making explicit all little steps, but I can be wrong even in the opposite direction taking as granted what instead is more subtle.2012-08-29
  • 0
    After having read the proof, I started to reconstruct it by myself, to test my comprehension. I needed to justify the statement "From (1) and (2) it follows that $\vdash\exists z<\overline{n}\overline{\mathrm{Prov}}(z,\overline{g(\neg\psi)})$" To justify it, I have thought what is written in the question. Isn't this justification necessary? Is my guess wrong? Thank you.2012-08-29

1 Answers 1