Are there precise statements that relate the proof-theoretic strength of Isabelle/HOL with some set theories?

Sounds like you would be interested in some of Andrei's research — particularily, the ITP'15 and ESOP'17 papers

I had a quick look at some of these works, but they seem to deal with consistency and conservativity of Isabelle/HOL over HOL, which are different questions. If in my initial question I replace Isabelle/HOL by HOL, then does it help?

I'd look into the citations of these papers, but there's also HOL4's Logic manual which constructs a model of HOL in ZFC: https://phoenixnap.dl.sourceforge.net/project/hol/hol/kananaskis-14/kananaskis-14-logic.pdf

Last updated: Jul 15 2022 at 23:21 UTC