# [FOM] Choice sequences and excluded middle

Sun Jun 29 18:31:35 EDT 2003

```Dear Guisseppina,

Aside from my response to you on the FOM list, let me send you the
relevant part of a note I sent to Marcus van Atten, in response to an
off-list posting from him.

Incidentally, I spent March 15-April 15, 2002 in Bogliasco, just down
the coast from you, at a research institute, with my companion. (She
studies contemporary Italian literature). I kept meaning to get
addresses of logicians in Genova and go visit. I even sent an email to
or too late---I don't remember.

We then spent April 23-May 23 in another research institue in Bellagio
on Lake Como. It was hard to come home.

Bill Tait

> About free choice sequences, you are of course right that Brouwer
> called them elements of the spread. My remark was based on a memory
> which may have its source in his calling them ``onaf''. I will correct
> that. But when one writes A(alpha*), what can ``alpha*''  refer to? [I
> am distinguishing the variable ``alpha'' from the name ``alpha*'' of a
> choice sequence.]  If alpha* is not law-like, then it is onaf: i.e.
> the symbol ``alpha*'' denotes, not a single sequence, but a basic open
> set of them (which will include law-like sequences), and so does not
> pick out a lawles sequence at all.
>
>> 2. Continuity of a function defined on all choice sequences one does
>> not get
>> for free; it is a principle that needs to be argued for.
>
> I would disagree with this: it is built into his notion of a function
> on a spread in ``On the domains of definition of functions'', the
> beginning of Section 2.
>
>> The issues are
>> discussed in a paper by Dirk van Dalen and me in BSL, September 2002,
>> `Arguments for the continuity principle'.
>
> Thanks: I hadn't yet read that paper, although it was on my list. But
> I totally disagree with your argument for (open data) on p. 330. For
> example A(alpha) = (n)[alpha(n) = 0 or alpha(n) not = 0]. More
> sophisticated examples require proof by math induction. In the
> relevant sense, proofs are not finite objects. (This is a mistake
> Heyting made in his Introduction to Intuitionism in the 1950's. I
> corrected him and his response was that he only wanted me to check the
> English.)  If every proof were finite, then no well-ordering of
> unsecured sequences would have type greater than omega.
>
> Of course, I would like you to state (open data) as A(alpha*) implies
> etc. rather than as A(alpha) implies etc. Now on the basis of my
> remark above, alpha*, being onaf, is not really any particular
> sequence but rather a basic open set of them; and so of course (open
> data) holds for all sequences in that open set.
>
> I will finish your paper with Dirk; but the main thrust of my remarks
> in the introduction is, as I said, not so much concerned with Brouwer.
> When I have corrected for my mistake---and perhaps have rethought a
> little bit on the basis of your paper, I will send you the
> introduction if you like.

```