FOM: Intuitionistic cuts/partitions
Harvey Friedman
friedman at math.ohio-state.edu
Sun Mar 15 11:22:46 EST 1998
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.
More information about the FOM
mailing list