Timeline for Is all ordinary mathematics contained in high school mathematics?
Current License: CC BY-SA 2.5
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 2, 2023 at 15:36 | comment | added | Emil Jeřábek | The inverse Ackermann function is not $\log^*$, but regardless of that, it is avaliable in EFA (as a provably total $\Delta_0$-definable function). So there is no reason to think Tarjan’s upper bound is not formalizable in EFA. Unsolvability of the Halting problem is likewise provable in EFA. | |
| Nov 25, 2010 at 21:38 | comment | added | Greg Graviton | Except that $\log *$ is not the inverse Ackermann function. :-) As for the formalization, you might have a point if it were only the upper bound; there could be better bounds that can be formalized but which haven't been proven yet. However, if I am informed correctly, the bound is actually sharp, so you'd have an algorithm whose asymptotic complexity cannot be formalized in EFA. | |
| Nov 25, 2010 at 17:14 | comment | added | Kaveh | But it seems to me the inverse Ackermann function (i.e. $\log^*$) is available in EFA. Anyway, this kind of things depends heavily on how one formalizes the statement so it seems to me that non-existence of a function can only mean that a specific formalization of the theorem is not provable. | |
| Aug 28, 2010 at 16:32 | history | answered | Greg Graviton | CC BY-SA 2.5 |