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.
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