[FOM] Request for references on Predicativity.

[giovanni sambin]

>Is there any other relevant literature that I ought to be aware of?
>
>Please advise,
>
>Steve Newberry

Per Martin-Loef's Intuitionistic Type Theory is a predicative 
foundation of mathematics.
Impredicativity is blocked simply because the power of a set is not a 
set, and a quantification then does not produce a proposition, that 
is a new entity.
It has been used in practice as the ground theory on which to develop 
mathematics, topology in particular, actually a pointfree approach to 
topology called formal topology.
I have myself contributed recently also with a new fully predicative 
theory which underlies topology, called the basic picture.
For more information, see http://www.math.unipd.it/~logic

Giovanni Sambin

*******
Giovanni Sambin
Professor of Mathematical Logic
Dipartimento di Matematica Pura e Applicata,
Universita' di Padova
Via Belzoni 7
35131 Padova (Italy)
tel. +39-049-8275987