Review
My take-away from this:
An effective Cauchy sequence converging to a real induces recursive enumerators for and , because if , then for some , so you eventually learn this.
The constructive meaning of a set is that that membership should be decidable, not just semi-decidable.
If is irrational, then and are complements, and each semi-decidable, so they are decidable. If is rational, then the complement of is , which is semi-decidable, so again these sets are decidable. So, from the point of view of classical logic, it's not only true that Cauchy sequences and Dedekind cuts are equivalent, but also effective Cauchy sequences and effective Dedekind cuts are equivalent.
However, it is not decidable whether a given Cauchy-sequence real is rational or not, and if so, which rational it is. So this doesn't give a way to construct decision algorithms for the sets and from recursive enumerators of them.
The constructive meaning of a set is that that membership should be decidable, not just semi-decidable.
You can encode semidecidable sets constructively as functions into , where is the Sierpinski type.
The Sierpinski type can be encoded various ways, e.g. coinductively by generators and subject to the quotient relation , which leads to two values, and .
The Sierpinski type is closed under countable disjunctions and finite conjunctions, and therefore functions into it are closed under countable unions and finite intersections. In classical math, excluded middle implies that the Sierpinski type, the booleans, and the truth values are all isomorphic, but in constructive math these equivalences are taboo. In particular, the function on the Sierpinski type is taboo, and would imply that the Sierpinski type is isomorphic to booleans.
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 , . To show these cover all the rationals, provide such that the value returned by c maps back to its argument, through functions or . But this lets us re-construct a function by seeing whether 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:
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.
I guess to clean it up even further:
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 , then I think that's true, but if you just have (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.
I claim Dedekind cuts should be defined in a less hardcoded manner. Galaxy brain meme:
I claim Cauchy sequences should be defined in a less hardcoded manner, too: A sequence is Cauchy (e.g. in (Q,Euclidean distance)) iff it converges in some (wlog one-element) extension of the space.
Not sure this works constructively. x < y or x = y or x > y is valid for the constructive rationals, but taboo for the constructive reals. Wouldn't this make it taboo for the real order to be an elementary extension of the rational order? Not familiar with constructive model theory so not entirely sure.
It seems that a real number defined this way will have some perhaps-infinite list of rationals it's less than and one it's greater than. You might want to add a constraint that the maximum of the list of numbers it's above gets arbitrarily close to the minimum of the list of numbers it's below (as Tailcalled suggested).
With respect to Cauchy sequences, the issue is how to specify convergence; the epsilon/N definition is one way to do this and, constructively, gives a way of computing epsilon-good approximations.
Oh, I misunderstood the point of your first paragraph. What if we require an enumeration of all rationals our number is greater than?
With just that you could get upper bounds for the real. You could get some lower bounds by showing all rationals in the enumeration are greater than some rational, but this isn't always possible to do, so maybe your type includes things that aren't real numbers with provable lower bounds.
If you require both then we're back at the situation where, if there's a constructive proof that the enumerations min/max to the same value, you can get a Cauchy real out of this, and perhaps these are equivalent.
perhaps these are equivalent.
They are. To get enumerations of rationals above and below out of an effective Cauchy sequence, once the Cauchy sequence outputs a rational such that everything afterwards can only differ by at most , you start enumerating rationals below as below the real and rationals above as above the real. If the Cauchy sequence converges to , and you have a rational , then once the Cauchy sequence gets to the point where everything after is gauranteed to differ by at most , you can enumerate as less than .
Chaitin's constant, right. I should have taken my own advice and said "an enumeration of all properties of our number that can be written in the first-order logic (Q,<)".
This means that, in particular, if your real happens to be rational, you can produce the fact that it is equal to some particular rational number. Neither Cauchy reals nor Dedekind reals have this property.
Sure! Fortunately, while you can use this to prove any rational real innocent of being irrational, you can't use this to prove any irrational real guilty of being irrational, since every first-order formula can only check against finitely many constants.
Something that I think it unsatisfying about this is that the rationals aren't previleged as a countable dense subset of the reals; it just happens to be a convenient one. The completions of the diadic rationals, the rationals, and the algebraic real numbers are all the same. But if you require that an element of the completion, if equal to an element of the countable set being completed, must eventually certify this equality, then the completions of the diadic rationals, rationals, and algebraic reals are all constructively inequivalent.
Hmmmm. What if I said "an enumeration of the first-order theory of (union(Q,{our number}),<)"? Then any number can claim to be equal to one of the constants.
If you want to transfer definitions into another context (constructive, in this case), you should treat such concrete, intuitive properties as theorems, not axioms, because the abstract formulation will generalize further. (remark: "close" is about distances, not order.)
If constructivism adds a degree of freedom in the definition of convergence, I'd try to use it to rescue the theorem that the Dedekindorder and Cauchydistance structures on ℚ agree about the completion. Potential rewards include survival of the theory built on top and evidence about the ideal definition of convergence. (I bet it's not epsilon/N, because why would a natural property of maps from ℕ to ℚ introduce the variable of type ℚ before the variable of type ℕ?)
Where B is the Boolean type.
Usually in defining Dedekind cuts, you'd use truth values rather than booleans for the codomain of indicator functions.
There's a ton of other nuances to real numbers in constructive math. For instance, Dedekind cuts defined by their lower bound, their upper bound, or both bounds are inequivalent (with both bounds being more appropriate in general, but lower bounds being useful sometimes in measure theory IIRC), and for Cauchy sequences you'd usually not just use CSRs but also Cauchy sequences of CSRs (and so on, recursively).
For a complete construction of the real numbers in constructive foundations, I recommend the Homotopy Type Theory book.
Showing that not every constructive Cauchy sequence corresponds to a constructive Dedekind cut
When constructed more carefully, every Cauchy sequence corresponds to a Dedekind cut, but it requires something stronger (such as excluded middle) to show that every Dedekind cut corresponds to a Cauchy sequence.
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.
Classically, a Cauchy sequence is a sequence of reals , such that for any , there is a natural such that for any , . 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 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 as the approximation. We are assured that this approximation must be within of any future in the sequence; therefore, the approximation error (that is, ) will not exceed .
A Dedekind cut, on the other hand, is a partition of the rationals into two sets such that:
It represents the real number . As with Cauchy sequences, we can approximate this number to within some arbitrary ; we do this by doing a binary search to find rationals with , at which point approximates to within . (Note that we need to find rational bounds on before commencing a straightforward binary search, but this is possible by listing the integers sorted by absolute value until finding at least one in and one in .)
Translating a Dedekind cut to a CSR is straightforward. We set the terms of the sequence to be successive binary search approximations of , 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 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 for which there exists some rational and some natural N, such that for every n > N, . (In particular, we set some , 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.
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:
Generally, type theories are computable, so and will be computable functions.
What about Dedekind cuts? This consists of a quadruple of values
Where is the Boolean type. corresponds to the set of rationals for which is true. The triple must satisfy:
specifies the sets and ; and show that and are non-empty; maps an element of to a greater element of . The conditions straightforwardly translate the classical definition to a constructive one.
Let’s first consider translating Dedekind cuts to CSRs. We can use and 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 .
The other way around is not possible in general.
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 be a Turing machine that does not necessarily halt, but returns a Boolean if it does halt. Let be equal to 0 if doesn’t halt; if halts in exactly steps returning a boolean , then, if is true, , and if is false, then .
We will first try representing as a function from Turing machines to CSRs. We will define to be a CSR for . This is a simple approximation; to find , we run for steps. If has halted by then, we know and can set . Otherwise, we set the approximation
This sequence is (constructively) Cauchy since all terms past are within of each other. This makes a valid for the Cauchy sequence computable (we simply need ).
On the other hand, cannot be represented as a function returning a Dedekind cut. Suppose represents the set for the Dedekind cut of . We will specify to be an arbitration oracle, by setting . This is an arbitration oracle by cases:
Since arbitration oracles are uncomputable, this shows that it isn’t possible to represent as a computable function returning a Dedekind cut.
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.