[FOM] Choice sequences and excluded middle

[William Tait]

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 
Sambin, asking for addresses; but his response was either not helpful. 
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.