# [FOM] Choice sequences and excluded middle

Sun Jun 29 18:20:04 EDT 2003

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
> 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

`