# A Tale of Two Set Theories

## 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1907.08368