Grothendieck universes

DOI10.2478/FORMA-2020-0018MaRDI QIDQ2113837zbMATH OpenOpenAlexFDO

Authors Karol Pąk

Publication date 14 March 2022

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

Full work available at URL https://doi.org/10.2478/forma-2020-0018

zbMATH Keywords

Grothendieck universeTarski-Grothendieck set theoryTarski's axiom A

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Non-trivial universes and sequences of universes
• A tale of two set theories
• scientific article; zbMATH DE number 3279146
• Canonical form of Tarski sets in Zermelo-Fraenkel set theory

Cites work

• scientific article; zbMATH DE number 3279146 (Why is no real title available?)
• A tale of two set theories
• Mizar: state-of-the-art and beyond
• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(2)

• Combining higher-order logic with set theory formalizations
• Non-trivial universes and sequences of universes

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Grothendieck universes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2113837)