Timeline for What can $I\Delta_0$ prove?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 10, 2021 at 2:10 | history | bounty ended | BPP | ||
| Feb 9, 2021 at 19:02 | vote | accept | BPP | ||
| Feb 9, 2021 at 13:22 | history | edited | user44143 | CC BY-SA 4.0 |
deleted 23 characters in body
|
| Feb 9, 2021 at 12:51 | comment | added | user44143 | @EmilJeřábek, let me know if this is good now | |
| Feb 9, 2021 at 12:50 | history | edited | user44143 | CC BY-SA 4.0 |
corrected in response to comments
|
| Feb 9, 2021 at 8:26 | comment | added | Emil Jeřábek | To clarify the above, Fermat’s two-square theorem is equivalent over $I\Delta_0$ to the statement $\bigl(\frac{-1}p\bigr)=1$ for prime $p\equiv1\pmod4$. This is not known to be provable even in $I\Delta_0+\Omega_1$. See doi.org/10.1016/0168-0072(91)90096-5 and doi.org/10.1002/malq.200910009. The weakest extension of $I\Delta_0$ known to prove it is the theory $I\Delta_0+\mathrm{Count}_2(\Delta_0)$ with modulo-$2$ counting principles (actually, its subtheory $IE_1+\mathrm{Count_2}(\nabla_1)$ suffices), which actually proves the full quadratic reciprocity theorem. | |
| Feb 9, 2021 at 7:47 | comment | added | Emil Jeřábek | As far as I am aware, $I\Delta_0$ is not known to prove Fermat’s two-square theorem. Its proofs require a counting argument to establish that $-1$ is a quadratic residue. (The theory can formalize the infinite descent argument that if $-1$ is a quadratic residue, then $m$ can be written as a sum of two squares.) | |
| Feb 9, 2021 at 3:43 | comment | added | Erfan Khaniki | $x^{\log x}$ is not provably total in $I\Delta_0$, by Parikh theorem. See: math.ucsd.edu/~sbuss/ResearchWeb/parikh/paper.pdf | |
| Feb 9, 2021 at 2:33 | history | answered | user44143 | CC BY-SA 4.0 |