[FOM] Choice sequences and excluded middle

[Giuseppina Ronzitti]

William Tait wrote:

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

Thanks for the remark.

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

The "belief" persists at least up 2000. See "Understanding and using
Brouwer's continuity principle", by W. Veldman, theorem 3.1. And also
"Elements of Intuitionism", second edition (revised) M. Dummett, Theorem 3.6,
p. 61.

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

What I meant was (1) that the notion of "spread" was introduced by Brouwer in
order to speak about sets like the continuum; (2) that the universal spread
$N^N$ is the set of "all possible infinite sequences of natural numbers",
taken as always proceedings (onbepaald voort te zetten reeksen); (3)  that
this cannot be the set of all sequence of a certain kind, as  expressions
like  "the set of all all lawlike (or lawless) sequences" are not considered
as meaningful totalities. Brouwer's notion of sequence, it seems to me,
cannot be reduced to some more primitive notion of a privileged kind of
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.

I am sorry, but I do not see that I am reintroducing obscurities. But it's
very well possible that I don't catch your point either. So, I'll think about
it.

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

I meant nothing about what is going on in my head (if anything at all). I do
not mean that I am an intuitionist. I just try to understand intuitionists
ways. What I meant was that CP is not an axiom in classical mathematics.

Best regards,
Giusi