FOM: Re: Intuitionistic cuts

[Harvey Friedman]

Reply to Pratt 5:55PM 3/14/98

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

Pratt writes:

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

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. As I have said several times on the f.o.m., these constructions prove
the existence of particular structures satisfying desired condtitions.
Then, as a basic matter of first order predicate logic, one merely
introduces a constant symbol(s) with the axiom that it represents a
structure with the desired properties. Then one uses that constant
symbol(s) in the normal way. The fact that there is no one construction of
a specific structure obeying the desired conditions that everybody will
endorse is of no special significance.

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

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