It looks as if you’re taking a constructive Dedekind cut to involve a “set of real numbers” in the sense of a function for distinguishing left-things from right-things.
Is that actually how constructivists would want to define them? E.g., Bishop’s “Foundations of Constructive Analysis”, if I am understanding its definitions of “set” and “subset” correctly (which I might not be), says in effect that a set of rational numbers is a recipe for constructing elements of that set, along with a way of telling whether two things constructed in this way are equal. I’m pretty sure you can have one of those but not be able to determine explicitly whether a given rational number is in the set, in which case your central argument doesn’t go through.
Are Cauchy sequences and Dedekind cuts equivalent if one thinks of them as Bishop does? There’s an exercise in his book that claims they are. I haven’t thought about this much and am very much not an expert on this stuff, and for all I know Bishop may have made a boneheaded mistake at this point. I’m also troubled by the apparent vagueness of Bishop’s account of sets and subsets and whatnot.
More concretely, that exercise in Bishop’s book says: a Dedekind cut is a pair of nonempty sets of rationals S,T such that we always have s<t and given rationals x<y either x is in S or y is in T. Unless I’m confused about Bishop’s account of sets, all of this is consistent with e.g. S containing the negative rationals and T the positive rationals, and not being able to say that 0 is in either of them. And unless I’m confused about your “arbitration oracles”, you can’t build an arbitration oracle out of that setup.
(But, again: not an expert on any of this, could be horribly wrong.)
Here’s how one might specify Dedekind cuts in type theory. Provide two types A,B with mappings a:A→Q, b:B→Q. To show these cover all the rationals, provide c:Q→A∨B such that the value returned by c maps back to its argument, through functions a or b. But this lets us re-construct a function Q→B by seeing whether c provides an A or a B. There are other ways of doing this but I’m not sure what else is worth analyzing.
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.
It looks as if you’re taking a constructive Dedekind cut to involve a “set of real numbers” in the sense of a function for distinguishing left-things from right-things.
Is that actually how constructivists would want to define them? E.g., Bishop’s “Foundations of Constructive Analysis”, if I am understanding its definitions of “set” and “subset” correctly (which I might not be), says in effect that a set of rational numbers is a recipe for constructing elements of that set, along with a way of telling whether two things constructed in this way are equal. I’m pretty sure you can have one of those but not be able to determine explicitly whether a given rational number is in the set, in which case your central argument doesn’t go through.
Are Cauchy sequences and Dedekind cuts equivalent if one thinks of them as Bishop does? There’s an exercise in his book that claims they are. I haven’t thought about this much and am very much not an expert on this stuff, and for all I know Bishop may have made a boneheaded mistake at this point. I’m also troubled by the apparent vagueness of Bishop’s account of sets and subsets and whatnot.
More concretely, that exercise in Bishop’s book says: a Dedekind cut is a pair of nonempty sets of rationals S,T such that we always have s<t and given rationals x<y either x is in S or y is in T. Unless I’m confused about Bishop’s account of sets, all of this is consistent with e.g. S containing the negative rationals and T the positive rationals, and not being able to say that 0 is in either of them. And unless I’m confused about your “arbitration oracles”, you can’t build an arbitration oracle out of that setup.
(But, again: not an expert on any of this, could be horribly wrong.)
Here’s how one might specify Dedekind cuts in type theory. Provide two types A,B with mappings a:A→Q, b:B→Q. To show these cover all the rationals, provide c:Q→A∨B such that the value returned by c maps back to its argument, through functions a or b. But this lets us re-construct a function Q→B by seeing whether c provides an A or a B. There are other ways of doing this but I’m not sure what else is worth analyzing.
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.