Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Tarski-Grothendieck set theory – NBG in Isabel...

view this post on Zulip Email Gateway (Aug 23 2022 at 09:11):

From: Ken Kubota <mail@kenkubota.de>
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

Last updated: Nov 21 2024 at 12:39 UTC