Are there any examples of mathematical theories T1,T2 which satisfy the following conditions?

1. T1 and T2 have the same "vocabulary" and are both formalized in the classical first order predicate calculus (with identity).

2. T1 is a sub-theory of T2.

3. There is available a precise criterion for determining whether any defining formula in the language of either of these theories is "predicative" or "impredicative".

4. All the defining formulae of T1 are "predicative".

5. At least one defining formula of T2 is "impredicative".

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

-
Although the main issue here is intended to be conditions 4, 5, and 6, I suspect that there will be real difficulty with 3. Part of the problem is that it's not easy to define predicativity precisely without generating some controversy. Another part is the possibility that, after you've defined predicativity precisely, two or more of the predicative defining formulas of T1 might conspire to imply some impredicative defining formula, in which case T2 might be obtained by adding the latter to T1 as a new defining formula, so that T2 might actually be equivalent to T1. –  Andreas Blass Oct 14 '13 at 22:47

As Andreas points out, condition 3 is problematic. However, I think the spirit of the question can be answered by a simple example. Let T be some weak subtheory of ZFC which is mutually interpretable with PA and let T1 be T plus the assertion Con(Z) for each finite fragment Z of ZFC. Let T2 be ZFC. Since ZFC proves Con(Z) for every finite fragment Z of itself, T1 is a subtheory of T2. All the defining formulas of T1 are predicative in the usual sense, and Con(T1) implies Con(ZFC) since if there were an inconsistency in ZFC then we could prove $\neg\,$Con(Z) in T, for some finite fragment Z of ZFC, which would entail that T1 is not consistent.
ZFC and $T_1$ are not just equiconsistent, they are faithfully interpretable in each other (by the Orey–Hájek–Lindström criterion). –  Emil Jeřábek Oct 15 '13 at 11:33