Consistency strength of different theorem provers

Stream: general

[Kenny Lau]

What are the consistency strength of different theorem provers? Which ones can prove which ones consistent?

[Johan Commelin]

In theory or in practice?

[Kevin Buzzard]

I'd be interested in a theoretical answer

[Mario Carneiro]

PA < HOL < ZFC < CIC < TG

[Mario Carneiro]

HOL light uses HOL, Isabelle/HOL uses a slightly stronger version of HOL, Metamath uses ZFC (with TG on the side), Lean and Coq use CIC, Mizar uses TG

[Mario Carneiro]

Agda has some induction recursion extension of CIC that puts it strictly above CIC but below TG

[Mario Carneiro]

actually Agda is probably inconsistent so it goes at the top

[Mario Carneiro]

• PA: Peano Arithmetic (mostly used by logicians, not so popular in theorem provers, used by MM0)
• HOL: Higher order logic
• ZFC: Zermelo-Fraenkel set theory
• CIC: Calculus of inductive constructions
• TG: Tarski-Grothendieck set theory

[Mario Carneiro]

There are a bunch of stronger consistency strengths in the large cardinal hierarchy above TG that are mainly studied in set theory, but I don't know any theorem prover to use them

[Johan Commelin]

I see. So one of my answers after my talk at CPP is plain wrong (-;

[Kenny Lau]

what do you mean Adga is probably inconsistent :rolling_on_the_floor_laughing:

[Johan Commelin]

Because I said that all these theorem provers are more or less equivalent (from the perspective of what they can prove in theory).

[Mario Carneiro]

I think it's still morally correct to say they are all basically equivalent

[Mario Carneiro]

I don't think most people take advantage of these "edge effects" of the system

[Mario Carneiro]

I think it is open whether Coq and Lean are equiconsistent

[Mario Carneiro]

It seems reasonable, although the most likely actual answer is that one or the other is inconsistent so equiconsistency fails. But once we've fixed whatever problems there are it should be true

[Mario Carneiro]

I don't know if Isabelle can prove the consistency of HOL light, but I think it can't

[Mario Carneiro]

HOL4 is also using plain HOL

[Johan Commelin]

It seems reasonable, although the most likely actual answer is that one or the other is inconsistent so equiconsistency fails. But once we've fixed whatever problems there are it should be true

Maybe they're both inconsistent :grimacing:

[Mario Carneiro]

that too

[Ulrik Buchholtz]

PA < HOL < ZFC < CIC < TG

NB, this is the ordering when CIC includes LEM. The strength of CIC without LEM/AC is somewhere between HOL and ZFC. The strength of pCIC (predicative variant, i.e., no impredicative Prop) without LEM/AC is somewhere between PA and HOL (much closer to PA than HOL or even 2nd order arithmetic). In particular, if the theory of Agda is not inconsistent, it's consistency strength is also not much above PA.

[Mario Carneiro]

even with the induction-recursion?

[Ulrik Buchholtz]

even with the induction-recursion?

Yes, it adds certain towers of admissible universes along small recursive ordinals, so it's still relatively tame. Michael Rathjen has explored the upper bounds of some of these systems, e.g. on the superuniverse. This article attempts to upper-bound many conceivable extensions à la induction-recursion; it all fits in a small fragment of 2nd order arithmetic, not much higher than $\Sigma^1_2$-AC.