Re: Cauchy completeness of Cauchy reals

[Vaughan Pratt <pratt@CS.Stanford.EDU>]

While I'm comfortable with coalgebraic presentations of the continuum, as
well as such algebraic presentations as the field P/I (P being a ring of
certain polynomials, I the ideal of P generated by 1-2x) that I mentioned
a week or so ago, I'm afraid I'm no judge of constructive approaches to
formulating Dedekind cuts.  Would a toposopher (or a constructivist of
any other stripe) view the following variants as all more or less equally
constructive, for example?

1.  Define a (closed) interval in the reals as a disjoint pair (L,R)
consisting of an order ideal L and an order filter R, both in the rationals
standardly ordered, both lacking endpoints.  Order intervals by pairwise
inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'.
Define the reals to be the maximal elements in this order.  Define an
irrational to be a real for which (L,R) partitions Q.

2.  Ditto but with the reals defined instead to be intervals for which
Q - (L U R) is a finite set.  ("Finite set" rather than just "finite" to
avoid the other meaning of "finite interval."  The order plays no role
in this definition, maximality of reals in the order being instead a
theorem.)

3.  As for 2 but with "finite" replaced by "cardinality at most 1".
The predicate "rational" is identified with the cardinality of Q - (L U R).

Vaughan