[FOM] Relevance of reverse mathematics to constructivity

[William Tait]

On Mar 21, 2010, at 11:00 AM, Carl Mummert wrote:
> For example, consider the choice scheme AC_{00} which says: if one has
> a definable relation R on the natural numbers such that for every n
> there exists an m with R(n,m), then there is a function f from the set
> of natural numbers to itself such that R(n,f(n)) holds for all n. This
> principle is accepted in Bishop-style constructive mathematics, but it
> is not valid in constructive set theory.  Each of these has some claim
> to the term "constructive mathematics". The issue whether choice
> principles such as AC_{00} are truly "constructive" seems to depend on
> which framework for constructive mathematics is employed.

This is a little misleading. From a constructive point of view, the natural numbers built up from 0 by iterating the successor operation form a different object from the natural numbers understood as the finite von Neumann ordinals.  In the latter case, the problem with choice is that  a proof of 
forall x in N exists y in N P(x,y) 
yields only an operation F  which applied to a set x _and a proof p that s is a finite von Neumann ordinal_  yields a y=F(x, p) in N such that P(x,y).  AC_{00} as you formulate it looses the parameter p.  

I expect that you were aware of this. But what I want to point out is that your example is not an example of a difference in conception of what is constructive. I venture the opinion that all constructivists would agree that  AC_{00} is constructive when N is taken in the primitive sense and that it is not when it is taken to be the set of finite von Neumann ordinals.

Best wishes,
Bill Tait