[FOM] Relevance of reverse mathematics to constructivity
William Tait
williamtait at mac.com
Sun Mar 21 17:32:34 EDT 2010
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
More information about the FOM
mailing list