FOM: Intuitionistic cuts/partitions

[Vaughan Pratt]

From: Friedman
>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.

Ah, excellent.  By collecting A and B as a doubleton instead of a pair
you overcome the degeneracy in Dedekind's definition (assuming the
usual reading of exists A, exists B, as exists pair A,B and not exists
set {A,B}).  In the setting of the rationals the result seems entirely
equivalent to what is achieved with a two-block PER.

The one noteworthy difference is that the PER approach avoids any
quantification over sets as done above (exists A and B).  Instead one
defines a real as a structure (Q,~) where Q is the given set of rationals
and ~ is a binary relation on Q, with all axioms being first order with
respect to that structure and no sets in sight besides the universe Q
itself, sine qua non.

It is interesting that the same two disjunctions (in (iv) and (v))
are required for the above definition of cut as for my PER-based one.
(iv) says there is at most one undefined rational (maybe an intuitionist
isn't allowed to read it that way but that's what it looks like to my
classical mind), while (v) more explicitly says there are at most two
blocks (and disjointness and nonemptiness in (i) establishes that there
are at least two).

(Excuse me if all this is well known, as I said this is not my turf and
I'm ignorant of many of the basic tricks of the intuitionism trade.  Too
much time spent with bits. :)

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

Thank you, the "even" was very helpful in getting me to think more like
an intuitionist, which I definitely have not had enough practice with.

Don't worry, I don't want to be one, just to understand how to think
like one.

I see now what is going on when Mac Lane and Moerdijk construct a special
topos to this effect: they, and you, both mean that Brouwer's "theorem"
to this effect should properly be understood as an axiom, yes?

Vaughan Pratt