2023/10/31 by Gilles Dowek, Dowek, Gilles, Alexandre Miquel +1
Computer Science · Mathematics · Psychology · #Advanced Topology and Set Theory #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Philosophy and Theoretical Science
paper · pdf · doi:10.48550/arxiv.2310.20253
openalex publication_date 2023/10/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.