Anthony Bordg (Mar 12 2021 at 21:28): Anthony Bordg (Mar 12 2021 at 21:28):Are there precise statements that relate the proof-theoretic strength of Isabelle/HOL with some set theories?
Jakub Kądziołka (Mar 12 2021 at 21:32):Sounds like you would be interested in some of Andrei's research — particularily, the ITP'15 and ESOP'17 papers
Anthony Bordg (Mar 13 2021 at 15:02):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?
Jakub Kądziołka (Mar 13 2021 at 16:49):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: Dec 21 2024 at 12:33 UTC