FOM: Intuitionistic cuts

[Vaughan Pratt]

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

This definition has the same defect that I pointed out in Dedekind's
original definition, with your sets A and B in place of Dedekind's A1
and A2.  In both Dedekind's and your versions of the statement the defect
is that an equally good definition results from interchanging A and B.
This is the same situation as when only A features in the definition.

How significant this defect is is beside the point, the context was
that Kanovei (correctly) pointed out that defining a cut as a partition
(understood as an equivalence relation) removed this defect, but
incorrectly attributed the idea to Dedekind, who did not define a
cut as a partition in this sense and whose definition has the same
problem that Kanovei fixed with his definition (when carefully defined,
my contribution).

As to (iv) being intuitionistic, excluded middle presumably makes (iv)
a weaker condition that with classical logic, yes?  (Not doubting,
just checking.)  What I'd originally hoped for was an intuitionistic
definition with the same strength, but I imagine that's impossible.

Vaughan