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: Mar 28 2024 at 20:16 UTC