[FOM] Relevance of reverse mathematics to constructivity

[William Tait]

On Mar 22, 2010, at 10:25 PM, Daniel Méhkeri wrote:
> 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_.

Dear Daniel,

If you don't mind, please do fill in a bit. Specifically, if one can safely lose the witness, why isn't AC_{00} valid?

Bill Tait