TL;DR
This paper explores the relationship between two set theories, demonstrating their equivalences and translating axioms and operators between the first-order Mizar and higher-order Egal frameworks.
Contribution
It establishes formal equivalences between the two set theories and constructs key axioms and operators across them, bridging first-order and higher-order frameworks.
Findings
Proved Tarski's Axiom A in Egal
Constructed Grothendieck Universe operator in Mizar
Showed equivalences of higher-order terms in Egal and first-order presentations
Abstract
We describe the relationship between two versions of Tarski-Grothendieck set theory: the first-order set theory of Mizar and the higher-order set theory of Egal. We show how certain higher-order terms and propositions in Egal have equivalent first-order presentations. We then prove Tarski's Axiom A (an axiom in Mizar) in Egal and construct a Grothendieck Universe operator (a primitive with axioms in Egal) in Mizar.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.