A Framework for Formalizing Set Theories Based on the Use of Static Set Terms


We present a new unified framework for formalizations of axiomatic set theories of different strength, from rudimentary set theory to full ZF . It allows the use of set terms, but provides a static check of their validity. Like the inconsistent “ideal calculus” for set theory, it is essentially based on just two set-theoretical principles: extensionality and comprehension (to which we add ∈-induction and optionally the axiom of choice). Comprehension is formulated as: x ∈ {x | ϕ} ↔ ϕ, where {x | ϕ} is a legal set term of the theory. In order for {x | ϕ} to be legal, ϕ should be safe with respect to {x}, where safety is a relation between..



    Upload a copy of this work     Papers currently archived: 76,391

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.


Added to PP

5 (#1,170,170)

6 months
1 (#451,971)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Arnon Avron
Tel Aviv University

Citations of this work

The middle ground-ancestral logic.Liron Cohen & Arnon Avron - 2019 - Synthese 196 (7):2671-2693.

Add more citations

References found in this work

No references found.

Add more references