Timeline for The approximate mean value theorem / Rolle's theorem in pure constructive mathematics
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 18, 2023 at 18:00 | comment | added | Nikolaj-K | I can't predict to what extent it helps you with your question, but I found this Phd thesis (Schuster, 2013) to be a nice resource, as well as this constructive reverse math text (Diener, 2020). The IVT in the context of different axioms plays a role in both. | |
| Nov 6, 2023 at 10:28 | comment | added | SpectreDNZ | In this regard also, I believe anything used for equivalence classes of Cauchy sequences could be translated into something about the Dedekind reals with countable choice, so I'd just take such a proof as saying that we at least need countable choice. Any proof using the Bishop setoid construction, as Mike himself pointed out in the comments of an answer, would be a proof about Cauchy sequences rather than about real numbers. And as Andrej Bauer has repeatedly given as a sentiment, attempting to Cauchy complete the rationals using Cauchy sequences without choice is too arduous a task. | |
| Nov 6, 2023 at 10:21 | comment | added | SpectreDNZ | @Gro-Tsen This was meant to be follow up to Mike Shulman's question (In fact, I thought it to be uncannily similar to it as a question, but there weren't any I could find on this specific topic), and the proof that was given to it in particular. I believe Dedekind reals would be the most optimal, as they seem to be the most concise and useable in a choiceless "least amount of assumptions" sort of environment. So one may approximate any real arbitrarily well with a single rational, but there might not be a Cauchy sequence of such rationals for said real. | |
| Nov 5, 2023 at 22:18 | comment | added | Gro-Tsen | Well, to start with, in “pure constructive mathematics” (I'm not sure what exactly you mean by that, but I assume something like IZF or the internal logic of a topos, so without even Countable Choice), there is no reason for Cauchy reals and Dedekind reals to be the same (and even “Cauchy reals” can mean several different things, I can think of at least three), so the answer to your question probably depends on exactly what sort of real numbers you want to talk about. | |
| Nov 5, 2023 at 22:12 | history | edited | YCor | CC BY-SA 4.0 |
removed capitals from title
|
| S Nov 5, 2023 at 19:08 | review | First questions | |||
| Nov 5, 2023 at 20:44 | |||||
| S Nov 5, 2023 at 19:08 | history | asked | SpectreDNZ | CC BY-SA 4.0 |