[FOM] Choice sequences and excluded middle

[William Tait]

On Wednesday, June 25, 2003, at 08:23  AM, Giuseppina Ronzitti wrote:

> William Tait wrote:
>
>
>>  It has often been asserted that Brouwer's theory of  choice sequences
>>  refutes the law of excluded middle in the form $\forall \alpha
>>  [A(\alpha) or not A(\alpha)]$, where $\alpha$ ranges over choice
>>  sequences.  (See, for example,  p. 209, Proposition 6.4 of
>>  Troelstra-van Dalen, _Constructivism in Mathematics: An Introduction 
>> I_,
>>  Amsterdam: North-Holland (1988).)
>
> Kleene remarks (S. C. Kleene, R. E. Vesley, "The foundations of
> intuitionistic mathematics",  usually referred to as FIM ) that no 
> formula
> of the form  $ not (A v not A)$ is provable in intuitionistic 
> analysis, if
> that is consistent, for $ not not (A v not A)$ is a propositional law. 
> But
> in general we
> must seek to prove negations of closures of substitution instances. We 
> thus
> "refute" $not (A v not A)$ by proving in intuitionistic analysis
>
> (27.17*)                                        $not \forall \alpha
> A[(\alpha) v not A(\alpha)]$
>
> ($\alpha$ is a variable for  choice sequences). Kleene says " for a 
> suitable
> $A(\alpha)$", I suppose meaning that the property A  be extensional ).

I think that what Kleene meant by " for a suitable A(\alpha)" was that 
we can look for instances of A such that 21.17* is provable. (It won't 
be the case for all A.)


> The remark is at p. 83 and the proof is in p. 84 of proposition 27.17* 
> and
> uses a form of  the continuity principle (the case for decisions).

I chose Troelstra-van Dalen raher than Kleene-Vesley only to indicate 
that the belief persisted at least even up until 1988.

>> I question this assertion and argue
>> that the appearance of a refutation hangs on the use of non-standard
>> notation, a usage equally available in non-constructive mathematics.
>
>> For simplicity, lets restrict attention to sequences in the `spread'
>> $N^N$, i.e. infinite sequences of natural numbers. The situation is 
>> the
>> same, \emph{mutatus mutandus}, for other spreads. The first thing to
>> say is that there are no literally `free' choice sequences: the only
>> infinite sequences, according to Brouwer, are law-like---in any case,
>> they are the (real) elements of $N^N$.
>
> As far as I understand, this does not seem to be right. Elements of 
> spreads
> are infinite sequences, but it is not true  that all *possible* 
> elements of
> $N^N$  are law-like (this fact could not account for $N^N$ be 
> uncountable).

You can't mean this. The diagonal argument that N^N is uncountable is 
perfectly constructive:  if n |-> f_n is a (constructive) sequence of 
(constructive) functions, then n |-> f_n(n)+1 defines a (constructive) 
function not in the sequence.

You are right that Brouwer calls choice sequences the elements of the 
spread---I should not have written that. But they are also called 
``unfinished'' {``onaf'')---at least in the case of the free choice or 
law-less ones; i.e. such a one can be given only by a finite initial 
segment (which can be continued in a law-like way) and so what is given 
does not determine a free choice (lawless) sequence.

I am taking the view that the way to understand the obscure talk about 
free choice sequences (i.e.  law-less ones)  is to see how they occur 
in constructive mathematical arguments. The only reference to them is 
by the introduction of variables (e.g. alpha) over them;  for to name 
one is either to confess that it isn't free or else it is to name a 
whole basic open set of sequences. So how do arguments involving these 
variables go? In my posting, I argued that the only thing that 
distinguishes such variables from variables over (constructive) 
functions, is the requirement of continuity that they impose on proofs 
of disjoint unions (disjunctions and existential quantifications).

> The main fact here is that Brouwerian infinite sequences and spreads 
> cannot
> be properly classically handled.

I have argued that one handles this quite well classically. Brouwer's 
theory has two components: quantification `over choice sequences' and 
the restriction to constructive proof---these are seperable. You are 
right to say

> In order to quantify over a spread one must use the so called 
> Continuity
> Principles

but I would say that the use of these principles exhausts the real 
content of talking about free choice sequences: the rest is GAS.

> As an easy consequence of the (simple) Continuity Principle (CP) one 
> can
> prove as a theorem the absurdity of the Principle of Excluded Third.

You can say this usefully only if you can explain what is wrong with my 
analysis---not by reintroducing obscurities, but by showing 
constructive mathematical arguments for which the analysis is 
inadequate. If the analysis is right, there is nothing distinctively 
constructive about this `proof of absurdity'. But, seen in this light, 
one would (or should) also hesitate to call it a proof of absurdity of 
the universal  closure of excluded middle.

> As such, the Continuity Principle (CP) is not a principle of 
> mathematical
> reasoning  in the classical sense and thus it is not available to the
> classical mathematician.

This is a statement of a creed, not an argument. It has been important 
to many intuitionists to think that they are speaking of a different 
subject from classical mathematics, rather than simply applying more 
restrictive principles of reasoning. The posting I sent, that elicited 
your response, was part of a general argument for the unity of 
(mathematical) reason.

In particular, I do not understand the distinction between a `principle 
of mathematical reasoning in the classical sense' and the constructive 
application of that principle in proofs. Do you mean that something 
special is going on in your head when you, as intuitionist, as opposed 
to a nonconstructivist, apply the principle?

Best regards,

Bill