🚀 go-pugleaf

In article <Bx2ALr.3Az@cantua.canterbury.ac.nz> wft@math.canterbury.ac.nz (Bill Taylor) writes:
>For instance, defining x as "the solution of x = exp(-x)", or as "the largest
>solution of x^5 - 8x^4 + 1 = 0",  are impredicative in this sense.  I do not
>refer to the use of the letter "x" of course, (which I have treated sloppily
>as a constant and a bound variable alternately), but the number itself, which
>has been defined only by implicitly referring to a set of numbers of which
>it may be a member.      This form of impredicativity is merely using a
>definition to *pick out* some particular thing which we know *already exists*,
>as Menzel observes; and seems thoroughly harmless.
>
>Similarly for that favourite example of impredicativity so suspicious to
>constructivists: the least upper bound of a set of reals.   The usual
>definition would be by a Dedekind cut; that of the set of rationals that are
>no greater than some real in the given set. This is thought to be dangerously
>impredicative by some, in that to check for a rational to be in the set, one
>must test it against all possible reals, and this may include the very real
>that one is trying to define. I have never seen the force of this objection,
>which seems to me no more sensible than for the equation-root examples above.
>I consider that Menzel's "picking out" remarks fully apply to this, and
>easily dispose of any objections.
Can't we just construct the reals using Cauchy sequences of rationals rather
than Dedekind cuts?  If we do this, we can actually construct the series
solution to x = exp(-x) or the largest solution of any polynomial we wish.
Perhaps the really interesting example of impredicativity here is when we
form (necessarily uncountable) quotient sets.

I read someplace (perhaps Johnstone's book on Topos Theory) that all of 
(intuitionistic) set theory can be developed in the (purely equational) 
theory of toposes, and that this requires no leap of existentialist faith 
as large as the existence of equivalence classes.

					Peace,
					Bill White