Skip to main content

Questions tagged [consistency-strength]

Use this tag when discussing the relative logical strength of axiom sets or foundations of theorem provers

Filter by
Sorted by
Tagged with
15 votes
3 answers
419 views

What is known about the consistency of proof assistant metatheories?

I realised I don't know the status of consistency of theorem provers' metatheories - what is currently known? For example, as far as I know Lean's type theory is equiconsistent to ZFC+countably many ...
It'sNotALie.'s user avatar
  • 1,445