Re: [isabelle] NBG in Isabelle/HOL?

Alex Krauss, Kevin Kappelmann and I are working on Tarski-Grothendieck in Isabelle/HOL, though our current focus is less on formalizing advanced set theory and more to get a usable set-theoretic type system in place.

Message: 2
Date: Sun, 17 May 2020 13:26:58 +0300
From: Mikhail Chekhov < mikhail.chekhov.w at>
Subject: [isabelle] NBG in Isabelle/HOL?
To: cl-isabelle-users at
< CACDt=M+_6Cro4TkMeDewVPObuTmnnnv7cHYnDaY69H3NFQi_8Q at>
Content-Type: text/plain; charset="UTF-8"

Dear All,

Recently, I stumbled upon a GitHub repository, which seems to contain a
formalization of NBG in Isabelle/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

Kind Regards,
Mikhail Chekhov

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