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.

翻译：我们展示了如何在模演绎（即用重写规则替代公理）中表述直觉主义策梅洛集合论，使得相应的证明概念具有规范化性质。为此，我们首先将集合论重新表述为点图理论（遵循P. Aczel的范式），通过将集合论等式解释为双相似性，并证明在此框架下，策梅洛公理可分解为图论原语，进而转化为重写规则。接着，我们证明模演绎中所得理论是策梅洛集合论（的微小扩展）的保守扩充。最后，我们证明了该理论直觉主义片段的规范化性质。