We present a first-order formalization of set theory which has a finite number of axioms. Its syntax is familiar since it provides an encoding of the comprehension symbol. Since this symbol binds a variable in one of its arguments we let the given formalization rest upon a calculus of explicit substitution with de Bruijn indices. This presentation of set theory is also described as a deduction modulo system which is used as an intermediate system to prove that the given presentation is a conservative extension of Zermelo's set theory.
展开▼
