Re: [isabelle] NBG in Isabelle/HOL?

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).

Quaife, A. Automated deduction in von Neumann-Bernays-Gödel set theory. J Autom Reasoning 8, 91–147 (1992).


> On 17 May 2020, at 11:26, Mikhail Chekhov <mikhail.chekhov.w at> wrote:
> 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
> direction?

Larry Paulson

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