I’ve learned some more constructive math since my previous comments, so I thought I should correct myself a bit:
In Coq, the type of truth values is called Prop. In other foundations, it might be encoded differently, including by encoding functions into truth-values as functions out of an arbitrary type.
You would generally not interpret functions into Prop as functions out of an arbitrary type. In predicative foundations, this is the only way to really specify subtypes, but the entire point of predicativity is that you can’t really work with the type of all subtypes, so this doesn’t really work for the real numbers.
For some reason, the standard way people tend to construct the Dedekind reals in predicative systems is to pick some type universe U and define propositions PropU to be the subsingletons of U. Then you can do most things you want to do with it, but the real numbers will not be a member of U for size reasons, and therefore the cuts cannot mention real numbers in their definition, only rational numbers.
I say “for some reason” because I feel like there is a perfectly cromulent alternative: Use the Sierpinski type . This is especially good if you can axiomatize to have lots of nice structure. But I guess people usually don’t use and usually don’t axiomatize enough goodness into it when they do.
Cauchy sequences you’d usually not just use CSRs but also Cauchy sequences of CSRs (and so on, recursively).
This is what the HoTT book does because they don’t want to assume countable choice, and without countable choice, CSRs quotiented by converging to the same point are not necessarily Cauchy-complete.
However, if you are being constructive because you want to be computable, then you can still assume countable choice, so this is not a problem.
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.
You can show that every Dedekind cut corresponds to a Cauchy sequence using countable choice rather than excluded middle. The binary search argument shows that for any N, there exists a rational number xN within range 1/N of the Dedekind cut. You need countable choice to assemble these into a sequence and thereby have a Cauchy sequence.
The counterexample is the sheaf topos where every object is a continuous function from . This topos doesn’t satisfy countable choice, and internally the Cauchy reals are locally-constant functions to the meta reals (locally-constant because is discrete), while the Dedekind reals are continuous functions to the meta reals.
Not sure I understand; how would you go from my pathological case ( approximating as a CSR) to a Dedekind cut? (Assuming you still endorse “every Cauchy sequence corresponds to a Dedekind cut”)
For a CSR , define , and define . (Formally, we might regard .) What we need to show is that and are downwards/upwards-closed (trivial), open (also trivial), inhabited (also trivial), disjoint (also trivial) and located, i.e. . (Locatedness is an epsilon-weakening of ; for proof, take and .)
To show that is located, evaluate at an that gives a precision of . All later values will fall in . Now pick and case-split on compared to :
Ah, okay. So we construct two propositions, for upper and lower. It’s not always the case that at least one is inhabited (as could converge to ). It’s more like both are verifiable, in that if is strictly less than the limit of , then is inhabited. This is in line with constructive topology; we think of propositions as analogous to open sets.
I’ve been thinking about effective topology recently in the form of the category of sets (r.e. axiomatizable subsets of Cantor space) and computable maps between them, and the ex / reg completion, which has as objects quotients of sets by equivalence relations (these are all compact Hausdorff, e.g. including the interval [0, 1]). It seems quotients are the main thing that makes the reals difficult; and topological quotients might relate to constructive “basic opens are verifiable” principles.
This is in line with constructive topology; we think of propositions as analogous to open sets.
The propositions in this case are open sets, but propositions in general can be whatever they want. Unless one uses . Though even for , -propositions can be non-open (they’re only required to be recursively enumerable). The openness of the cuts is one of the defining conditions.
I’ve been thinking about effective topology recently in the form of the category of sets (r.e. axiomatizable subsets of Cantor space) and computable maps between them, and the ex / reg completion, which has as objects quotients of sets by equivalence relations (these are all compact Hausdorff, e.g. including the interval [0, 1]). It seems quotients are the main thing that makes the reals difficult; and topological quotients might relate to constructive “basic opens are verifiable” principles.
Unfortunately I don’t really have any intuition for this. 😅 I have been thinking a bit about -PERs with various levels of quantifier complexity, though, but my intuition is mostly for and sets.
I’ve learned some more constructive math since my previous comments, so I thought I should correct myself a bit:
You would generally not interpret functions into Prop as functions out of an arbitrary type. In predicative foundations, this is the only way to really specify subtypes, but the entire point of predicativity is that you can’t really work with the type of all subtypes, so this doesn’t really work for the real numbers.
For some reason, the standard way people tend to construct the Dedekind reals in predicative systems is to pick some type universe U and define propositions PropU to be the subsingletons of U. Then you can do most things you want to do with it, but the real numbers will not be a member of U for size reasons, and therefore the cuts cannot mention real numbers in their definition, only rational numbers.
I say “for some reason” because I feel like there is a perfectly cromulent alternative: Use the Sierpinski type
This is what the HoTT book does because they don’t want to assume countable choice, and without countable choice, CSRs quotiented by converging to the same point are not necessarily Cauchy-complete.
However, if you are being constructive because you want to be computable, then you can still assume countable choice, so this is not a problem.
You can show that every Dedekind cut corresponds to a Cauchy sequence using countable choice rather than excluded middle. The binary search argument shows that for any N, there exists a rational number xN within range 1/N of the Dedekind cut. You need countable choice to assemble these into a sequence and thereby have a Cauchy sequence.
The counterexample is the sheaf topos
See also What is the computational content of the axiom of choice? for more on countable choice.
Not sure I understand; how would you go from my pathological case (
For a CSR
To show that
If
If
Ah, okay. So we construct two propositions, for upper and lower. It’s not always the case that at least one is inhabited (as
I’ve been thinking about effective topology recently in the form of the category of
The propositions in this case are open sets, but propositions in general can be whatever they want. Unless one uses
Unfortunately I don’t really have any intuition for this. 😅 I have been thinking a bit about