Stream: General

Topic: Isabelle/HOL's proof-theoretic strength


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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 07 2023 at 08:19 UTC