7
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ 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). $\endgroup$
    – Mark S.
    Sep 26, 2019 at 17:16

1 Answer 1

Reset to default
7
$\begingroup$

Most people who use Isabelle, use it with HOL. It seems pretty clear that this archive is created by and meant to serve the needs of Isabelle users, so it makes sense the entries will be in the most common theory used with Isabelle. As far as I can tell, this archive does not mandate that you use Isabelle/HOL, and seemingly you could provide an Isabelle/ZF derivation if you wanted.

A quick Google for "isabelle hol set theory" produces this paper, A Formalized Set-Theoretical Semantics for Isabelle/HOL by Rabe and Iancu, which provides a (machine-checked in Twelf) formalization of a ZFC semantics for Isabelle/HOL. I'm confident this is not the first work comparing HOL and ZFC. You can also no doubt find papers with a more precise comparison between HOL and ZFC. Classical HOL is typically treated as having a fairly naive set theoretic semantics.

In practice, I strongly suspect going from informal mathematics to a machine-checked system is, for most math, comparably (and significantly) difficult regardless of the foundation used of the target system if its classical, and often even when it's constructive. Classical versus Constructive is definitely a bigger divide than Set Theory versus Type Theory. Another way of saying this is a good chunk of math is not in any particular foundations, or you could make about as strong a claim that some piece of informal mathematics is "in HOL" as it is "in ZFC".

While I imagine most mathematicians, especially those who can't recite the ZFC axioms, are happy enough to simply assume some suitable metatheoretical work has been done for HOL, this might not be a terrible opportunity to evaluate a foundations directly on its own merit...

$\endgroup$
4
  • $\begingroup$ This makes some sense, but if your claim is that it should be just as easy to formalize math in ZF and ZF is "tried and true", it seems silly that almost all Isabelle users have chosen to formalize results in a foundation which hasn't been studied even close to as much and isn't necessarily widely accepted. I'm not really sure what it means to have a formal semantics for HOL in ZF. Does this mean a proof in HOL can be translated into a proof in ZF, hence HOL is in some sense the same as (or a subset of) ZF? $\endgroup$
    – Physical Mathematics
    Sep 25, 2019 at 4:33
  • 2
    $\begingroup$ @KeeferRowan Answering the latter first, having a semantics in ZFC means we can interpret HOL into ZFC which means we can view working in HOL as just shorthand for manipulating certain ZFC sets. This implies ZFC believes HOL is consistent and means HOL is strictly weaker than ZFC. As for the former part, I didn't say "just as easy", merely comparable. Neither is easy. This was also for the task of formalizing some informal, nominally "in ZFC" math which is a very different task from working formal-first. Either way, one might say it is silly to assume we stumbled upon the optimal... $\endgroup$
    – Derek Elkins left SE
    Sep 25, 2019 at 5:12
  • 3
    $\begingroup$ ... foundations in 1922 and have learned nothing of value in the last century and the advent of digital computers in no way changed things. Acceptance is not particularly relevant. The meta-theoretical results ensure that if you "believe in ZFC" you can (even more) "believe in HOL", but I don't think most mathematicians really care. Familiarity is not relevant as while Isabelle/HOL will certainly be unfamiliar to most mathematicians, so will Mizar which is based on an extension of ZFC. Consensus about results is irrelevant when you only care about what your proof checker says is true. $\endgroup$
    – Derek Elkins left SE
    Sep 25, 2019 at 5:13
  • $\begingroup$ 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. $\endgroup$
    – Physical Mathematics
    Sep 25, 2019 at 19:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .