Timeline for Has an uncomputable variant of the Cantor staircase ever been used in constructive logic?

Current License: CC BY-SA 4.0

28 events

when toggle format	what		by	license	comment
Dec 30, 2022 at 20:49	comment	added	LSpice		Title of @AndrejBauer's talk referenced above: The countable reals.
Dec 30, 2022 at 20:48	history	edited	LSpice	CC BY-SA 4.0	Name of question; punctuation inside `\begin{cases}`
Dec 30, 2022 at 19:31	history	edited	wlad	CC BY-SA 4.0	improved readability of formulas
Dec 25, 2022 at 17:44	comment	added	Andrej Bauer		Yes, but I have nothing to say at the moment. I would find it rather incredible if such a topos existed.
Dec 25, 2022 at 14:59	history	edited	wlad	CC BY-SA 4.0	edited body
Dec 25, 2022 at 14:27	history	edited	wlad	CC BY-SA 4.0	deleted 13 characters in body
Dec 25, 2022 at 14:17	history	edited	wlad	CC BY-SA 4.0	Eliminated some brackets
Dec 25, 2022 at 14:08	comment	added	wlad		@AndrejBauer Did you see my response about $\mathsf{Hom}(\mathbb{R}, \mathbb{R})$?
Dec 25, 2022 at 13:58	comment	added	Andrej Bauer		Yes, James and I need to finish up the paper, so far this talk is available: youtube.com/watch?v=4CBFUojXoq4
Dec 25, 2022 at 13:57	comment	added	wlad		@AndrejBauer I mean all classically continuous functions $\mathbb R^c \to \mathbb R^c$.
Dec 25, 2022 at 13:57	comment	added	Andrej Bauer		I don't think that can be done. If $h \in \mathsf{Hom}(\mathbb{R}, \mathbb{R})$ then $h(0) \in \mathbb{R}$, so if every classically continuous function appears in $ \mathsf{Hom}(\mathbb{R}, \mathbb{R})$ then all classical reals will appear in $\mathbb{R}$. Maybe I misunderstand your idea.
Dec 25, 2022 at 13:55	comment	added	wlad		@AndrejBauer There's a topos in which $\mathbb R$ is countable? So that open problem has been settled then.
Dec 25, 2022 at 13:55	comment	added	wlad		@AndrejBauer I think we need the internal $\mathbb R$ to correspond to external $\mathbb R^c$, but the morphisms $\mathbb R \to \mathbb R$ to correspond externally to all the classically continuous functions.
Dec 25, 2022 at 13:55	comment	added	Andrej Bauer		You could use the topos constructed by James Henson and myself in which $\mathbb{R}$ is countable. I still don't see how you're going to define $F$, though. There's lots of excluded middle in the definition you wrote.
Dec 25, 2022 at 13:53	comment	added	wlad		@AndrejBauer The effective topos doesn't work because I need countable choice to fail.
Dec 25, 2022 at 13:53	comment	added	Andrej Bauer		A topos that would satisfy your criteria is the effective topos, but I don't see how the sequence $(F_n)_n$ would be computable (each $F_n$ is computable, but the sequence itself doesn't seem to be). P.S.: The discussion about $\Omega$ is a red herring.
Dec 25, 2022 at 13:49	history	edited	wlad	CC BY-SA 4.0	added 30 characters in body
Dec 25, 2022 at 13:47	comment	added	wlad		The internal logic of the topos does not prove the existence of an uncomputable number.
Dec 25, 2022 at 13:43	comment	added	wlad		@JoelDavidHamkins Because it only exists in the external logic.
Dec 25, 2022 at 13:43	history	edited	wlad	CC BY-SA 4.0	added 1171 characters in body
Dec 25, 2022 at 13:18	comment	added	Joel David Hamkins		I am confused about the proposal. How do you intend to define the function in the topos without $\Omega$ being in the topos?
Dec 25, 2022 at 12:20	history	edited	wlad	CC BY-SA 4.0	edited title
Dec 25, 2022 at 12:12	comment	added	wlad		@Trebor The $\Omega$ is in the external logic.
Dec 25, 2022 at 12:11	history	edited	wlad	CC BY-SA 4.0	deleted 1 character in body
Dec 25, 2022 at 12:11	comment	added	Trebor		How do you define $\Omega$ without LEM?
Dec 25, 2022 at 12:10	history	edited	wlad	CC BY-SA 4.0	deleted 1 character in body
Dec 25, 2022 at 12:09	comment	added	wlad		Should I ask this on a mailing list or somewhere else?
Dec 25, 2022 at 11:50	history	asked	wlad	CC BY-SA 4.0

toggle format