[FOM] Predicativity in CZF

[Daniel Méhkeri]

Michael Rathjen a écrit:

> One of the axioms of CST is exponentiation, that is the statement that 
> given two sets A and B, the set of all functions from A to B,  A->B, 
> forms a set. The subset collection axiom of CZF is a generalization 
> of exponentiation.

Is this a fair summary: Subset collection asserts the existence of the set of (graphs of) _intensional_ functions from A to B. By contrast, the axiom of Exponentiation asserts the existence of the set of (graphs of) _extensional_ functions from A to B. 

I have taken a cue from Andrej Bauer's post on Countable Choice: applying an intensional function to an element of A gives an element of B, but the
applications of an intensional function to two extensionally equal elements of A might not give extensionally equal elements of B. So for example reading the Choice axioms intuitionistically, we find the full axiom of Choice fails, because the antecedent only asserts an intensional function, but the consequent asserts an extensional function; Countable Choice works because natural numbers have normal forms. 

Subset Collection (via Fullness) asserts: for every A and B there is a set C containing only total relations from A to B, and such that for any total relation from A to B, there exists one in C of which it is the superset. Although we've gotten rid of the free predicate, Nik Weaver points out that every element of the full power set of the cartesian product of A and B potentially forces the existence of something in C. Of course the alleged power set doesn't exist, so the collection C is doubtful.

But "total relation from A to B" means: for every x in A there is at least one related element y in B. Reading intuitionistically, it is the superset of (the graph of) an certain intensional function from A to B. So if C were the set of intensional functions from A to B, then that would already be in C, so Fullness, therefore Subset Collection, would be validated. Of course this still depends on a function space construction, but we didn't need to assume any power sets.

Dan Mehkeri
--


      Découvrez les styles qui font sensation sur Yahoo! Québec Avatars.
http://cf.avatars.yahoo.com/