FOM: Re: Intuitionistic cuts
friedman at math.ohio-state.edu
Sat Mar 14 17:30:48 EST 1998
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.
>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.
More information about the FOM