Here it is claimed that Lean's type theory is equiconsistent with ZFC + existence of $n$ inaccessible cardinals for every natural $n$. This is a bit worrying if you just want to work with pure ZFC: how do you know if the proof in Lean didn't use the existence of inaccessible cardinals? A first thought would be checking that the proof used didn't use Type u for u bigger than $0$, but someone told me this is not enough. Can someone offer more insight into this?
$\begingroup$
$\endgroup$
2
-
2$\begingroup$ I don’t know much about Lean specifically, but I do know that the aspect of Coq which makes it equiconsistent with ZFC + infinitely many inaccessibles is a combination of the impredicative Prop universe (quantifying over all propositions gives you another proposition) and the universes. $\endgroup$– Mark SavingCommented Apr 12, 2022 at 18:56
-
4$\begingroup$ you might also want to ask this at the new proofassistants.stackexchange.com if you don't get an answer here $\endgroup$– Chris GrossackCommented Apr 12, 2022 at 19:38
Add a comment
|