21
$\begingroup$

I read this CSTheory SE post, which suggests that it is often not clear what variant of MLTT or CIC is being referred to. But I would like to know the proof-theoretic strengths of the various underlying foundational systems for more 'constructive' proof assistants such as Agda, Coq, Lean. For example, this paper gives the proof-theoretic strength of MLTT[1984]. But Coq is not based on MLTT[1984], but on some (evolving?) variant of CIC. This introduction seems to mix both type theory and Coq, and omits details "for the sake of simplicity", so I don't really know what is the whole system...

Can anyone present a precise table comparing the proof-theoretic strengths of the most common systems underlying Agda, Coq, Lean? In particular, I am interested in what happens when features that might be considered impredicative are included or excluded. So far I have seen two, one being impredicative types (e.g. impredicative Prop) and the other being impredicative inductive/recursive constructions. I am also interested in what happens when LEM is included or excluded, because it seems to me that we are unable to provide non-circular (ontological) justification for having both impredicative Prop and LEM. (Related.)

For instance, what is the strength of MLTT[1984]+LEM? Does it exceed that of ZBQC ≅ MOST? What about CIC and CIC+LEM?

$\endgroup$
5
  • 3
    $\begingroup$ Adding LEM doesn't increase the strength. This is seen by the double negation translation. $\endgroup$
    – Trebor
    Mar 29, 2022 at 23:42
  • 3
    $\begingroup$ @Trebor there is no such thing as a double negation for CIC. If you do it on a proof relevant sort, it will break dependent elimination. If you do it on SProp, it works but SProp can only be used to prove dead branches so you don't increase you expressivity in Type. $\endgroup$ Mar 30, 2022 at 9:39
  • 4
    $\begingroup$ @Trebor: No, double-negation translation works for only certain systems, such as pure FOL to pure IFOL, or PA to HA. Even for FOL theories, it does not imply that adding LEM does not change the strength. Over the base theory IFOL we have ( A+LEM ⊢ Q ) iff ( DN(A) ⊢ DN(Q) ) where DN is the double-negation translation, which is not the same as ( A ⊢ DN(Q) ). In fact, CZF is quite weak compared to ZFC but CZF+LEM = ZFC. $\endgroup$
    – user21820
    Mar 30, 2022 at 10:05
  • $\begingroup$ Of course it depends on what you call LEM. If you interpret it naively, then HoTT + LEM = Falso, which is the most dramatic strength increase you can name. In practice we mean some version of truncated LEM, which is fine. $\endgroup$
    – Trebor
    Mar 30, 2022 at 10:16
  • $\begingroup$ @Trebor: I meant full LEM, which is not known to be inconsistent with MLTT and CIC. And I am not interested in HoTT in this post. Either way, I don't understand why you don't acknowledge that there is no double-negation translation for MLTT/CIC, which makes your initial comment wrong. $\endgroup$
    – user21820
    Mar 30, 2022 at 12:46

1 Answer 1

26
$\begingroup$

Here are a few comparisons of dependent type theories with fragments of Peano arithmetic and set theories that I know of:

Predicative systems (the MLTT family)

Predicative systems are comparable with small fragments of second-order arithmetic. Their strength is measured by which inductive definitions are allowed:

  • When there is only a type of natural numbers, we get the strength of ATR₀, in the sense that both theories prove the same Π⁰₂ statements about arithmetic (proved in the paper you mention). ATR₀ is a small fragment of PA2 which plays an important role in reverse mathematics.
  • Adding W-types makes the system stronger than Δ¹₂-CA but weaker than Π¹₂-CA, which are slightly larger fragments of PA2.
  • Induction-recursion is still a bit stronger, but is expected to be bounded above by KPM+ (see here) which is still weaker than Π¹₂-CA, I believe. This is more or less the theory of Agda.

The order can be refined by taking into account the number of predicative universes : MLTT₁ < MLTT₂ < ... < MLTTω < MLTT₁ + W < ... MLTTω + W < MLTT₁ + IR < ...

A detailed table that also includes ordinal notations and references can be found on the nLab.

Extensionality axioms such as function extensionality, proposition extensionality, UIP, univalence, equality reflection... do not add any logical strength to the system. The full law of excluded middle, however, is another story: now any type is either inhabited or not, which basically makes Bool an impredicative universe of propositions — and impredicative systems are much stronger. In fact, MLTT + LEM has the same strength as CIC + LEM.

Impredicative systems (System F, CC, CIC)

The introduction of an impredicative universe adds a tremendous amount of logical strength to a system. We jump from small fragments of second-order arithmetic to systems which are at least as strong as the full PA2.

  • System F has the strength of second-order arithmetic, in the sense that an integer function is provably total in PA2 if and only if it can be defined in system F (standard reference).
  • CC, the calculus of constructions (which has an impredicative universe Prop which sits inside the predicative universe Type) has the strength of higher-order arithmetic.
  • CCω, which adds a hierarchy of predicative universes, is stronger than Zermelo set theory (proved here), but weaker than ZF set theory (as witnessed by the normalization proof).

Note that the strength comparison theorems are about definable functions, not provable arithmetic statements as before. Indeed, all of these systems have no inductive types at all, so even the integers need to be encoded with impredicativity. And while you can define very complex functions on these impredicative integers, predicates cannot tell them apart: you can't even prove 0≠1. If we want to do such things, we need to add inductive types with large elimination, which results in CIC, the calculus of inductive constructions.

  • If we restrict large elimination in the impredicative universe to sub-singleton inductive types, then we can lift functions that are defined on impredicative integers to predicative, inductive integers while remaining compatible with classical set-theoretic semantics. This is more or less the theory of Coq.
  • If we allow large elimination for all inductive types in the impredicative universe, then the system becomes incompatible with classical logic.
  • Finally, if you add LEM and a variant of the axiom of choice to CIC, then it becomes comparable with ZFC set theory (proved here)
$\endgroup$
16
  • $\begingroup$ Thank you very much. Can you provide a precise reference for CIC, that lists all the rules in one place precisely? I am not comfortable with the references I can find, which mix precise type-theory syntax with a lot of verbose English phrases. In particular, it seems that the CIC in your post is actually not the same as the CIC in the introduction I cited... $\endgroup$
    – user21820
    Mar 30, 2022 at 12:56
  • $\begingroup$ Like MLTT, CIC is used for several closely related systems — they all feature dependent types, an impredicative universe and inductive types, but there is some fuzziness surrounding the specifics of the (co)inductive types and the predicative universes (polymorphism, cumulativity...). I think my use of the word roughly matches the introduction of C. Paulin-Mohring, though. $\endgroup$ Mar 30, 2022 at 15:07
  • $\begingroup$ No, the one in my cited PDF is impredicative, but the one in your post seems to be predicative, because you talk later about adding impredicative universes. If there is fuzziness everywhere in the literature, can you please list out explicitly all the rules in the CIC that your post is supposedly about? Thanks! $\endgroup$
    – user21820
    Mar 30, 2022 at 15:12
  • $\begingroup$ Other than that, there is a description in the Coq reference manual (with all the options, including SProp, coinduction, and several notions of polymorphism — but the complexity of this version means that its meta-theory is not completely clear), in Timany and Sozeau's "Consistency of the pCuIC" (but this system does not have any kind of inductive types inside of Prop, which means there is much less functions on the inductive natural numbers), and in the various formalizations of the system, such as MetaCoq. $\endgroup$ Mar 30, 2022 at 15:13
  • $\begingroup$ Maybe I was not clear enough in my answer: MLTT is predicative, and the CIC is impredicative (I describe it as an extension of CCω, which is impredicative, with inductive types). I don't believe I mention CIC before talking about impredicativity, so it would help me if you could point out what made you think that. $\endgroup$ Mar 30, 2022 at 15:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.