Timeline for What is the known weakest axiom system has Löb's derivability conditions?
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 2, 2016 at 15:16 | comment | added | Emil Jeřábek | 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. | |
| May 2, 2016 at 9:10 | comment | added | Emil Jeřábek | I don't understand your comment. $I\Delta_0+EXP$ is "digging into complexity" just as $\Delta^b_1$-CR is, only not deep enough to match the complexity of the problem (basic syntactic manipulations can be done in uniform $TC^0$, they don't need a tower of exponentials of running time). | |
| May 1, 2016 at 16:10 | comment | added | Ruizhi Yang | 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? | |
| May 1, 2016 at 15:03 | comment | added | Emil Jeřábek | $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. | |
| May 1, 2016 at 14:32 | comment | added | Payam Seraji | I think $I\Delta_0$+exp is the weakest natural subsystem of PA which proves all provability conditions. | |
| May 1, 2016 at 13:38 | comment | added | Monroe Eskew | Can you possibly "axiomatize" those conditions to create the weakest system? | |
| May 1, 2016 at 10:08 | history | asked | Ruizhi Yang | CC BY-SA 3.0 |