# [FOM] Choice sequences and excluded middle

Harvey Friedman friedman at math.ohio-state.edu
Sun Jun 29 22:22:44 EDT 2003

Reply to Tait 7:12AM 6/23/03.

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

Let us consider the two sorted language with variables over natural
numbers and variables over functions from natural numbers into
natural numbers. We also have the usual +,x,0,1,<,= on the natural
numbers, and function application. Connectives, and quantifiers over
both sorts.

Let A be a sentence in this language. Many people think that
intuitionists have some notion of "free choice sequence" which the
function variables range over, and also have an intuitionistic view
of logic. That's how they wish to interpret the "meaning" of
sentences in this language. This approach is supposed to be in
consonance with the normal way of viewing the purely numeral
fragment; i.e., the language of Heyting's Arithemtic = language of
Peano Arithmetic.

But you are suggesting a different, proof theoretic view.

Of course, you don't want your view to be simply identified with:
study a certain axiom system.

I think you want to cast your view in some more profound way, that is
also attractive to the ordinary nonituionistic mathematician -
"classical mathematician" - who can make no sense of a "choice
sequence".

I don't quite see how you want to set this up as an attractive
subject for the classical mathematician. What it is about? Is it a
technical proof theoretic subject, or an attractive proof theoretic
subject for the classical mathematician? Is it a study in the
continuous functions on Baire space?

`