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?
$\begingroup$
$\endgroup$
6
-
1$\begingroup$ Can you possibly "axiomatize" those conditions to create the weakest system? $\endgroup$– Monroe EskewCommented May 1, 2016 at 13:38
-
1$\begingroup$ I think $I\Delta_0$+exp is the weakest natural subsystem of PA which proves all provability conditions. $\endgroup$– Payam SerajiCommented May 1, 2016 at 14:32
-
2$\begingroup$ $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. $\endgroup$– Emil JeřábekCommented May 1, 2016 at 15:03
-
$\begingroup$ 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? $\endgroup$– Ruizhi YangCommented May 1, 2016 at 16:10
-
1$\begingroup$ 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. $\endgroup$– Emil JeřábekCommented May 2, 2016 at 15:16
|
Show 1 more comment