Authors: Gilles Dowek, Alexandre Miquel
Title: A cut elimination theorem for set theory
Abstract: 
We show how to express Zermelo's 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
cut-elimination property.  For that, we first rephrase set theory
as a theory of pointed graphs (following a paradigm due to 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's theory.
Finally, we build a premodel of this theory from which we deduce
the cut-elimination property for its intuitionistic fragment.