[isabelle] NBG in Isabelle/HOL?



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.