[FOM] Derivability conditions for Robinson arithmetic

[Ali Enayat]

On Sep 20 Carl Mummert asked whether any of the HBL
(Hilbert-Bernays-Loeb) conditions is known to fail for Q (Robinson's
arithmetic).

The following answer is kindly provided by Albert Visser, who has
given permission for his reply to be posted here.

********************************************************************************************************
I do not think there is a published proof that one of the HBL
conditions fails in
Q. However this question is underspecified since even small variations of
setting up the provability predicate are not provably equivalent in Q.
Are we to fix a
fully specified one? Do we want `fails for some reasonable proof
predicate' or `fails
for all reasonable proof predicates', etc. The latter quantifier is of
course hopeless ...
My guess would be that all conditions (except of course the
necessitation *rule*) fail for all reasonable formalizations.
One should realize that Q does not even verify the associativity of addition.
More interesting is the case of I\Delta_0. My student Andre van Kooij
verified (many years ago) that
there is a finitely axiomatized subtheory, say T, of I\Delta_0 that
verifies the HBL for T.
The problem here is *provable implies provably provable*. To do that
you need to work with a relational
language, with a non-standard treatment of syntax (checking
balancedness of bracket structures) and
you need a really different proof strategy than the usual one for
*provable implies provably provable*.
The usual proof of *provable implies provably provable* involves a
p-time transformation of proofs that
is not lin-time and, thus, cannot help us.
Best,
Albert