Zulip Chat Archive

Stream: general

Topic: Consistency strength of different theorem provers


view this post on Zulip Kenny Lau (Jan 29 2020 at 08:49):

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

view this post on Zulip Johan Commelin (Jan 29 2020 at 08:50):

In theory or in practice?

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 08:57):

I'd be interested in a theoretical answer

view this post on Zulip Mario Carneiro (Jan 29 2020 at 11:24):

PA < HOL < ZFC < CIC < TG

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 29 2020 at 11:27):

actually Agda is probably inconsistent so it goes at the top

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 29 2020 at 11:30):

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

view this post on Zulip Kenny Lau (Jan 29 2020 at 11:30):

what do you mean Adga is probably inconsistent :rolling_on_the_floor_laughing:

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Jan 29 2020 at 11:31):

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

view this post on Zulip Mario Carneiro (Jan 29 2020 at 11:32):

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

view this post on Zulip Mario Carneiro (Jan 29 2020 at 11:34):

I think it is open whether Coq and Lean are equiconsistent

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 29 2020 at 11:37):

HOL4 is also using plain HOL

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Jan 29 2020 at 11:37):

that too

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 29 2020 at 13:16):

even with the induction-recursion?

view this post on Zulip 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 Σ21 \Sigma^1_2 -AC.


Last updated: May 17 2021 at 22:15 UTC