We know that Peano Arithmetic satisfies Löb's derivability conditions, which is required in the proof of Gödel's 2nd incompleteness theorem. Is this the best result? If not, is there any known weaker system have the derivability conditions, and is there a weakest?

Bounded Arithmetic, Propositional Logic, and Complexity Theoryshows this for the theory $S^1_2$, and therefore for $PV_1$ by $\forall\Sigma^b_1$-conservativity. I couldn’t find an explicit reference for a TC^0 theory; it doesn’t seem to be stated in Cook and Nguyen’sLogical Foundations of Proof Complexity. $\endgroup$ – Emil Jeřábek May 2 '16 at 15:16