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.
Date: Sun, 17 May 2020 13:26:58 +0300
Subject: [isabelle] NBG in Isabelle/HOL?
Content-Type: text/plain; charset="UTF-8"
Recently, I stumbled upon a GitHub repository, which seems to contain a
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