Are there any examples of mathematical theories T1,T2 which satisfy the following conditions?
T1 and T2 have the same "vocabulary" and are both formalized in the classical first order predicate calculus (with identity).
T1 is a sub-theory of T2.
There is available a precise criterion for determining whether any defining formula in the language of either of these theories is "predicative" or "impredicative".
All the defining formulae of T1 are "predicative".
At least one defining formula of T2 is "impredicative".
T1 has not been proved inconsistent, but it can be proved that if T1 is consistent-then so is T2.
Most mathematicians, I think, feel that so-called "impredicative" definitions are very useful and do not---by themselves---necessarily lead to inconsistencies. However the majority of the arguments supporting this viewpoint appear to be informal, philosophical or even "ad hoc". I am wondering if it has been (or could be) supported mathematically by the kind of result I have outlined above.