[FOM] D11 arithmetic

[Studtmann, Paul]

Solomon Feferman has shown that Delta11 arithmetic with an induction axiom,
not an induction schema, call it D11, is proof theoretically reducible to
Peano Arithmetic, PA.  Hence,

PA |- cons(PA) -> cons(D11).

I am curious whether anyone knows whether there are any results that might
bear on the following question.  Suppose that one were to add a single axiom
asserting the existence of a set of a certain sort to D11.  More
specifically, suppose one defines the notion of being recursive in
accordance with some condition, F, up to some number n and then added an
axiom of the following sort to D11:

(EX1)(y)(y is in X1 <-> (EX2)(En)(X2 is recursive up to n in accordance with
F & y is in X2))

Call the resulting theory D11+.  Now, the question.  Is it the case that:

PA |- cons(D11) -> cons(D11+)

Paul Studtmann