# What is the known weakest axiom system has Löb's derivability conditions?

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?

• Can you possibly "axiomatize" those conditions to create the weakest system? – Monroe Eskew May 1 '16 at 13:38
• I think $I\Delta_0$+exp is the weakest natural subsystem of PA which proves all provability conditions. – Payam Seraji May 1 '16 at 14:32
• $I\Delta_0+EXP$ is an overkill. Lob's provability conditions are provable in PV, or even in TC^0 theories like Johanssen&Pollett's $\Delta^b_1$-CR. – Emil Jeřábek May 1 '16 at 15:03
• Thanks! But if we don't dig into complexity, is $I\Delta_0 + EXP$ the best answer we can expect? Is there any reference on this question? – Ruizhi Yang May 1 '16 at 16:10
• As for references: the only problematic condition is $T\vdash\mathrm{Pr}_T(\ulcorner\phi\urcorner)\to\mathrm{Pr}_T(\ulcorner\mathrm{Pr}_T(\ulcorner\phi\urcorner)\urcorner)$. The Claim on p. 303 of Krajíček’s Bounded Arithmetic, Propositional Logic, and Complexity Theory shows 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’s Logical Foundations of Proof Complexity. – Emil Jeřábek May 2 '16 at 15:16