FOM: Intuitionistic cuts/partitions

[Harvey Friedman]

Reply to Pratt 4:53PM 3/15/98.

Kanovei wrote 6:41PM 3/12/98:

>Indeed, a CUT (or: Dedekind cut) is a partition
>of the rationals onto two disjoint sets A and B,
>such and such ... .

Perhaps Pratt wants an intuitionistic analog to this approach that Kanovei
attributes to Dedekind. Here it is:

An intuitionistic cut is a set (Brouwer species) X such that there exists
A,B in X where

	i) A,B are disjoint sets of rationals, each of which 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;
	v) for all C in X, C = A or C = B.

We define X < Y if and only if there exists A,B in X and C,D in Y with the
above properties, where B and C meet. Again, one proves intuitionistically
that this is isomorphic to the the pair of cuts approach and to the Cauchy
sequence approach.

Here is what Pratt wrote:

>After removing the above degeneracy as Kanovei suggested, I tried
>and failed to find a Horn sentence defining a cut.  But even after
>putting the degeneracy back, your definition of cut is still not a Horn
>sentence, witness the disjunction in (iv).  But this disjunction is in
>intuitionistic logic weaker than classical disjunction, given that the
>latter insists on excluding the middle.  My question is whether this is
>a strict weakening in this case.  For example if with this definition
>of cut one could not prove the existence of discontinuous functions then
>it would certainly be weaker, as discontinuous functions obviously exist
>with the classical definition of cut.

With this definition of cut, it is well known that one cannot prove,
intuitionistically, the existence of discontinuous functions from R into R,
and that one can even consistently add that all functions from R to R are
continuous, and even stronger statements.