# A question about whether impredicative formulae always lead to (paradoxical) inconsistencies in formalized theories

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

## 1 Answer

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.

To your broader point, the assertion that any given recursively enumerable formal system is consistent would be considered by a standard predicativist to be intelligible and to have a definite truth value. So a predicativist should be willing to be a formalist with regard to systems such as ZFC which lack a predicative justification but which seem likely to be consistent.

-
If I read this correctly, T1 is the formalization of a predicativist mathematician who has just smoked a joint. Still predicativist, but with bleary eyes and giggling. – Andrej Bauer Oct 15 '13 at 6:46
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
@Andrej: it does sound like someone just smoked a joint ... – Nik Weaver Oct 15 '13 at 19:04
Thanks for your many interesting responses. I realize that my condition (3) will cause trouble and I deliberately stated it that way because there is so much disagreement about what makes a formula predicative or impredicative. As far as I am concerned any criterion that is precise and published in the literature will do. But one should probably not raise the bar too high. For those who feel that PA is loaded with impredicative formulae, it probably seems obvious that no such theories as T1 and T2 could possibly exist. – Garabed Gulbenkian Oct 15 '13 at 19:21
It occurs to me that the weak theory of arithmetic known as Robinson's Q could be takenas T1, since there would see to be many predicativity – Garabed Gulbenkian Oct 17 '13 at 18:08