People generally use "rounded" cuts when defining Dedekind cuts constructively. When a rounded cut defines a rational number, that rational number is included in neither the upper nor the lower set.
More formally, you can constructively define a closed interval of real numbers, potentially containing infinity, as follows:
This corresponds to a closed interval of real numbers that ranges from [sup L, inf U].
(Well, sort of. The bounds of this interval cannot actually be iteratively approximated. I think there are some contexts where you want that, because it means there are more intervals that are constructively definable. For instance this type of interval is closed under arbitrary intersections, whereas if the bounds could be approximated, it would not be closed under arbitrary intersections. It's one of those things where constructive math takes a concept and shatters it into multiple. But you regain iterative approximateability later as you force it to refer to just 1 real number.)
You can then force the interval to be finite by saying:
(If you want it to be only finite in one direction, you could have only one of these statements. Another option is to include "L is inhabited" but then drop the U set from your definition, in which case you get lower reals, which are useful in measure theory IIRC.)
Real numbers can then be identified with the closed intervals of zero width, which can be forced as follows:
So basically if you have an approximation (x, y) in (L, U), you could e.g. take (2x+y)/3 < (x+2y)/3 and use this rule to tighten your bound.
Here U and L could be represented by functions A, B -> Q, but critically there would not be any straightforward functions back into A and B. The closest would be the final requirement, which could be taken to provide a function (x < y) -> A u B (strictly speaking one should probably have some appropriate quotients I'd guess), but if e.g. one of x and y is the actual value of the real number, then the function would always pick the answer corresponding to the other of the x and y.
In classical ZF and ZFC, there are two standard ways of defining reals: as Cauchy sequences and as Dedekind cuts. Classically, these are equivalent, but are inequivalent constructively. This makes a difference as to which real numbers are definable in type theory.
Cauchy sequences and Dedekind cuts in classical ZF
Classically, a Cauchy sequence is a sequence of reals x1,x2,…, such that for any ϵ>0, there is a natural N such that for any m,n>N, |xm−xn|<ϵ. Such a sequence must have a real limit, and the sequence represents this real number. Representing reals using a construction that depends on reals is unsatisfactory, so we define a Cauchy sequence of rationals (CSR) to be a Cauchy sequence in which each xi is rational.
A Cauchy sequence lets us approximate the represented real to any positive degree of precision. If we want to approximate the real by a rational within ϵ, we find N corresponding to this ϵ and use xN+1 as the approximation. We are assured that this approximation must be within ϵ of any future xi in the sequence; therefore, the approximation error (that is, |xN+1−limi→∞xi|) will not exceed ϵ.
A Dedekind cut, on the other hand, is a partition of the rationals into two sets A,B such that:
It represents the real number supA. As with Cauchy sequences, we can approximate this number to within some arbitrary ϵ; we do this by doing a binary search to find rationals x<y with x∈A,y∈B,|x−y|<ϵ, at which point x approximates supA to within ϵ. (Note that we need to find rational bounds on supA before commencing a straightforward binary search, but this is possible by listing the integers sorted by absolute value until finding at least one in A and one in B.)
Translating a Dedekind cut to a CSR is straightforward. We set the terms of the sequence to be successive binary search approximations of supA, each of which are rational. Since the binary search converges, the sequence is Cauchy.
To translate a CSR to a Dedekind cut, we will want to set A to be the set of rational numbers strictly less than the sequence’s limit; this is correct regardless if the limit is rational (check both cases). These constitute the set of rationals y for which there exists some rational ϵ>0 and some natural N, such that for every n > N, y+ϵ<xn. (In particular, we set some ϵ<12((limi→∞xi)−y), and N can be set so that successive terms are within ϵ of the limit).
We’re not worried about this translation being computable, since we’re finding a classical logic definition. Since CSRs can be translated to Dedekind cuts representing the same real number and vice versa, these formulations are equivalent.
Cauchy sequences and Dedekind cuts in constructive mathematics
How do we translate these definitions to constructive mathematics? I’ll use an informal type theory based on the calculus of constructions for these definitions; I believe they can be translated to popular theorem provers such as Coq, Agda, and Lean.
Defining naturals, integers, and rationals constructively is straightforward. Let’s first consider CSRs. These can be defined as a pair of values:
Satisfying:
∀(ϵ:Q,ϵ>0),(m:N,m>t(ϵ)),(n:N,n>t(ϵ)):|s(m)−s(n)|<ϵ
Generally, type theories are computable, so s and t will be computable functions.
What about Dedekind cuts? This consists of a quadruple of values
Where B is the Boolean type. A corresponds to the set of rationals for which a is true. The triple must satisfy:
a specifies the sets A and B; b and c show that A and B are non-empty; d maps an element of A to a greater element of A. The conditions straightforwardly translate the classical definition to a constructive one.
Let’s first consider translating Dedekind cuts to CSRs. We can use b and c as bounds for a binary search and generate successive terms in the binary search to get our Cauchy sequence. It is easy to bound the error of the binary search and thereby specify t.
The other way around is not possible in general.
Showing that not every constructive Cauchy sequence corresponds to a constructive Dedekind cut
I will show that there is a constructive CSR that cannot be translated to a constructive Dedekind cut, assuming a computable type theory.
This will use the framework of arbitration oracles, or consistent guessing in Scott Aaronson’s terms.
Let M be a Turing machine that does not necessarily halt, but returns a Boolean if it does halt. Let f(M) be equal to 0 if M doesn’t halt; if M halts in exactly n steps returning a boolean b, then, if b is true, f(M)=1/n, and if b is false, then f(M)=−1/n.
We will first try representing f as a function from Turing machines to CSRs. We will define s(M) to be a CSR for f(M). This is a simple approximation; to find s(M)i, we run M for i steps. If M has halted by then, we know f(M) and can set s(M)i=f(M). Otherwise, we set the approximation s(M)i=0
This sequence is (constructively) Cauchy since all terms past i are within 2/i of each other. This makes a valid t for the Cauchy sequence computable (we simply need t(ϵ)>2/ϵ).
On the other hand, f cannot be represented as a function returning a Dedekind cut. Suppose a(M) represents the A set for the Dedekind cut of f(M). We will specify g:M→B to be an arbitration oracle, by setting g(M)=a(M)(0). This is an arbitration oracle by cases:
Since arbitration oracles are uncomputable, this shows that it isn’t possible to represent f as a computable function returning a Dedekind cut.
Conclusion
While CSRs are equivalent to Dedekind cuts in classical logic, they are not equivalent in type theory. In type theory, every Dedekind cut can be translated to an equivalent CSR, but not vice versa. While a constructive CSR allows approximation to an arbitrary positive approximation error, a constructive Dedekind cut additionally allows exact queries to determine whether some rational is strictly greater than the represented real number.
This has implications for representing real numbers in type theory. I’m interested in this because I’m interested in constructive definitions of maximal lottery-lotteries in social choice theory, and I expect this to be relevant in other areas of math where constructive and computable definitions are desirable.