[FOM] Relevance of reverse mathematics to constructivity

[Daniel Méhkeri]

William Tait wrote:

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

I think many constructivists will not agree.

The distinction between the primitive N and the set-theoretic ordinal 
omega isn't very relevant under many interpretations of constructive 
set theory, including the standard type-theoretic interpretation of CZF 
due to Aczel, under which Dependent Choices is also a theorem.

My one-line explanation would be that for any member of set-theoretic omega, there is a "canonical witness" that it is a member, so the witness can be safely "lost". I can make this more precise, or I can refer to Aczel: _The type-theoretic interpretation of constructive set theory: choice principles_.

Regards,
Daniel

-- 




      Offrez un compte Flickr Pro à vos amis et à votre famille.
http://www.flickr.com/gift/