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