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

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



Larry Paulson







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