Re: Choice sequences, intuition, etc

Bill Taylor says...

OK, I think I've got it. A free choice sequence is "merely"
a sequence for which the first k terms are known, for any k,
but for which any question essentially involving infinitely
many members, has no knowable answer.

I think that's right.

Bishop describes... ...one such doubt is about
the rule of ex falso quodlibet, false->X for any X.

I heartily agree! Constructivists should avoid this like
the plague, IMHO, as I cannot see what earthy algorithmic
meaning could be given to it, in any particular case.
Can anyone else? I would love to hear, if so.

If you *define* FALSE to be the second-order statement
"forall propositions X, X" (in other words, all statements
are true), then FALSE -> X is constructively provable.

EXACTLY SO! And as we seem to be agreed that Bishop considered
that mathematical meaning amounted to computational meaning,
this seems to suggest that he found NO MEANING to Choice Sequences.

I think that that's not a completely accurate description of
Bishop's philosophy. Constructive tasks almost always take
the form of "Given this, construct that". Bishop insisted that
what is *constructed* must be computationally meaningful, but
he carefully refrained from making the assumption that what is
*given* must be constructable. So when Bishop proves that
"forall reals r, such and such and such follows" he is *not*
assuming that the real r is constructable. He is assuming that
it has computational content, but not that it be constructable.
To have computational content, a real r must have an associated
method for providing a rational number that is within 1/n of r,
for every natural number n, but Bishop nowhere assumes that
this method must be a computable function. In this way, Bishop's
theorems are always classically valid (which would not be the
case if he assumed something along the lines of "all reals are
computable").

So Bishop's methods allow one to define *constructive* functions
on potentially nonconstructive objects.

--
Daryl McCullough
Ithaca, NY

.

Relevant Pages

  • Re: Choice sequences, intuition, etc
    ... before setting out on the actual math. ... meaning could be given to it, ... but I think modern constructivists like Bridges do. ... of an algorithm for turning an algorithm for p into ...
    (sci.logic)
  • Re: A quote (and question) about intuitionism
    ... |Is that a definition of truth? ... then, according to the meaning, the statement is sometimes ... So for me the evidence I have for FLT is ... If I understand correctly, constructivists, roughly speaking, ...
    (sci.math)
  • Re: A quote (and question) about intuitionism
    ... |Is that a definition of truth? ... then, according to the meaning, the statement is sometimes ... considered appropriate by a lot of constructivists, ... fact that we have ways of discovering facts about the past. ...
    (sci.math)
  • Re: A quote (and question) about intuitionism
    ... To constructivists, ... what problem they have with the meaning of "there exists". ... obediently taking Bourbaki's formalistic philosophy absolutely ... How does this differ, ...
    (sci.math)
  • Re: On Well-Ordering(s) and Sets Dense in the Reals, Infinity
    ... >> except equipollent may have a different meaning than that there ... > sequence of application of derivation rules; ... > ordering is a well-ordering? ... "uncountability of the reals", or rather, I do. ...
    (sci.math)