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.


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. : )

  • $\begingroup$ You can see the full proof into Elliott Mendelson, Introduction to mathematical logic (4th ed - 1997), page 209-210; regarding point 2, the proof exploits some properties of the $\le$ relation. $\endgroup$ Mar 3 '15 at 9:29
  • $\begingroup$ Yeh, I had a look into his proof. He does, as far as I can see, define rosser's proof predicate purely syntactical. I'll have another look and see, if I can extrude the idea. Still I'm interested in the first question I stated. : ). Thanks for your comment. $\endgroup$
    – aphorisme
    Mar 3 '15 at 9:44
  • $\begingroup$ I do not full grasp your concern ... Rosser's formula is a syntactical object; you are working in PA, i.e. first-order arithmetic, and thus you can simply add to the language the defined predicates $<$ and $\le$. Thus, in first-order language for arithmetic, $x \le y$ is a "well-formed" expression. $\endgroup$ Mar 3 '15 at 9:53
  • $\begingroup$ Well, my problem is the following (I might be missing something): Smorynski defines $\Bew{PA}^R$ as a primitive recursive relation. Of course, we then have $\Bew{PA}^R(x,y)\Leftrightarrow \text{PA}\vdash\color{red}{\Bew{PA}^R(\overline{x},\overline{y})}$ and so on, but I need some features of how $\Bew{PA}^R$ is defined, especially the $\forall wz\leq x$, to prove what I need to. But the $\color{red}{\Bew{PA}^R}$ is just a predicate symbol. I don't know nothing about it. $\endgroup$
    – aphorisme
    Mar 3 '15 at 10:02
  • $\begingroup$ I see... In Mendelson' textbook, Godel and Rosser theorems are proved after a chapter deicated to "formal number theory" where, e.g. it is proved that $x < y$ is a primitive recursive relation and that relations obtained from p.r. relations by means of the conncetives and the bounded quantifires (like $\forall z \le x$) are p.r [see page 180]. $\endgroup$ Mar 3 '15 at 10:08

Long comment

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

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".


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.