[isabelle] Tarski-Grothendieck set theory – Re: NBG in Isabelle/HOL?



It should be mentioned that Tarski-Grothendieck set theory was also implemented quite successfully in Mizar:

"The Mizar Mathematical Library (MML) consists of Mizar Articles. Two articles form the foundation of the library:
	• built-in notions
	• the axioms of the Tarski-Grothendieck set theory."

	http://www.mizar.org/library/ <http://www.mizar.org/library/>


See also: http://mizar.uwb.edu.pl/version/current/mml/tarski.miz <http://mizar.uwb.edu.pl/version/current/mml/tarski.miz>


Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota
https://doi.org/10.4444/100



> Am 18.05.2020 um 08:33 schrieb Joshua Chen <josh at joshchen.io>:
> 
> Alex Krauss, Kevin Kappelmann and I are working on Tarski-Grothendieck in Isabelle/HOL https://bitbucket.org/cezaryka/tyset/ <https://bitbucket.org/cezaryka/tyset/>, though our current focus is less on formalizing advanced set theory and more to get a usable set-theoretic type system in place. 
> 
> Best, 
> Josh 
>> Message: 2
>> Date: Sun, 17 May 2020 13:26:58 +0300
>> From: Mikhail Chekhov < mikhail.chekhov.w at gmail.com <mailto:mikhail.chekhov.w at gmail.com>>
>> Subject: [isabelle] NBG in Isabelle/HOL?
>> To: cl-isabelle-users at lists.cam.ac.uk <mailto:cl-isabelle-users at lists.cam.ac.uk> 
>> Message-ID:
>> < CACDt=M+_6Cro4TkMeDewVPObuTmnnnv7cHYnDaY69H3NFQi_8Q at mail.gmail.com <mailto:CACDt=M+_6Cro4TkMeDewVPObuTmnnnv7cHYnDaY69H3NFQi_8Q at mail.gmail.com>>
>> 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 ( https://github.com/ioannad/NBG_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.