[FOM] Relevance of reverse mathematics to constructivity
Daniel Méhkeri
dmehkeri at yahoo.ca
Mon Mar 22 23:25:35 EDT 2010
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/
More information about the FOM
mailing list