Timeline for What subsystem of third order arithmetic proves the real numbers are Dedekind complete?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 13, 2020 at 15:34 | comment | added | Sam Sanders | @Pakhomov: one has to be very careful with the combination of $\exists^2$ and principles that allow for third-order parameters. See my "Plato and the foundations of mathematics" paper on arxiv. | |
| Aug 13, 2020 at 15:33 | answer | added | Sam Sanders | timeline score: 3 | |
| Jul 23, 2020 at 9:39 | comment | added | Fedor Pakhomov | It seems to me that in a similar way it is possible to show that over some some reasonable base system of higher-order reverse math (I guess something like $\mathsf{RCA}_0^{\omega}+\exists^2$ would work here) the third-order Dedekind completeness principle will be equivalent to the variant of $\Pi^1_1\textsf{-CA}_0$ that allows higher order parameters. Unfortunately, I am not comfortable enough with higher-order reverse math to write an answer. | |
| Jul 23, 2020 at 9:35 | comment | added | Fedor Pakhomov | It is fairly easy to show that over $\mathsf{ACA}_0$ Dedekind completeness for $\Pi^0_\infty$-sets of reals is equivalent to $\Pi^1_1\textsf{-CA}_0$. It is possible to derive $\Pi^1_1\textsf{-CA}_0$ from this form of Dedekind completeness using the fact that $\Pi^1_1\textsf{-CA}_0$ equivalent over $\mathsf{ACA}_0$ to the principle "every ill-founded tree $T\subseteq \omega^{<\omega}$ has a leftmost path." The latter equivalence could be proved using Kleene's normal forms for $\Pi^1_1$-sets. | |
| Jul 22, 2020 at 15:14 | comment | added | François G. Dorais | $\Pi^1_1$-CA (allowing third order parameters) is surely enough. Given a nonempty $X \subseteq \mathbb{R}$ which is bounded above, we can form the set $U = \{ q \in \mathbb{Q} : (\forall x \in \mathbb{R})(r \in X \to r \leq q)\}$ of all rational upper bounds of $X$ using $\Pi^1_1$-comprehension with parameter $X$. Note that $U$ is really just a second-order object, so $\inf U$ exists (by arithmetic comprehension) and $\sup X = \inf U$. So there is no need for any third-order axioms per se. | |
| Jul 22, 2020 at 14:02 | history | asked | Keshav Srinivasan | CC BY-SA 4.0 |