Reflection using the derivability conditions

We extend arithmetic with a new predicate $Pr$, giving axioms for it based on first order versions of L\"ob's derivability conditions. We hoped that the addition of a reflection schema mentioning $Pr$ would then give a non-conservative extension of the original arithmetic theory. The paper investigates this possiblity. It is shown that, under special conditions, the extension is indeed non-conservative. However in general such extensions turn out to be conservative