An effective Cauchy sequence converging to a real r induces recursive enumerators for {q∈Q∣q<r} and {q∈Q∣q>r}, because if q>r, then q>r+ε for some ε>0, so you eventually learn this.
The constructive meaning of a set is that that membership should be decidable, not just semi-decidable.
If r is irrational, then {q∈Q∣q<r} and {q∈Q∣q>r} are complements, and each semi-decidable, so they are decidable. If r is rational, then the complement of {q∈Q∣q<r} is {r}⊔{q∈Q∣q>r}, 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 {q∈Q∣q<r} and {q∈Q∣q>r} 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 True:Σ and Maybe:Σ→Σ subject to the quotient relation Maybe(x)=x, which leads to two values, True and False:=Maybe(False).
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 not function on the Sierpinski type is taboo, and would imply that the Sierpinski type is isomorphic to booleans.
My take-away from this:
An effective Cauchy sequence converging to a real r induces recursive enumerators for {q∈Q∣q<r} and {q∈Q∣q>r}, because if q>r, then q>r+ε for some ε>0, so you eventually learn this.
The constructive meaning of a set is that that membership should be decidable, not just semi-decidable.
If r is irrational, then {q∈Q∣q<r} and {q∈Q∣q>r} are complements, and each semi-decidable, so they are decidable. If r is rational, then the complement of {q∈Q∣q<r} is {r}⊔{q∈Q∣q>r}, 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 {q∈Q∣q<r} and {q∈Q∣q>r} from recursive enumerators of them.
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 True:Σ and Maybe:Σ→Σ subject to the quotient relation Maybe(x)=x, which leads to two values, True and False:=Maybe(False).
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 not function on the Sierpinski type is taboo, and would imply that the Sierpinski type is isomorphic to booleans.