[FOM] Derivability conditions for Robinson arithmetic

[Carl Mummert]

Dear FOM,

It's well known that the standard proofs of Goedel's second
incompleteness theorem require that the theory is able to verify the
Hilbert-Bernays derivability conditions for the provability predicate,
or some similar set of derivability conditions. Proofs that Robinson's
arithmetic Q and other weak arithmetics do not prove their own
consistency use different, more ad hoc, methods. Looking through the
literature, I can find various remarks about the derivability
conditions and Q, but nothing specific.

Is there a published proof that one that one of the Hilbert-Bernays
conditions is not provable in Q?

This question was originally posed by Charles Stewart on MathOverflow [1].

Sincerely,

Carl Mummert
Marshall University

1: http://mathoverflow.net/questions/38874/derivability-conditions-for-robinson-arithmetic