# Why are impredicative constructions used less in type theory than in material set theory?

Many infinitary objects in (say) ZFC are constructed with impredicative principles. The natural numbers are formed by intersecting every inductive set (whose existence is given by the axiom of infinity). $$\sigma$$-algebras are generated by intersecting all $$\sigma$$-algebras containing the generators; and many algebra textbooks define the generation of subgroups/ideals/subrings etc with this method.

However, although there are such examples in type theory, we don't use that very often even in proof assistants with built-in impredicativity. The natural numbers in Coq are still constructed with inductive types, which are considered predicative. There seems to be some difficulty using the impredicative definitions. Is it only because we don't use excluded middle, or is it some property of type theory that makes it biased towards the predicative side?

• Can you suggest an impredicative definition of natural numbers in type theory? Sep 25, 2022 at 14:37
• Suggested predicativity as a tag synonym for impredicativity
– Couchy
Sep 26, 2022 at 15:14
• Excluded middle is a red herring. Impredicative definitions work quite well in a topos. Aug 22 at 16:26

Regarding natural numbers, and inductive types (ie. initial algebras of some form) in general, impredicative encodings are inconvenient, as they only specify weakly initial algebras, rather than initial ones. This means that while one can define functions by recursion on natural numbers, it is not possible to prove things by induction (indeed, induction is not derivable for impredicative encodings). It is not even possible to show that the (impredicatively encoded) booleans $$true$$ and $$false$$ are different! As far as I understand, this is why Cedille adds some kind of parametricity on top of their impredicative definitions, in order to regain the possibility to do proofs by induction. Note also the other answer by Mike Shulman, regarding the fact that in a setting where you have a primitive identity type, you can use it to "carve out" better-behaved types out of the standard impredicative encodings, letting you regain induction.

Moreover, the computational behaviour of impredicative encodings is quite impractical, as the reduction rules you get for the recursor are not the ones you could hope for (typically, you do not have that $$rec_{\mathbb{N}}(P,b_0,b_{S},S\ n) \rightarrow b_S\ n \ rec_{\mathbb{N}}(P,b_0,b_{S},n)$$ for an open $$n$$). This is linked with the standard weirdness that the predecessor function on Church-encoded natural numbers executes in a number of steps proportional to the size of the integer. For more about this, you can go look up the original paper by Paulin-Mohring on adding inductive types to Coq, where she motivates a great deal her addition.

Finally, using impredicativity where only much weaker principles would suffice is also questionable. Not only because this feels like using a bazooka to kill a fly, but also because in practice (proof-relevant) impredicativity is incompatible with many principles, typically classical ones (this is why impredicative Set is not part of default Coq any more). Moreover, if you care about foundations, giving a good account of (proof-relevant) impredicativity is hard, because Polymorphism is not set-theoretic (here polymorphism is pretty much the same thing as proof-relevant impredicativity), so there are no models of it which interprets types as sets.

There is one situation where these impredicative definitions pose much less problems though, namely that of proof-irrelevant impredicativity, ie. defining a proposition in an impredicative way. Indeed:

• you do not care about induction principles for these, because you do not want to distinguish two inhabitants of a proposition (which is exactly what induction gives you);
• you should not care too much about computational content, again because the less you look at computation in proof-irrelevant types, the better;
• proof-irrelevant impredicativity has set-theoretic models (if you interpret the impredicative sort as the two-element set), and it is in general easier to model.

In practice, in Coq for instance, you can still define propositions by induction, but this is usually seen as just a convenience to talk about an impredicatively-defined proposition, that could easily be desugared. Indeed, Coq by default only generates non-dependent recursors, but no dependent induction principle, and if you look at the set-theoretic models of CIC by Werner (as far as I know, the state of the art), he models inductive types, but does not handle inductive propositions, saying those can just be impredicatively encoded.

• These are all quite cool to know, but why can ZF use impredicative natural numbers at ease, while type theories can't? Surely it's not because ZF is "not set-theoretic"?
– Trebor
Sep 24, 2022 at 2:25
• In the impredicative encoding of integers in ZF, the impredicativity is used to define a proof-irrelevant proposition (being an integer) on a pre-existing datatype (the class of sets). But in the impredicative encoding of integers in System F/CC, we use the impredicative definition for the datatype itself. In other words, we are replacing integers with the type of "proofs of integer-ness". The two are very similar, but not quite the same, which could explain the difficulty of working with the latter.
– Loïc
Sep 25, 2022 at 18:06
• I think there is some uncarity here about what type theory we're talking about. Could you provide a little more details about one specific possible type theory that allows us to have impredicative encodings? Sep 26, 2022 at 20:39
• I do not know for Loïc, but what I have in mind are Pure Type Systems of the λ-cube, especially the Calculus of Constructions (possibly with an infinite hierarchy of universes, but I do not think that this makes a difference here), or the purely functional fragments of (old) Coq’s type theory, which deviate from CC by having two impredicative sorts as the lowest universes, one for "irrelevant" content (Prop) and one for "relevant" content (Set). I think these are the systems considered in the papers by Geuvers, Paulin-Mohring and Reynolds I linked to. Sep 27, 2022 at 9:09

Induction over impredicative encodings requires internalizing a small amount of parametricity. See https://cedille.github.io/ for an example of a language that does this. Otherwise working around the lack of induction requires really awkward use of setoids similar to working around extensionality.

It's worth noting impredicative Set in Coq is inconsistent with unique choice. See https://github.com/coq/coq/wiki/Impredicative-Set .

Because impredicative set sorts can be awkward to use or inconsistent with common axioms they're not very common in type theories. Also impredicativity leads to more complicated metatheory.

IIRC some type theories omit inductive types for proof irrelevant sorts. Maybe it ought to be the case that in provers like Coq

Inductive or (A B: SProp): SProp := | left (a: A) | right (b: B).


Desugars to an impredicative encoding somewhere. But I'm not sure of the precise details of how this should work.

• Actually requiring parametricity strikes me as odd, because parametricity is anti-classical, and ZFC certainly uses impredicativity well without parametricity!
– Trebor
Sep 23, 2022 at 1:32
• @Trebor TBH I haven't really looked into how Cedille does things and whether it is compatible with classical axioms. I'm not really familiar with how set theory is used in practice but I guess once you have quotients the awkward setoid problem is really only a minor issue. IIRC nominal sets aren't compatible with choice either which is a pig when trying to add HOAS to things. Not sure why HOAS is so violently anti classical. Sep 23, 2022 at 2:11

This is not directly an answer to the question, but since two other answers have claimed that impredicative encodings can't satisfy induction principles, I thought someone ought to set the record straight.

It's true that the ordinary naive impredicative encodings do not satisfy induction principles. However, there are enhanced impredicative encodings that do satisfy induction principles. This was shown by Awodey, Frey, and Speight in Impredicative Encodings of (Higher) Inductive Types for type theory with UIP. For homotopy type theory it is trickier, but I sketched an enhancement of their approach using idempotent-splitting here.

I don't claim that the resulting encodings are practical, and they certainly have all the same drawbacks as the naive impredicative encodings. But in principle, it is possible to encode datatypes impredicatively in a way that does satisfy an induction principle.

• Thanks for the correction, I knew about the earlier work on inductive types, but not about this one. I'll add a note to my answer. Nov 14, 2022 at 10:52
• Regarding the fact that these encodings lack large elimination, does this mean you also cannot prove non-confusion/injectivity of constructors (the standard proof of which crucially relies on large elimination)? If so, in my opinion this means that the induction principle is actually quite weak… Nov 14, 2022 at 11:00
• @MevenLennon-Bertrand Can't you have a smaller (predicative) universe containing true and false inside the impredicative universe? Eliminating into that would suffice to prove injectivity and disjointness of constructors. Nov 15, 2022 at 1:58
• Ah, this is an interesting question! I do not know of any system like this, but it might doable, and in which case indeed you could prove those basic properties. Nov 15, 2022 at 10:41