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:
U and L are sets of rationals
If x in L and y in U, then x < y
U is upwards-closed; for any x < y with x in U, y is in U
L is downwards-closed
U is downwards-rounded (open); for any x in U, there exists a y < x such that y is in U
L is upwards-rounded
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:
U is inhabited
L is inhabited
(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:
For any x < y, either x is in L or y is in U
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.
The power of this seems similar to the power of constructive Cauchy sequences because you can use the (x < y) → A u B function to approximate the value to any positive precision error.
If you have (x<y)→A∪B, then I think that’s true, but if you just have (x<y)→||A∪B|| (where ||−|| is propositional truncation, basically quotienting by the relation that is always true, so collapsing the two sides to be indistinguishable), then the homotopy type book suggests that it might be wrong.
It’s a bit similar to how the naive types-as-propositions encoding of the axiom of choice makes it trivially provable constructively, but a more careful encoding makes it imply excluded middle.
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:
U and L are sets of rationals
If x in L and y in U, then x < y
U is upwards-closed; for any x < y with x in U, y is in U
L is downwards-closed
U is downwards-rounded (open); for any x in U, there exists a y < x such that y is in U
L is upwards-rounded
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:
U is inhabited
L is inhabited
(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:
For any x < y, either x is in L or y is in U
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.
I guess to clean it up even further:
A set L is a lower real number when it is inhabited, downwards-closed and upwards-rounded.
A set U is an upper real number when it is inhabited, upwards-closed and downwards-rounded.
A closed interval [sup L, inf U] is constructed with a lower real L and an upper real U such that L < U.
A closed interval [sup L, inf U] is a real number if every rational interval x < y either has x < sup L or inf U < y.
The power of this seems similar to the power of constructive Cauchy sequences because you can use the (x < y) → A u B function to approximate the value to any positive precision error.
If you have (x<y)→A∪B, then I think that’s true, but if you just have (x<y)→||A∪B|| (where ||−|| is propositional truncation, basically quotienting by the relation that is always true, so collapsing the two sides to be indistinguishable), then the homotopy type book suggests that it might be wrong.
It’s a bit similar to how the naive types-as-propositions encoding of the axiom of choice makes it trivially provable constructively, but a more careful encoding makes it imply excluded middle.