There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers ([Predicative definition](https://mathoverflow.net/questions/36972/predicative-definition) and [Impredicativity](https://mathoverflow.net/questions/26220/impredicativity))


Still I must confess I do not understand the concept well enough. All I've seen is a verbal explanation with a bunch of very clear examples. And being used to mathematics, I feel uncertain about it until I will have some formally defined entity, preferably some mathematical model of its behavior.


For example, I don't know whether there is a definition of predicativity which is sufficiently formal so that given a formula in any language whatsoever one would be able to tell whether it is predicative or not. I don't even know whether it makes sense to speak about predicativity of a **formula** since I've only seen discussions of (im)predicative **definitions**.


Seemingly predicativism must be closely related to constructivism, and again I could not find descriptions of precise relationship between these two. One of the things confusing me here is that e. g. in a programming language one might have perfectly correct self-referential construction of a datatype, so this seemingly will produce an example of a constructive impredicative definition.


Also I have vague feeling that predicativity must be somehow related to induction, in particular that any inductive definition must be predicative. Does this make sense and if yes is it correct? What about coinduction, is it related?



> 
> So to summarize, are there texts addressing these and similar questions from purely mathematical viewpoint? In particular, texts with systematic purely formal treatment of (im)predicativity? Ideal would be some mathematical (say, algebraic) structure which models behaviour of predicative vs. impredicative whatevers.
> 
> 
> 


And let me add that although I've tagged this as reference request, I would be also grateful for on-the-spot explanations without any references.



Formal/rigorous treatment of (im)predicativity/predicativism
**Solomon Feferman's papers provide formal systems for predicativity**, most recently [here](http://math.stanford.edu/~feferman/papers/pfa%281%29.pdf). Other papers on his website and in his book *In the Light of Logic* have other expositions. These systems are predicative either by virtue of their ordinal analysis, or by virtue of being conservative over PA.


**The subtypes** $\{x\in T:\phi\}$ in these systems are the focal points for predicative restrictions. Either you can not form subtypes using $\phi$'s which quantify over types, or you can form those subtypes but don't have the axioms to prove much about them.


**For examples**, see the development of analysis in the cited paper. It proves the least upper bound principle for sequences of real numbers, but not for sets. The resulting development may be your best source for intuitions about predicativity which are backed up by a formal system.


