[FOM] Choice sequences and excluded middle

[William Tait]

The following is an excerpt from the introduction to a collection of 
essays of mine that I am preparing. It was originally prepared for the 
LaTeX typesetter: I have doctored it a bit so that it should be 
readable without knowledge of LaTeX commands.

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).) 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$.  A formula  $A(\alpha)$ is 
understood, on the usual semantics of predicate logic, to be a 
propositional function which assigns to each value $\alpha*$ of 
$\alpha$ a  proposition $A(\alpha*)$. But, since the only values 
$\alpha*$ there are are (real) functions,  the meaning of the open 
formula $A(\alpha)$ should be the same as that of $A(f)$, where $f$ 
ranges over $N^N$; and so the meaning of $\forall \alpha A(\alpha)$  
should be the same as that of  $\forall f A(f)$. But that is not what 
is intended by intuitionists: the ordinary conception of the 
quantifiers is not working here. For example, if $A(x) = \exists y 
B(x,y)$, then $\forall f A(f)$ certainly carries the meaning that there 
is a function $G$ such that $\forall f B(f, G(f))$: that just follows 
from the general (constructive) meaning of $\forall$ and $\exists$. But 
it  by no means implies that $G$ is a continuous function of $f$. (In 
this discussion, the topology of $N^N$ is the usual Baire space 
topology and the topology of the integers is the discrete topology. We 
don't need to discuss the topology of the other types that may be 
involved.) But, in contrast,  $\forall \alpha A(\alpha)$ is intended to 
carry the meaning that there is a continuous function $G$ such that  
$\forall \alpha B(\alpha, G(\alpha))$.

In fact, the entire role of  choice sequence variables is just this: 
let  $x$ and $\alpha$ be sequences of ordinary variables and choice 
sequence variables, respectively.

1. Given an open formula $A(y)  = B(x, \alpha, y)$ (with all the free 
variables displayed), then a proof of $\exists y A(y)$ as a function of 
these variables is to be a pair $p(x, \alpha) = (G(x, \alpha), q(x, 
\alpha))$, where $ q(x, \alpha)$ is a proof of $A(G(x, \alpha))$ and 
$p$ (and so, in particular, $G$) is continuous in $\alpha$.

2. Given a formula $A = B(x, \alpha) or C(x, \alpha)$ (with all the 
free variables displayed), then a proof of $A$ as a function of these 
variables is a pair $p(x, \alpha) = (G(x, \alpha), q(x, \alpha))$ which 
is continuous in the variables $\alpha$, where $G$ is $\{0, 1\}$-valued 
and,  for any given values of the variables, if $G(x, \alpha) =0$, then 
$q(x, \alpha)$ is a proof of $B(x, \alpha)$ and, if $G(x, \alpha) = 1$, 
then $q(x, \alpha)$ is a proof of $C(x, \alpha)$.

  In other words,  choice sequence variables are not of a distinct new 
type of variable in the usual sense. They are used, rather than the 
variables $f$ over (real) sequences, simply as a syntactical devise to 
indicate to which variables  the continuity requirement is to apply in 
forming proofs of disjoint unions (i.e.disjunctions or existential 
quantifications).

The particular example of Troelstra and van Dalen, cited above, is the 
formula $A(\alpha) = \forall n [\alpha(n) = 0] or not \forall n[ 
\alpha(n) = 0].$ The authors in effect point out  that, with the above 
convention regarding the notation $\alpha$, $\forall \alpha A(\alpha)$ 
is refutable. Indeed the constant function $\alpha* = 0$, provides a 
counterexample:  there is no {0, 1}-valued function $G$ continuous at 
$\alpha*$ such that $G(\alpha) = 0 \iff \forall n \alpha(n) = 0$. But I 
would be reluctant to call this a refutation of the  principle $\forall 
x [B(x) or not B(x)]$ as normally understood.  One obtains the 
appearance of a counterexample only by introducing non-standard 
notation. But, more to the point, the convention by means of which the 
apparent counterexample is created, namely the convention concerning 
the use of choice sequence variables, is equally available to classical 
mathematics: there is nothing special in the conception of constructive 
mathematics which admits  this `counterexample'.

Bill Tait