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.

Madeleine Birchfield (Jul 06 2024 at 01:42):

Reid Barton said:

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.

Quick question, do the Dedekind real numbers and Cauchy real numbers coincide in the topos of condensed sets?

Madeleine Birchfield (Aug 04 2024 at 17:51):

So in constructive mathematics, not every Cauchy real number has a base $b$ radix expansion in the absence of (Cauchy-analytic) WLPO, but does every irrational Cauchy real number (in the sense of being apart from a rational number) have a non-repeating base $b$ radix expansion? Here, we're talking about having the structure rather than mere existence.

Andrew Swan (Aug 04 2024 at 17:58):

Yes, if a real number is apart from every rational, then in particular it is either strictly greater or strinctly smaller than every finite radix approximation, so you can just build up the radix expansion inductively.

Madeleine Birchfield (Aug 04 2024 at 19:28):

Does the converse hold? i.e. does every non-repeating (infinite) base $b$ radix expansion converge to a Cauchy irrational number?

Andrew Swan (Aug 04 2024 at 19:50):

I guess that would work, as long as non-repeating is stated with a sufficiently strong formulation. I think the usual proof that rational numbers repeat should work constructively, so if a number is apart from every repeating radix expansion, it must be apart from every rational.

Madeleine Birchfield (Aug 04 2024 at 19:58):

Then I guess it comes down to defining the apartness relation on base $b$ radix expansions, so that non-repeating is defined as apart from all repeating radix expansions.

Andrew Swan (Aug 04 2024 at 20:03):

Right. It would be enough that for every digit there exists a later digit that is not the same.

Madeleine Birchfield (Aug 04 2024 at 20:27):

Base $b$ radix expansions can be defined as (integer, sequence of digits) pairs; i.e. elements of $\mathbb{Z} \times (\mathbb{N} \to \mathrm{Fin}(b))$, where $\mathrm{Fin}(b)$ is a finite set of cardinality $b$. The apartness relation on $\mathbb{Z}$ is given by negation of equality $k \neq m$, while the apartness relation on $\mathbb{N} \to \mathrm{Fin}(b)$ is given by $\exists n:\mathbb{N}.x(n) \neq y(n)$, and so the apartness relation on $\mathbb{Z} \times (\mathbb{N} \to \mathrm{Fin}(b))$ is defined as the disjunction of the apartness relations of its component.

Madeleine Birchfield (Aug 04 2024 at 20:29):

Andrew Swan said:

Right. It would be enough that for every digit there exists a later digit that is not the same.

Also this wouldn't work because it isn't just that single digits repeat, but that finite lists of digits can also repeat in a repeating radix expansion. So one would have to quantify over finite sublists of the sequence of digits.

Madeleine Birchfield (Aug 04 2024 at 20:43):

I had been wondering about the definition of the real numbers in some textbooks. The textbooks defined the rational numbers, and then they define the Cauchy irrational numbers via non-repeating base 10 radix expansions, and then they assume analytic LPO by stating that every real number is either a rational number or a (Cauchy) irrational number, with most of classical real analysis following from this assumption.

Andrew Swan (Aug 04 2024 at 20:46):

Madeleine Birchfield said:

Andrew Swan said:

Right. It would be enough that for every digit there exists a later digit that is not the same.

Also this wouldn't work because it isn't just that single digits repeat, but that finite lists of digits can also repeat in a repeating radix expansion. So one would have to quantify over finite sublists of the sequence of digits.

Oh, you're right - it should be that for all n and a, there is k and x such that the a + kn + x digit is different from the a + x digit.