## Stream: general

### Topic: Consistency strength of different theorem provers

#### Kenny Lau (Jan 29 2020 at 08:49):

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

#### Johan Commelin (Jan 29 2020 at 08:50):

In theory or in practice?

#### Kevin Buzzard (Jan 29 2020 at 08:57):

I'd be interested in a theoretical answer

#### Mario Carneiro (Jan 29 2020 at 11:24):

PA < HOL < ZFC < CIC < TG

#### Mario Carneiro (Jan 29 2020 at 11:26):

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 (Jan 29 2020 at 11:27):

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

#### Mario Carneiro (Jan 29 2020 at 11:27):

actually Agda is probably inconsistent so it goes at the top

#### Mario Carneiro (Jan 29 2020 at 11:28):

• 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 (Jan 29 2020 at 11:30):

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 (Jan 29 2020 at 11:30):

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

#### Kenny Lau (Jan 29 2020 at 11:30):

what do you mean Adga is probably inconsistent :rolling_on_the_floor_laughing:

#### Johan Commelin (Jan 29 2020 at 11:31):

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 (Jan 29 2020 at 11:31):

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

#### Mario Carneiro (Jan 29 2020 at 11:32):

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

#### Mario Carneiro (Jan 29 2020 at 11:34):

I think it is open whether Coq and Lean are equiconsistent

#### Mario Carneiro (Jan 29 2020 at 11:35):

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 (Jan 29 2020 at 11:36):

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

#### Mario Carneiro (Jan 29 2020 at 11:37):

HOL4 is also using plain HOL

#### Johan Commelin (Jan 29 2020 at 11:37):

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:

that too

#### Ulrik Buchholtz (Jan 29 2020 at 13:10):

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 (Jan 29 2020 at 13:16):

even with the induction-recursion?

#### Ulrik Buchholtz (Jan 29 2020 at 13:28):

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.

Last updated: May 17 2021 at 22:15 UTC