Cut elimination for Zermelo set theory

TL;DR

This paper demonstrates how to encode Zermelo set theory within deduction modulo using rewrite rules, ensuring proof normalization by translating set theory into graph-theoretic primitives and bisimilarity.

Contribution

It introduces a novel encoding of Zermelo set theory as a theory of pointed graphs with rewrite rules, establishing normalization and conservativity in deduction modulo.

Findings

Proof normalization for the intuitionistic fragment

Encoding set theory as graph primitives and bisimilarity

Deduction modulo extension conservativity

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.