Timeline for Provability in $S^1_2$
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 4, 2017 at 16:38 | answer | added | Itai Bar-Natan | timeline score: 1 | |
| Sep 4, 2017 at 16:33 | comment | added | Dmytro Taranovsky | @EmilJeřábek Arbitrary $Π^0_1$ statements can be rephrased in EFA as $∀Δ^b_1$ (though sometimes only by replacing $∀x$ with $∀y \, ∀x<\log(y)$, which gives $S^1_2$ a strong extra assumption). Correctness/optimality of algorithms is usually already $∀Δ^b_1$. I am also interested in examples that can be converted to $∀Δ^b_1$ if $S^1_2$ were to prove P=PSPACE (but only if their unprovability in $S^1_2$ has been shown unconditionally). Consistency statements are a good example, but it would be surprising if they were essentially the only example. | |
| Sep 4, 2017 at 13:27 | comment | added | Emil Jeřábek | ... for instance, the consistency of the first-order theory in the language of pure equality axiomatized by $\exists x\,\exists y\,(x\ne y)$, formulated as a usual Hilbert-style or sequent calculus. | |
| Sep 4, 2017 at 13:26 | comment | added | Emil Jeřábek | There aren’t that many natural statements of this form ($\forall\Delta^b_1$ ) in the first place, all I can think of are various consistency statements. Over a weaker base theory, the strongest $\forall\Delta^b_1$ sentence provable in $S^1_2$ is the consistency of the Extended Frege propositional proof system, which is not a very powerful statement. Then, simple examples of $\forall\Delta^b_1$ statements not provable in $S^1_2$ are consistency statements for calculi that we assume not to be p-simulated by EF: ... | |
| Sep 3, 2017 at 21:17 | history | asked | Dmytro Taranovsky | CC BY-SA 3.0 |