Cut elimination for Zermelo set theory
Logic in Computer Science
2023-11-01 v1
Abstract
We show how to express intuitionistic Zermelo set theory in deduction modulo (i.e. by replacing its axioms by rewrite rules) in such a way that the corresponding notion of proof enjoys the normalization property. To do so, we first rephrase set theory as a theory of pointed graphs (following a paradigm due to P. Aczel) by interpreting set-theoretic equality as bisimilarity, and show that in this setting, Zermelo's axioms can be decomposed into graph-theoretic primitives that can be turned into rewrite rules. We then show that the theory we obtain in deduction modulo is a conservative extension of (a minor extension of) Zermelo set theory. Finally, we prove the normalization of the intuitionistic fragment of the theory.
Keywords
Cite
@article{arxiv.2310.20253,
title = {Cut elimination for Zermelo set theory},
author = {Gilles Dowek and Alexandre Miquel},
journal= {arXiv preprint arXiv:2310.20253},
year = {2023}
}