[FOM] Choice sequences and excluded middle

[Harvey Friedman]

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 
>admits  this `counterexample'.
>

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?