[FOM] Choice sequences and excluded middle

[Giuseppina Ronzitti]

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

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

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

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

As an easy consequence of the (simple) Continuity Principle (CP) one can
prove as a theorem the absurdity of the Principle of Excluded Third.
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. Moreover, the notions of "spread" and "choice
sequence" (or even better "infinitely proceeding sequence") are
intuitionistically meaningful only if intuitionistically understood by
allowing continuity principles as principles of mathematical reasoning.
Thus it does not seem to be right the assertion that "the appearance of a
refutation hangs on the use of non-standard notation, a usage equally
available in non-constructive mathematics" as this usage is not properly
equally available in non-contructive mathematics.

Another immediate consequence of the Continuity Principle (CP) is the
continuity of the real functions. Functions defined on spreads are, in this
sense, necessarily continuous.

Giusi Ronzitti,
Genova.