A Tale of Two Set Theories
Logic in Computer Science
2019-07-22 v1
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.
Cite
@article{arxiv.1907.08368,
title = {A Tale of Two Set Theories},
author = {Chad E. Brown and Karol Pąk},
journal= {arXiv preprint arXiv:1907.08368},
year = {2019}
}