[FOM] Choice sequences and excluded middle

Mon Jun 23 08:12:48 EDT 2003

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
`