FOM: Intuitionistic cuts

Harvey Friedman friedman at
Sat Mar 14 10:26:31 EST 1998

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.

More information about the FOM mailing list