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?
Why does Archive of Formal Proofs use Isabelle/HOL as opposed to Isabelle/ZF
automated-theorem-provingaxiomsfoundationslogic
Related Solutions
You are correct in your explanation of why no proof of self-consistency can ever be trusted. If a proposed nice formal system $S$ (that interprets PA and has a proof verifier program) proves its own consistency, then the incompleteness theorems tell us that in fact it is not consistent. Even more so, $S$ itself knows this fact. This is completely contrary to what Hilbert expected.
Symbolically we can prove Godel's second incompleteness theorems expressed in provability logic: $ \def\nn{\mathbb{N}} \def\con{\text{Con}} \def\sound{\text{Sound}} $
- (GI*) If $S ⊢ \con(S)$ then $S ⊢ 0=1$.
- (GI) $S ⊢ □\con(S)→□(0=1)$.
In general, $\con(S)$ does not say that $S$ is consistent, but merely says that $S$ is arithmetically consistent, namely that $S$ does not prove $(0=1)$.
If $S$ proves $(0=1)$, then $S$ is useless because it proves every false arithmetical sentence. So for $S$ to be useful it must not prove $(0=1)$, in which case $\con(S)$ is a true arithmetical sentence, and hence by (GI*) $S$ must not prove the true arithmetical sentence $\con(S)$.
So it is not that $S ⊢ \con(S)$ has no semantic content. It is a statement about finite strings, and if it is true then it tells us via (GI*) that $S ⊢ 0=1$. You must distinguish carefully between the meaningfulness of "$S ⊢ \con(S)$" and the meaninglessness of asserting "$\con(S)$" just because $S$ proves it (which is of course stupid even if the incompleteness theorems did not hold).
But your explanation of "we cannot bootstrap consistency proofs" is incorrect. You are essentially trying to assert:
We cannot take some exceedingly simple system $A$ that we believe is consistent and from that construct a stronger system $B$ such that $A ⊢ \con(B)$, and then assert that $B$ is consistent.
This is erroneous; you need $A$ to be arithmetically sound (or at least $Σ_1$-sound) before you can go from "$A ⊢ \con(B)$" to "$B$ is consistent"! So it is not enough to start from a consistent $A$. It is true that if $B$ interprets $A$, then $A$ cannot prove $\con(B)$ by (GI*), but that fact does not permit you to make the above assertion.
It is not possible to replace "consistent" by "arithmetically sound" either, because arithmetical soundness is not itself an arithmetical property. So I think there is not much you can say about bootstrapping that requires invoking (GI*).
That said, there are things you can say based on either (GI*) or (GI). For example, either of them suffice to show that $□P→P$ cannot be an axiom for every $P$. Note the relation with Lob's theorems (L*) and (L). This shows that every useful nice formal system $S$ cannot have an internal self-proof-to-truth assumption. Perhaps this is a better way to understand the impact of incompleteness. Note that $S$ can still have the rule ( if $⊢ □P$ then $⊢ P$ ). In fact, this rule is redundant if $S$ is $Σ_1$-sound.
More interestingly (as shown in the linked post), although $S$ proves $P∨¬P$ for every $P$, it may not prove $□P∨□¬P$, nor even $□P∨□¬P∨□¬(□P∨□¬P)$. And (as shown in the other post on that thread), $S$ cannot even have an internal self-consistency-implies-proof-to-truth assumption, namely that $S$ cannot always prove $¬□(0=1)∧□P→P$ without also proving $□(0=1)$ and rendering it all meaningless.
The answer to "are there any constructive higher-order logics" is yes. Martin-Löf type theory and its many descendants and variants are the examples that first come to mind.
However, you seem to be particularly interested in versions of simple type theory as implemented in Isabelle/HOL. In principle, the HOL logic as implemented in Isabelle is the same as that implemented in the other theorem provers in the HOL family (HOL IV, HOL Light, ProofPower, ...). John Harrison's HOL Light presents the logic in a way that clearly separates out the intuitionistic fragment (see his paper HOL Light: an overview). I suspect it would require some significant restructuring of Isabelle/HOL to adopt the HOL Light formulation. If that's something you'd like to happen, then I suggest you raise this on the Isabelle mailing list rather than here.
As a small aside: the axiom of choice implies the axiom of excluded middle in higher-order logic.
Best Answer
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...