# A Tale of Two Set Theories

arXiv: https://arxiv.org/abs/1907.08368 · HTML: https://mlsanity.com/paper/1907.08368/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Jul 2019.

## Built on by (most cited first, 2 of 2)

- [Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents](https://mlsanity.com/paper/2603.06737/) (2026)
- [Translating SUMO-K to Higher-Order Set Theory](https://mlsanity.com/paper/2305.07903/) (2023)

## Abstract (arXiv)

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.