Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Radix expansions in constructive mathematics

Madeleine Birchfield (Jan 28 2024 at 14:06):

According to the nLab article on [[radix notation]], the analytic LLPO is equivalent to the statement that for every real number there exists a radix expansion. However the nLab article on [[principle of omniscience]] states that the analytic LLPO is equivalent to the statement that every real number has a radix expansion, which can be interpreted as that every real number has a radix expansion as structure. Unless one can construct a radix expansion for a real number from mere existence of a radix expansion for the real number, having a radix expansion as structure is stronger than the mere existence of a radix expansion. So which statement is equivalent to the analytic LLPO, mere existence of a radix expansion for all real numbers or the structure of a radix expansion for all real numbers?

Madeleine Birchfield (Jan 28 2024 at 14:21):

Mere existence and structure do not coincide for signed radix expansions for real numbers. If for every real number there exists a signed radix expansion, this just implies that the Cauchy real numbers and Dedekind real numbers are isomorphic via theorem 6.9.7 of Auke Booij's thesis at https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf. If every real number has a signed radix expansion as structure, this implies the WLPO via lemmas 6.10.1 and 6.10.2 and theorem 6.9.5, which in turn is equivalent to the analytic WLPO because the Cauchy real numbers and Dedekind real numbers are isomorphic.

Since every radix expansion of a real number is a signed radix expansion of a real number, this would imply that the analytic LLPO is simply the mere existence of a radix expansion for all real numbers, since having radix expansions as structure for all real numbers would also imply the analytic WLPO, which is not the same as the analytic LLPO.

Andrew Swan (Jan 28 2024 at 15:20):

There can't be a function choosing a binary expansion for each Dedekind real without having analytic WLPO: Define $f : \mathbb{R} \to 2$ so that $f(x) = 0$ if the first digit in the expansion is greater than or equal to $0$ and $1$ otherwise. If $f(0) = 0$, then $x = 0$ iff $f(-|x|) = 0$, and if $f(0) = 1$ then $x = 0$ iff $f(|x|) = 1$.
I'm not 100% convinced the mere existence follows from analytic LLPO either without WCC, but I have to think about that some more. Note that the existence of radix expansion implies the existence of a Cauchy sequence.

Reid Barton (Jan 28 2024 at 17:54):

I wouldn't expect the nLab to be globally consistent about the exact constructive meaning of phrases like "every Dedekind real number has ...".

Reid Barton (Jan 28 2024 at 17:58):

Condensed sets (and probably many other topoi of similar nature) satisfies $\forall x : \mathbb{R}. \, x \le 0 \vee x \ge 0$, but every function $\mathbb{R} \to 2$ is constant.

John Baez (Jan 28 2024 at 18:26):

Please, folks, don't be shy about editing the nLab and changing a phrase like "every Dedekind real number has ..." to something that's more precise in a constructive context, at least if 1) constructive mathematics is close to the focus of the passage in question and 2) you know how to make it more precise.

Madeleine Birchfield (Jan 28 2024 at 19:34):

Andrew Swan said:

Note that the existence of radix expansion implies the existence of a Cauchy sequence.

One could do better and say that the existence of a radix expansion for a real number $x$ implies the existence of a monotonic Cauchy sequence of rational numbers which converges to $x$. Similarly, from the structure of a radix expansion for a real number $x$, one can construct a monotonic Cauchy sequence of rational numbers which converges to $x$. Do the reverse implications hold as well in general? If not, under what conditions do the reverse implications hold?

John Baez (Jan 28 2024 at 21:55):

Can you have a monotone Cauchy sequence that converges to $x$ yet still not know how long you need to wait for its $n$ th decimal digit to agree with that of $x$? I think part of the answer to this depends on what you constructivists mean by "converge to $x$" . Do you just know that for each $\epsilon > 0$ it eventually will come within $\epsilon$ of $x$ but not how long you need to wait, or do you know how long you need to wait?

John Baez (Jan 28 2024 at 21:57):

Also, do you folks accept both 0.99999999... and 1.0000000... as valid decimal expansions of 1?

Mike Shulman (Jan 29 2024 at 00:30):

Usually constructivists require that Cauchy sequences have a specified "modulus of convergence", i.e. a function $\epsilon \mapsto N$ such that blah blah, or equivalently that they all use some standard such modulus, e.g. always $|x_m-x_n| < \frac{1}{m} + \frac{1}{n}$.

Mike Shulman (Jan 29 2024 at 00:31):

I don't know how much it changes the notion of real number if you require only a truncated $\forall\epsilon \exists N$.

John Baez (Jan 29 2024 at 02:03):

If a Cauchy sequence $x_i$ comes with a specified modulus of convergence, I believe from that we can compute a function $n \mapsto N$ such that all terms $x_i$ with $i > N$ will have the same first $n$ decimal places, if we take the relaxed attitude that, e.g., 1.29998 and 1.30001 share the first 4 decimal places (i.e., 2999 and 3000 count as 'the same').

Andrew Swan (Jan 29 2024 at 09:47):

John Baez said:

If a Cauchy sequence $x_i$ comes with a specified modulus of convergence, I believe from that we can compute a function $n \mapsto N$ such that all terms $x_i$ with $i > N$ will have the same first $n$ decimal places, if we take the relaxed attitude that, e.g., 1.29998 and 1.30001 share the first 4 decimal places (i.e., 2999 and 3000 count as 'the same').

Yes, that's right. As a variation on this you can always find radix expansions if you allow digits to be negative (so you can "guess" 1.3 as an approximation and then if the real turns out to actually be 1.29998 you can write it as 1.3000-2.

Andrew Swan (Jan 29 2024 at 09:48):

I've convinced myself that there are computable Cauchy sequences with no computable binary expansion - if that works then Lifschitz realizability provides a model where LLPO holds but not every real has a binary expansion.

Andrew Swan (Jan 29 2024 at 10:02):

Madeleine Birchfield said:

Andrew Swan said:

Note that the existence of radix expansion implies the existence of a Cauchy sequence.

One could do better and say that the existence of a radix expansion for a real number $x$ implies the existence of a monotonic Cauchy sequence of rational numbers which converges to $x$. Similarly, from the structure of a radix expansion for a real number $x$, one can construct a monotonic Cauchy sequence of rational numbers which converges to $x$. Do the reverse implications hold as well in general? If not, under what conditions do the reverse implications hold?

In general you can't show convert a monotonic Cauchy sequence to a binary expansion without LLPO - given a binary sequence $\alpha$ with at most one 1, define a Cauchy sequence $q_n$ as $q_n = -2^{-n}$ if $\alpha(m) = 0$ for $m \leq n$, $q_n = -2^{-m}$ if $\alpha(m) = 1$ for even $m \leq n$ and $q_n = 2^{m}$ if $\alpha(m) = 1$ for odd $m \leq n$. Then knowing whether the first digit of the binary expansion is 0 or -1 tells you whether $\alpha(2n) = 0$ for all n or $\alpha(2n + 1) = 0$ for all n.

Andrew Swan (Jan 29 2024 at 10:50):

I modify what I said above about Lifschitz realizability - computable real numbers do have computable binary expansions, but this can't be done in a uniform way, and it is possible to use this to show not every Cauchy real has a binary expansion in Lifschitz realizability (which does have LLPO).

Reid Barton (Jan 29 2024 at 16:53):

And this is because it is missing countable choice, right?

Andrew Swan (Jan 29 2024 at 17:21):

Yes, in fact even weak countable choice must fail, which I'm not sure if I noticed before.

Madeleine Birchfield (Jan 29 2024 at 17:39):

I wonder how much of the use of (weak) countable choice in constructive real analysis could be replaced with (weak) countable choice for only surjections out of the real numbers.

Andrew Swan (Jan 29 2024 at 18:19):

Yes, there's a lot of scope for weakening weak countable choice. As well as restricting to functions that can choose reals you can combine with $\mathbf{AC}_{\mathbb{N}, 2}$ to look at functions where "every set has at most 2 elements and all except at most one has 1." There's a weaker choice principle in the paper by Escardó and Knapp at https://doi.org/10.4230/LIPIcs.CSL.2017.21 that follows from LPO and they use for various results. You can even combine that with $\mathbf{AC}_{\mathbb{N}, 2}$ to get something possibly weaker still.

Morgan Rogers (he/him) (Jan 30 2024 at 09:40):

Andrew Swan said:

Yes, there's a lot of scope for weakening weak countable choice.

Removing the context from this, I find it delightfully surprising as a statement! The foundations are a lot deeper than I had seen before.

Madeleine Birchfield (Feb 03 2024 at 03:46):

Andrew Swan said:

Yes, there's a lot of scope for weakening weak countable choice. As well as restricting to functions that can choose reals you can combine with $\mathbf{AC}_{\mathbb{N}, 2}$ to look at functions where "every set has at most 2 elements and all except at most one has 1." There's a weaker choice principle in the paper by Escardó and Knapp at https://doi.org/10.4230/LIPIcs.CSL.2017.21 that follows from LPO and they use for various results. You can even combine that with $\mathbf{AC}_{\mathbb{N}, 2}$ to get something possibly weaker still.

Probably another few axioms derivable from (weak?) countable choice one could use are

1. there exists a $\sigma$-frame, or an initial $\sigma$-frame (This could probably be constructed impredicativity as the intersection of all $\sigma$-subframes of the set of truth values)
2. the set of semi-decidable truth values $\Sigma_0^1$ is a $\sigma$-frame

One can construct a version of the Dedekind real numbers using the $\sigma$-frame, which makes it amenable to predicativists, but in either case the asssociated localic real numbers are only a $\sigma$-locale instead of a locale, which probably has topological and analytic consequences causing it to behave differently from the usual Dedekind real numbers and localic real numbers defined using the set of truth values.

Madeleine Birchfield (Feb 03 2024 at 03:51):

One can also use the stronger axiom, independent of countable choice (I think) but implied by excluded middle, that

3. the set of decidable truth values $2$ is the initial $\sigma$-frame

Then the classical construction of the Dedekind real numbers using functions from $\mathbb{N}$ to $2$ is possible. Unless $2$ being a $\sigma$-frame implies that $2$ is a frame, this should be weaker than excluded middle.