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 and 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.