[FOM] Derivability conditions for Robinson arithmetic

[David Auerbach]

I think the poster has in mind something like Bezboruah and Shepherdson's classic paper in which they (while proving a version of G2 for Q) disparage the means they needed to do it ("Even for the simple way of expressing consistency we choose, the construction of the model requires a fair amount of algebraic effort. We regard this really as an example of how not to do it..."). They also point out (channeling Kreisel) that the underivable sentence in question is a dubious candidate for "really expressing" consistency (*in Q*).  It is certainly true that the derivability conditions don't hold for Q. 
  The relevant earlier paper, establishing that the third derivability condition, the theoremhood of Th A  -->Th Th A, is the relevant culprit, is Jeroslow's  "Consistency statements in formal theories" in Fundamenta Mathematicae, vol. 72 (1971), pp. 17-40 or his "Redundancies in the Hilbert-Bernays derivability conditions for Gödel's Second Incompleteness Theorem" in JSL 1973.   
 The underlying intuition is that to establish the generality that if something is provable then it's provable that it's provable requires being able to "follow" the inductive characterization of *proof*.  And Q doesn't have induction.  That's why PA  is a natural bottom for the usual proofs of G2 with its usual rendering as being about the unprovability of a consistency sentence. 



David Auerbach                                                      auerbach at unity.ncsu.edu
Department of Philosophy and Religious Studies
NCSU
Raleigh, NC 27695-8103

On Sep 20, 2010, at 9:42 AM, Carl Mummert wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom