Title: λZ: Zermelo’s Set Theory as a PTS with 4 Sorts
Abstract: We introduce a pure type system (PTS) λZ with four sorts and show that this PTS captures the proof-theoretic strength of Zermelo's set theory. For that, we show that the embedding of the language of set theory into λZ via the 'sets as pointed graphs' translation makes λZ a conservative extension of IZ+AFA+TC (intuitionistic Zermelo's set theory plus Aczel's antifoundation axiom plus the axiom of transitive closure)—a theory which is equiconsistent to Zermelo's. The proof of conservativity is achieved by defining a retraction from λZ to a (skolemised version of) Zermelo's set theory and by showing that both transformations commute via the axioms AFA and TC.
Publication Year: 2006
Publication Date: 2006-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 8
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot