FOM: Re: Intuitionistic cuts

[Vaughan Pratt]

Pratt:
>This definition has the same defect...
>How significant this defect is is beside the point...

Friedman:
>This definition has no defect in the normal sense of the word; nor does the
>usual classical treatment of the classical real line in terms of Dedekind
>cuts.

Fine, call it something other than a defect then, a degeneracy say.
Kanovei made the point, which I for one liked very much, that there
is another formulation of cut where the degeneracy I was complaining
about, trivial or not, can be removed satisfactorily, and I was agreeing
with him.  I then asked some questions about the situation resulting
from removing that degeneracy.

What you're proposing puts that degeneracy back and is therefore
irrelevant to this thread.

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

Friedman:
>I don't understand this question at all. Please explain. Perhaps I can then
>supply an impossibility theorem.

(As a caveat I should say that I'm not on my turf here and am likely
to be making some elementary errors, which I'd be very grateful to
have corrected.)

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.

Vaughan Pratt