FOM: Dedekind --- The ultimate definition of cut? Erratum

[Vaughan Pratt]

From: Vaughan Pratt <pratt at CS.Stanford.EDU>
>We can then define a real (or at least a cut) as follows.
>
>	***********************************************
>	* A real is a PER on the rationals consisting *
>	* of exactly two nonempty convex open blocks. *
>	***********************************************

Oh dear, I slipped up.  The undefined elements can form a contiguous block
(my embarrassingly elementary error was to generalize from the absence
of any finite number of undefined elements greater than one by dropping
"finite" without thinking).  The bound of one undefined element seems
to have to be made explicit, as in:

	***********************************************
	* A real is a PER on the rationals consisting *
	* of exactly two nonempty convex open blocks  *
	* and at most one undefined element.          *
	***********************************************

While this definition does eliminate choice between equally good
definitions, which was my main goal, I fondly imagined (though fortunately
did not claim) that it did so intuitionistically, but this was wishful
thinking.  I don't see how to state either upper bound (two and one)
as a Horn sentence.  Replacing equivalent by inequivalent only moves the
problem deeper into the basement, namely into the transitivity requirement
in the definition of PER.  One can express the limit of two blocks by
the equivalent (in this context) requirement that both blocks be infinite
(in width, not cardinality), but for whom would this be an improvement?

The upper bound of one on undefined elements would seem to get to the
heart of Brouwer's concern.  In practice we do not discover reals to
such precision, the undefined elements usually do form an interval of
nonzero width.  Narrowing the interval to zero width expresses an ideal
rather than an actuality.  In that sense classicism is idealism.

I am not sure what to make of my difficulty in expressing the bound of
two on the number of blocks intuitionistically.  Can it be done, or is
there some other intrinsic problem with the cut-based definition of the
reals that Brouwer overlooked?

Vaughan Pratt