HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

A Finite First-Order Presentation of Set Theory

Stéphane Vaillant 1
1 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : We present a first-order formalization of set theory which has a finite number of axioms. Its syntax is similar to that often used in textbooks: it provides an encoding of the comprehension symbol. We prove that this formalization is a "conservative extension" of Zermelo's set theory. In fact the proof is more general and applies to other variants of Zermelo's set theory like ZF. This formalization rests upon an encoding of the comprehension binder in a language of explicit substitution. This presentation of set theory is also described as a deduction modulo system and the proof of equivalence is done within this formalism.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 8:12:38 PM
Last modification on : Friday, February 4, 2022 - 3:22:53 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:00:12 PM


  • HAL Id : inria-00072244, version 1


Stéphane Vaillant. A Finite First-Order Presentation of Set Theory. RR-4344, INRIA. 2001. ⟨inria-00072244⟩



Record views


Files downloads