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:
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
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
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'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.