Can Robinson's Q prove Presburger arithmetic consistent?

Question

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?

Answer 1

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.