# Can Robinson's Q prove Presburger arithmetic consistent?

I made an assertion in What are some examples of theories stronger than Presburger Arithmetic but weaker than Peano Arithmetic? that Q has higher consistency strength than Pres, Presburger arithmetic; i.e., Q proves the consistency sentence for Pres.

But in fact, I only know something weaker, that Q can formalise the provability predicate for Hilbert systems, and so prove, say, that Peano arithmetic proves Pres consistent.

Is there a direct proof of consistenct of Pres in Q?

-

I believe that Theorem 1 of Bezboruah and Shepherdson 1976 [1] covers your question, at least in spirit. Their theory $T_0$ is a finite theory extending $Q$. Quoting their paper:

Theorem 1. Let $L$ be any formal system with a recursive set of axioms, a finite number of finitary and recursive rules of inference including modus ponens and having $A \to A$ as a theorem for all sentences $A$. Let $$Con_L =_{df}\quad \lnot(\exists y,z)(Th_L(y) \land Th_L(z) \land neg(z,y))$$ where $\text{Th}_L$, $\text{neg}$ are given in Definition 3 below. Then $\text{Con}_L$ is not provable in $T_0$.

The authors, however, express the common doubt that consistency proofs in Q are philosophically meaningful.

"We must agree with Kreisel that this is devoid of any philosophical interest and that in such a weak system this formula cannot be said to express consistency but only an algebraic property which in a stronger system (e.g. Peano arithmetic P) could reasonably be said to express the consistency of Q."

The (well known?) difficulty here is that Q can formalize the provability predicate but cannot verify the Hilbert-Bernays derivability conditions for it.

1: A. Bezboruah and J. C. Shepherdson, "Gödel's Second Incompleteness Theorem for Q", The Journal of Symbolic Logic Vol. 41, No. 2 (Jun., 1976), pp. 503-512, JStor.

-
So Q is rock bottom. Well, along with the various weakenings of Q that there are. Which derivability condition(s) does Q fail? I know that Pudlak has expressed reservations about the Löb conditions. –  Charles Stewart Sep 14 '10 at 18:43
I'm having trouble locating a reference for it. I was under the impression that Q cannot show provability is closed under modus ponens, but perhaps this is only sloppiness in (multiple) papers I just checked that say say "Q is too weak" but perhaps all mean "Q is too weak for the standard proofs of the derivability conditions to go through". I'm interested in knowing the answer to this myself. –  Carl Mummert Sep 14 '10 at 20:28
These questions are, of course, sensitive to how you go about formalising the provability predicate. There's been a fair bit of work on formalising provability using tableaux search, which can give better properties, and I know that Dan Willard has looked at this for Q. I asked the question at MO: mathoverflow.net/questions/38874/… –  Charles Stewart Sep 15 '10 at 21:19