FOM: Intuitionistic cuts

[Harvey Friedman]

Pratt 10:02AM 3/14/98 writes:

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

Yes. An intuitionistically correct cut-based formulation is given as
follows. We have two sets A,B of rational numbers, such that

	i) A,B are disjoint and each have an element;
	ii) (x in A & y < x) implies y in A;
	iii) (x in B & y > x) implies y in B;
	iv) if x < y then x in A or y in B.

Here x,y are rationals, and A,B are sets in the sense of Brouwer's theory
of species. And we define (A,B) < (C,D) if and only if B,C meet. One
proves, e.g., that this ordering is isomorphic to the (quasi) ordering of
Cauchy sequences with prescribed rate of convergence.