[FOM] Predicativity in CZF

[Daniel Méhkeri]

Nik Weaver writes:

> The set of extensional functions from N to {0,1} seems to me just
> as impredicative as the power set of N.  Isn't that right?

I wouldn't expect so, since not all subsets of N are decidable. For
that matter, not all subsets of {{}} are decidable either. Of course if they were, then the function space construction would almost immediately give the power set. So again this reasoning is not available with classical logic.

> But now that you mention it, set induction is also impredicative
> --- with, again, predicative well-ordering being the issue.

> The justification for set induction (again, please correct me
> if I'm wrong) is that sets are thought of as being built up in
> well-ordered stages.  But that would only be enough to support
> set induction for delta_0 predicates.

I hadn't thought of Set Induction either, it seemed harmless. But I guess the devil is in the details. Maybe instead of trying to construct infinite sets by a transfinite number of stages, one can think of the set of natural numbers as simply given, and all sets as built up in a finite number of stages by applying set constructors (none of which, of course, is the power set). Full induction would be available over the natural number set and over the finite number of stages. 

Dan 
-- 



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