# Why does Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF?

Why does Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF? If you took your average mathematician on the street and tried to pin down the axiomatics they are implicitly using they'd probably say ZF(C). Even if they couldn't give formal statements of the axioms, that's what they trust could give formal statement of their proofs/results. Why then does a formalization project like Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF in formalizing proofs in things like Analysis? Is there a reason to believe the axiomatization of Isabelle/HOL is stronger/weaker/the same as ZF(C) or is it just incomparable? Are there any relative consistency proofs? Basically, if you believe ZF, why should you believe Isabelle/HOL?

• As an aside, while it's not the "Archive of Formal Proofs" (nor the "Journal of Formalized Mathmatics", nor similar things for other systems), the Metamath Proof Explorer has a bunch of formal proofs that are (I suppose arguably for formal logic reasons) explicitly using ZF(C). Sep 26, 2019 at 17:16

• Alright, that does clear things up pretty well. Basically, I'm happy so long as ZFC $\geq$ HOL in some meaningful sense. I wouldn't be happy if ZFC and HOL were incomparable or of indeterminate relation. Since ZFC is the nominal framework for basically all of contemporary math (besides maybe some set theory stuff and logic stuff), it seems a necessary precondition for HOL formalized proofs to be interesting is if they guarantee the analogous result holds in ZFC. Sep 25, 2019 at 19:28