Understanding Rosser's Theorem

Question

Initial Situation

For some time now I'm trying to understand a proof for Rosser's Theorem -- the proof given in Smorynski's article "The Incompleteness Theorems" (here is a first entry from google: The Incompleteness Theorems - Smorynski), well actually it's not a proof but a list of hints -- and I'm struggling.

The Definitions

Rosser's Proof Predicate is defined as an extension to the "usual" proof predicate in the following way:

$\newcommand{\Bew}[1]{\mathbf{Bew}_{\text{#1}}} \newcommand{\encode}[1]{\left\ulcorner #1 \right\urcorner}$ $$\Bew{PA}^R (x,y) \leftrightarrow \left(\Bew{PA}(x,y)\wedge \forall zw\leq x\left(\Bew{PA}(z,w)\rightarrow y\neq [\encode{\neg},w]\wedge w \neq [\encode{\neg},y]\right)\right).$$

(This is from page 841 -- I've just changed $\mathbf T$ to $\text{PA}$.)

And Rosser's Theorem is then stated as follows:

Let $\text{PA}\vdash \varphi \leftrightarrow \neg \exists x . \Bew{PA}^R(x,\encode{\varphi})$ and assume that $\text{PA}$ is consistent. Then

1. $\text{PA}\nvdash \varphi$;
2. $\text{PA}\nvdash \neg\varphi$;
3. $\text{PA}\vdash\text{Con}_{\text{PA}}^R$.

Own ideas

First of all: it seems to me that Rosser's proof predicate is defined at first as a primitive recursive relation. If so, I agree with Smorynski here: it is extensional the same as $\Bew{PA}$ (seen as a primitive recursive relation), as long as we assume that $\text{PA}$ is consistent. Then, of course, 1. follows in the same way, as one can show it in the usual incompleteness theorem style ($\text{PA}\vdash\phi\Rightarrow \text{PA}\vdash\Bew{PA}^R(e,\encode{\phi})$ is the key, which holds then, for some closed term $e$.)

But then, I got some trouble showing 2. Since in my version, I need $\leq$ as a predicate in the language and not as a primitive recursive relation, or: I have to establish a connection from $\leq$ as primitive recursive relation to $\leq$ as a syntactical object. (I can give more details on that, but I think this is the wrong way anyways.)

Now, 3. seems clear to me, although my proof is a bit too meta for my taste.

Questions

So, the big question is: how to proof 2. if one accept that $\Bew{PA}^R$ is defined as a primitive recursive relation at forehand? Especially with the following hint Smorynski gives: 2. follows from 3. Aha!

Or: How to proof 1, if one defines $\Bew{PA}^R$ as an extension to $\Bew{PA}$ in the syntactical world?

Or, second question one step further: how does one proof $\text{PA}\vdash\phi\Rightarrow \text{PA}\vdash\Bew{PA}^R(e,\encode{\phi})$, when $\Bew{PA}^R$ is seen syntactically?

Any ideas or hints, also solutions, are appreciated. : )

Answer 1

Long comment

If the issue is with $∀z≤x \ Pz$, we have to recall some definitions from :

• Dirk van Dalen, Logic and Structure (5th ed - 2013), page 213 :

Definition A relation $R$ is primitive recursive if its characteristic function $\chi_R$ is so.

The equality relation is p.r. : $\chi_=(x, y) = \overline {sg}(|x − y|)$

The order relation is p.r. : $\chi_<(x, y) = \overline {sg}((x + 1) - y)$

We say that $R$ is obtained by bounded quantification from $S$ if

$R(n,m) = Qx \le m \ S(n,x)$, where $Q$ is one of the quantifiers $∀,∃$.

Consider the bounded existential quantification: $R(x,n) = ∃y \le n \ S(x, y)$; then $\chi_R(x,n) = sg(y \le n \ \chi_S(x, y))$, so if $S$ is primitive recursive, then $R$ is so.

The $∀$ case is similar.

---

You can see also Smorynski's article itself, page 833 : for the relation of equality and bounded quantifiers.

In page 836 you can see how bounded quantifiers are used to define the representing functions for the syntactic notions of term and formula.

Finally [page 838], the bounded quantifier is used also in the definition of the $Prov_T(x,y)$ predicate.

Thus, in principle, nothing different happens with Rosser's predicate [page 841] : $Prov^R_T(x,y)$, which is simply "a little bit more complex".