BIG EDIT: I decided to re-write this question completely as it was first posted with a lot of misunderstandings on my part and unclear statements. Trying to edit it - with feedback from the lovely people that took time to try and understand it - just made it worse.

TL;DR: Are we not required to be able to construct a working example, say of a theoretically working calculator, when proving a construction of the real numbers? It is not my understanding that we're required to in general mathematics (since constructive mathematics exists), but if we're not - on what grounds then do we consider a construction proved?

First post here - and must I say how I admire all of you taking so much of your time to make information so readily available and understandable!

I'm beginning my university studies in math this summer, and so I'm fairly green - only a curious high school student. I have experience with programming.

Introduction to my question:

I'm trying to understand when something is considered proven. It is the construction of the real numbers using Dedekind cuts that I have a hard time understanding being considered proven, when reading or watching videos about the construction on the internet, or in the textbook I have: “Classic Set Theory” by Derek Goldrei. I do not feel the same way about the construction via Cauchy sequences, and I will try to explain why. EDIT for other novices finding this: I realize I should have made it clear that what I'm talking about here are definitions, and made it more explicit that talking about 'proving' a definition (in itself) is normally not a correct way of using the word 'proof'. What we normally do prove (and to me that part is proven satisfactory) are that our definition of real numbers satisfy the axioms of a complete ordered field. What I had a hard time understanding though, was that definitions could be widely accepted of something like a >construction<, without it being shown that the 'inner workings' of such a construction could actually 'work in practice'. I was somehow in disbelief about that, I guess mostly from having a programmer's mindset about definitions. In programming all code consists of definitions, but these definitions (obviously) have to succeed in doing the intended thing, for them to be considered 'accepted' - but math is not programming (and I think that is a good thing), and hence is not only about 'doing'. I do think though, that I've realized in all of this, that I'm philosophically a mathematical constructivist.

I'm unsure if it makes me a 'constructivist', but I expect that we would be able to (at least in theory) construct a calculator (ie. code a program) using a given representation of the real numbers, for that representation to be considered a proven representation. I expect such a 'calculator' would be able to perform computations using the standard field operations. It seems to me that is also why we define the sums and products of, in this case, Dedekind left cuts when we define the construction of the reals as Dedekind cuts? I might be wrong.

I expect of such a 'calculator' that I could give give it, say something like $\sum_{i=1}^∞ \frac{1}{i^2}$ and $\sum_{i=0}^∞ \frac{1}{i!}$ as input, and tell it to compute $e(\frac{\pi^2}{6}+15)$ and as a result it would be able to give as output as many digits of this computation as I would wish, if it was given enough time.

I know this can be done using infinite sums and for example taking the Cauchy product of these series, and I do not find it so hard either to imagine a program that would be able to do this with the construction of the reals using Cauchy sequences, as long as we programmatically define fx the equality operator 'directly', so to say, instead of involving the set theory of equivalence classes. We would also do some clever programming to automate the epsilon-delta type of proofs usually involved in the definitions of the equivalence relation usually involved (but here programmed directly into the comparison operators). Such a program could then both output the result of fx the calculation given above, and when comparing two 'Cauchy sequence representations' of reals, it would both be able to output whether one is less than another / equal to it, and also the epsilon-delta-type proof it made to prove that it is so. Such a program would in my mind use metaprogramming, and we would essentially internally represent a real number as an algorithm, and manipulate these algorithms when calculating.

I do not, on the other hand, find it easy to envision such a calculator program which would use Dedekind left cuts as its 'inner representation' of numbers. I will detail why in the very end, because this is a very long question, I am aware.

Start of my question:

As I understand it (and this is just an example) when we prove that the rationals are countable, then we require the one proving to give an example of a bijective function between the rational numbers and the natural numbers, or I guess at least a surjective one from the naturals to the rationals. The usual example given to a novice like me is a 'snaking' function illustrated visually on this picture from wikipedia:

From https://en.wikipedia.org/wiki/Pairing_function

When watching several of the youtube videos on the 'Hilbert’s Hotel Paradox' or on the cardinality of infinite sets, the requirement for a function such as the 'snaking' function, is given on the grounds that we can't simply 'take one row at a time' since each row is infinite, and so we would never 'reach' the next row. This makes perfect sense to me. As I understand the Cauchy product, it has the same logic behind it, and I guess can also be said to be a kind of 'snaking' function.

To program a calculator with Dedekind left cuts as its 'inner representation' of numbers we would run into a similar problem as far as I can figure it out, where we would 'get stuck in an infinite sequence' without being able to output the results of our calculations in the manner described above in the introduction.

The actual question:

How am I as a novice to understand that we seem to require different 'standards of proving' in two situations both involving infinite sets of rational numbers?

In one situation we require an example function to be given (that is an example construction, I guess in constructivist sense), and in another we 'can get away with' defining a real number to be “1) a proper, non-empty subset of $\Bbb Q$ 2) that is 'closed to the left' 3) and has no maximum element.” (details left out, as I assume you know this), and then define the sum and product of such sets, without having to explain how we do not fx 'get stuck in an infinite sequence' without being able to output (as much as we want of) the infinite sequence representing the actual result of a given sum/product?

From what I’ve seen, the example of a 'Dedekind left set representation' of a real number then usually is given as:

$\mathbf{r} = \{q\in\Bbb Q: q^2 <_\Bbb Q 2$ or q is negative$\}$

Which is an algebraic number, and not a transcendental one, and also an example I actually can envision constructing an algorithm to list (as much as I want) the left set of, using a 'snaking' function with the comparison test '$q^2 <_\Bbb Q 2$ or q is negative'.

But I cannot on the other hand figure out how we would be able to code such an algorithm for a transcendental number, that cannot be defined merely by a simple comparison like the above. And that was after all the point to begin with, as we were not merely trying to construct the algebraic numbers? I can't think of any other way right now than coding the Cauchy construction (as detailed in the introduction) and then for each rational in the Cauchy sequence (say of partial sums of one of the famous series for 𝜋) to use use a 'snaking' function to list all rationals less than it - except that it is an infinite process and we would never 'reach' the next rational in the Cauchy sequence?? The algorithm wouldn't succeed for exactly the same reason that we can't simply 'take one row at a time' in the example of proving the rationals to be countable? Please correct me if I’m wrong!

Edited after accepting the answer: From my limited knowledge it seems that the standard definition of Dedekind cut reals, given fx in my book, are taken to be 'proven' (I know they are definitions, but say 'accepted' then) on the grounds of the ZF axioms, and in my mind are especially related here the Axiom of Separation combined with the Axiom of Infinity. They are then proven to satisfy the axioms of a complete ordered field, but in my mind that comes somehow 'after', I guess because I'm wondering from a philosophical/ontological point of view. In what sense they 'exist'. I have realized after being answered that this kind of wondering just mean I have to do some studiying constructive mathematics :) I have tried to edit the title to better reflect the content that was answered.

I hope I'm able to explain myself. Thank you so much for your time if you read all of this!! I would really like to understand this :)

All the best, Isa

  • 1
    $\begingroup$ In constructive mathematics, which is much closer to programming, the Dedekind and Cauchy completions of the rationals may not be isomorphic. Your question seems to be much more about that rather than the axiom of choice. $\endgroup$
    – Asaf Karagila
    Apr 22, 2023 at 10:48
  • 1
    $\begingroup$ The post has some overhead, like that you're from Denmark, that some people supposedly have double standards and that people would be insisting on criss-crossing. It's not clear to me what you're really looking for. Given an effective method to compute when a rational number is smaller than some given real $r$, Dedekind cut or not, you'll be able to compute a digit expansion. For this you don't need to compare other irrational numbers with $r$. Not all numbers that you can define and from axioms prove to exist constitute a computable number. $\endgroup$
    – Nikolaj-K
    Apr 22, 2023 at 14:40
  • 4
    $\begingroup$ Yes, the rationals are countable in that there are surjections $f\colon {\mathbb N}\to {\mathbb Q}$. Yes, by starting to go through all $n\in{\mathbb N}$ and checking $f(n)<r$, you can attempt to get information about a given, comparable transcendental number. But that's not the process that necessarily needs to be performed to compute the decimal expansion and so it's not clear to me why the countability aspect of the rationals even makes it into a question concerning the Dedekind reals that are computable. $\endgroup$
    – Nikolaj-K
    Apr 22, 2023 at 15:12
  • 1
    $\begingroup$ Among the usual assumptions about computability is that a number is computable if there exists a Turing machine that can compute it. There are only a countable number of Turing machines and therefore only a countable number of computable numbers. As for what it means to "compute" a number, you should at least be able to decide whether or not any given rational number is less than your computable number or greater. Then you can enumerate the Dedekind cut of your number by snaking through the rationals and only accepting numbers less than yours. Does this relate to your question? $\endgroup$
    – David K
    Apr 22, 2023 at 18:44
  • 1
    $\begingroup$ The "programming" aspect of this question appeals to me since after my math undergrad I ended up getting my PhD in CS instead. Using a "calculator" (that is, a computer of some kind) to compute with real numbers is a very interesting topic that is also full of pitfalls that I think you are not aware of. I would like to address some of those but it will have to wait until tomorrow. $\endgroup$
    – David K
    Apr 23, 2023 at 2:17

1 Answer 1


You are correct that as you've defined them, constructive mathematics has issues with Dedekind cuts. This is why it is necessary to use a different definition of the Dedekind reals when working constructively.

Definition: a pair $(L, U)$, where $L, U \subseteq \mathbb{Q}$, is said to be a Dedekind cut pair when all of the following are satisfied

  • $L$ is downward closed, and $U$ is upward closed;
  • For all $\ell \in L$, there exists $\ell' \in L$ such that $\ell < \ell'$; similarly, for all $u \in U$, there exists $u' \in U$ such that $u' < u$ [roundedness];
  • There exists some $\ell \in L$, and there exists some $u \in U$ [inhabitedness];
  • $L \cap U = \emptyset$ [nonoverlapping]; and
  • For all $x, y \in \mathbb{Q}$, if $x < y$, then $x \in L$ or $y \in U$ [locatedness]

The Dedekind real numbers can then be defined to be the set of all Dedekind cut pairs.

Note that for all $L \subseteq \mathbb{Q}$, there exists at most one $U \subseteq \mathbb{Q}$ such that $(L, U)$ is a Dedekind cut pair. In fact, we can explicitly describe this candidate $U$ as $U = \{u \in \mathbb{Q} \mid \exists u' \in \mathbb{Q} (u' < u \land \forall \ell \in L (\ell < u'))\}$. It's a nice exercise to show that if $(L, U')$ is a Dedekind cut pair, then $U = U'$.

If $(L, U)$ is a Dedekind cut pair, then $L$ is a proper subset of $\mathbb{Q}$. For we can take some $u \in U$ by inhabitedness. Then $u \notin L$ by the nonoverlapping condition. Furthermore, $L$ is non-empty; this follows from inhabitedness. $L$ is also "closed to the left", or, as I phrased it, "downward closed". And $L$ has no maximum element, which follows from roundedness.

Conversely, suppose classical logic holds, and let $L$ be a proper, nonempty subset of $\mathbb{Q}$ with is downward closed and has no maximum element. Then there exists a (necessarily unique) $U$ such that $(L, U)$ is a Dedekind cut pair; as mentioned above, this $U$ is $U = \{u \in \mathbb{Q} \mid \exists u' \in \mathbb{Q} (u' < u \land \forall \ell \in L (\ell < u'))\}$. Thus, under classical logic, there is a canonical bijection between the set of Dedekind cut pairs, and the set of left Dedekind cuts. This bijection sends $(L, U)$ to $L$.

Here are some facts we can constructively prove about the Dedekind cut reals.

  • Let $x$ be a Cauchy sequence real. Then $(L_x, U_x)$ is a Dedekind cut real, where $L = \{q \in \mathbb{Q} \mid q < x\}$ and $U = \{q \in \mathbb{Q} \mid q > x\}$. Moreover, the map $\mathbb{R}_{Cauchy} \to \mathbb{R}_{Dedekind}$ given by $x \mapsto (L_x, U_x)$ is injective. Thus, we can identify $\mathbb{R}_{Cauchy}$ with a subset of $\mathbb{R}_{Dedekind}$.
  • If we assume an extremely weak version of the countable choice, then the above injection is actually a bijection. Thus, the Cauchy and Dedekind real numbers are the same.
  • We can approximate a Dedekind cut real number arbitrarily well by a rational number. For all $n \in \mathbb{N}_+$ and all $(L, U) \in \mathbb{R}_{Dedekind}$, there exists $q \in \mathbb{Q}$ such that $q \in L$ and $q + 1/n \in U$.

Let's return to your discussion of how you could implement a calculator for Dedekind reals. One way to represent a Dedekind cut $(L, U)$ would be as a tuple $(\ell, u, f, g, h)$, where $\ell \in L$, $u \in U$, $f : L \to L$, $g : U \to U$, and $h : \{(x, y) \in \mathbb{Q}^2 \mid x < y\} \to \{0, 1\}$, which has the following properties.

First, for all $x \in L$, $f(x) > x$. Second, for all $x \in U$, $g(x) < x$. Third, for all $x, y \in \mathbb{Q}$ such that $x < y$, if $h(x, y) = 0$, then $x \in L$, and if $h(x, y) = 1$, then $y \in U$.

With a reasonable amount of cleverness, one could then implement the various operations on real numbers that we all know and love.

One extremely important point is that your Cauchy reals calculator - and this Dedekind reals calculator - cannot actually compute whether two computable real numbers are equal. This is provably impossible.

If you want more information on constructive analysis, one good source is Bishop's Foundations of Constructive Mathematics.

  • 1
    $\begingroup$ You have definitely done a better job at convincing me than any material I've come upon so far. I'm very grateful. And how eloquently! Deep respect. And I like that you give it to me as a homework excersie to conjure up an example rule for the function h(x,y) :) I'm so looking forward to my university studies right now. And thanks a lot, I will definitely take a look at the book. If I can't figure out a rule for h(x,y), will that book maybe help me to? Or some other book? :) My deepest respect for taking your time to answer something like this! $\endgroup$
    – Isa_Degn
    Apr 23, 2023 at 20:07
  • 1
    $\begingroup$ I have accepted your answer, since I have become aware that I really have asked two big questions at once - and you have definitly answered one of them in a way that was very enlightening for me. The difference between math and programming has also definetly become clearer. The other question about the axiomatic foundation on which the Dedekind construction stands in classical mathematics is I quess also something I should and could be able find an answer to by more reading. Thank you again. $\endgroup$
    – Isa_Degn
    Apr 23, 2023 at 20:26
  • $\begingroup$ When you say "cannot actually compute whether two computable real numbers are equal", do you then mean that if all we have is, say, the sequence of rational elements in a given Cauchy sequence but have no access to the algorithm computing the elements of the sequence? $\endgroup$
    – Isa_Degn
    Apr 23, 2023 at 20:50
  • 1
    $\begingroup$ @Isa_Degn No, that’s not what I mean. Let’s say we have an algorithm that computes a function $f : \mathbb{N} \to \{0, 1\}$. Consider the number $x = \sum\limits_{i = 0}^\infty \frac{f(n)} {10^n}$, which is the number whose $i$th digit after the decimal place is given by $f(i)$. Computing whether $x = 0$ amounts to computing whether for all $n$, $f(n) = 0$. It turns out this is impossible. Intuitively, we don’t know how many digits we would need to compute before concluding all digits are zero. $\endgroup$ Apr 23, 2023 at 23:58
  • $\begingroup$ I am honered that you take time to answer me Mark, thank you, and realize I should probably have felt more honered to begin with. You don't need to read the rest of this comment. -- I still did not understand exactly what had been proven, but this time I made more serious attempt of finding the answer online. For others interested: mathoverflow.net/questions/40618/… The wiki-page on computable numbers (lacks citations) says the situation is different if the modulus of convergence is known. See also: computable analysis. $\endgroup$
    – Isa_Degn
    Apr 24, 2023 at 7:37

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .