FOM: Intuitionistic cuts
pratt at cs.Stanford.EDU
Sat Mar 14 20:55:30 EST 1998
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,
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.
More information about the FOM