Prove that the minimal finitely axiomatizable theory of arithmetic $\mathbf{Q}$ plus the Rosser sentence is consistent.

Question

Let $T$ be $\mathbf{Q}$ (which is a minimal finitely axiomatized theory of arithmetic). Let $R$ be the Rosser sentence of $T$. Let $T_0$ be $T + \{R \}$ and $T_1$ be $T + \{\sim R\}$. Show that $T_0$ and $T_1$ are both consistent. Show that $T_0 \cup T_1$ is inconsistent.

For reference, the Rosser sentence of $T$ is:

\begin{align*} \vdash_T R &\leftrightarrow \forall y ( \text{Prf}_T ( \ulcorner R \urcorner, \mathbf{y}) \to \exists z < y (\text{Disprf}_T(\ulcorner R \urcorner, \mathbf{z}))) \\ \end{align*}

The last part is quite easy. $T_0 \cup T_1$ has both $R$ and $\sim R$ so it's inconsistent.

However, we can prove that the Rosser sentence is undecidable in $\mathbf{Q}$ or any consistent, finitely axiomatizable extension of $\mathbf{Q}$.

To quickly review the proof that the Rosser sentence is not provable in any consistent, finitely axiomatizable extension of $\mathbf{Q}$: Suppose the Rosser sentence is provable, then there is some natural number that serves as a witness for its provability and by the Rosser sentence such that there is an earlier witness for its disprovability which yields a contradiction. Hence, the Rosser sentence is not provable.

$T_0$ is $T + \{R\}$. That is a finitely axiomatizable extension of $\mathbf{Q}$. Therefore, based on the proof we just reviewed, it must be inconsistent, and it seems to produce a refutation of the assigned problem, rather than a solution.

Answer 1

I answered this in the comments, but will recap in an answer:

• There is not one Rosser sentence $R,$ but rather a different Rosser sentence $R_T$ for each theory. These all take the form you write down, but the definition of the $\mathrm{Prf}_T$ and $\mathrm{Disprf}_T$ formulas depend on the theory $T.$ If $T$ is a consistent, recursive extension of $\mathbf Q,$ the Rosser sentence $R_T$ is not decidable from $T$, but this doesn't mean it can't be decidable from some consistent, recursive extension $T_0$ of $T.$
• As for how to do the problem, if $T+\{R\}$ were inconsistent, we would have $T+\{R\}\vdash A\land\lnot A$ for some $A,$ and then by the deduction theorem, $T\vdash R\to (A\land \lnot A).$ But, by truth tables, $R\to (A\land \lnot A)$ is logically equivalent to $\lnot R,$ so $T\vdash R,$ which is impossible since $R$ is $T$'s Rosser sentence. The same argument works to show that $T+\{\lnot R\}$ is consistent.

All the work in the second bullet is in proving a theorem so frequently used that it is worth caching in memory:

If $T$ is any theory and $A$ is any sentence in its language, then $T+\{A\}$ is inconsistent if and only if $T\vdash \lnot A.$

So once that fact is in hand, the argument is just: "Since $T\nvdash R,$ $T+\{\lnot R\}$ is consistent, and since $T\nvdash \lnot R, $ $T+\{R\}$ is consistent."