Email Gateway (Aug 23 2022 at 09:09): Email Gateway (Aug 23 2022 at 09:09):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
Recently, I stumbled upon a GitHub repository, which seems to contain a
formalization of NBG in Isabelle/HOL (https://github.com/ioannad/NBG_HOL).
However, if I understand correctly, this development has not been submitted
to the AFP and it is not maintained any longer (the last commit was 4 years
ago). This post is an attempt to "snoop" for information on whether, since
then, anyone has attempted a similar feat. Generally, I am looking for a
working axiomatization of NBG in HOL for Isabelle2020 in the style of "ZFC
in HOL" or its predecessor HOL/ZF.
In this context, I would also be keen to know about other work on the
formalization/semantics of alternative set theories stronger than ZFC (e.g.
MK) in Isabelle/HOL. Is anyone aware of any ongoing projects in this
direction?
Kind Regards,
Mikhail Chekhov
Email Gateway (Aug 23 2022 at 09:10):From: Lawrence Paulson <lp15@cam.ac.uk>
Bernays-Gödel set theory does not look attractive to me. It’s main advantage is its finite axiom system within first-order logic, but that’s irrelevant in our higher-order setting. It’s main drawback is that you simply write a formula when specifying a subset (via the separation axiom), forcing you to find an encoding using a combinator language. Prior attempts to use it with automatic theorem provers only confirm the difficulties:
Belinfante, J.G.F. Computer Proofs in Gödel’s Class Theory with Equational Definitions for Composite and Cross. Journal of Automated Reasoning 22, 311–339 (1999). https://doi.org/10.1023/A:1006050629424
Quaife, A. Automated deduction in von Neumann-Bernays-Gödel set theory. J Autom Reasoning 8, 91–147 (1992). https://doi.org/10.1007/BF00263451
Larry
Larry Paulson
Email Gateway (Aug 23 2022 at 09:10):From: Joshua Chen <josh@joshchen.io>
Alex Krauss, Kevin Kappelmann and I are working on Tarski-Grothendieck in
Isabelle/HOL <https://bitbucket.org/cezaryka/tyset/>, though our current focus
is less on formalizing advanced set theory and more to get a usable set-
theoretic type system in place.
Best,
Josh
Email Gateway (Aug 23 2022 at 09:10):From: Lawrence Paulson <lp15@cam.ac.uk>
Sorry, important correction: “you CANNOT simply write a formula” (such as f(x)=g(x) & x>0).
Email Gateway (Aug 23 2022 at 09:11):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Lawrence Paulson,
Thank you for providing the remark. I did struggle to understand the
intended meaning/significance of the first part of the sentence, but
the meaning of the message could still be inferred from the second part, in
conjunction with what I have seen based on the content of the repository
that I mentioned in my question.
Kind Regards,
Mikhail Chekhov
Last updated: Nov 21 2024 at 12:39 UTC