7
$\begingroup$

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?

$\endgroup$
2
  • 1
    $\begingroup$ Can you suggest an impredicative definition of natural numbers in type theory? $\endgroup$ 2 days ago
  • 2
    $\begingroup$ Suggested predicativity as a tag synonym for impredicativity $\endgroup$
    – Couchy
    yesterday

2 Answers 2

6
$\begingroup$

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.

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, but 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.

$\endgroup$
4
  • $\begingroup$ 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"? $\endgroup$
    – Trebor
    Sep 24 at 2:25
  • 2
    $\begingroup$ 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. $\endgroup$
    – Loïc
    yesterday
  • $\begingroup$ 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? $\endgroup$ 19 hours ago
  • $\begingroup$ 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. $\endgroup$ 6 hours ago
4
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ Actually requiring parametricity strikes me as odd, because parametricity is anti-classical, and ZFC certainly uses impredicativity well without parametricity! $\endgroup$
    – Trebor
    Sep 23 at 1:32
  • $\begingroup$ @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. $\endgroup$ Sep 23 at 2:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.