Name
Abstract | ||
|---|---|---|
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 formulas and finite sets of variables. The various systems we consider differ from each other mainly with respect to the safety relations they employ. These relations are all defined purely syntactically (using an induction on the logical structure of formulas). The basic one is based on the safety relation which implicitly underlies commercial query languages for relational database systems (like SQL). Our framework makes it possible to reduce all extensions by definitions to abbreviations. Hence it is very convenient for mechanical manipulations and for interactive theorem proving. It also provides a unified treatment of comprehension axioms and of absoluteness properties of formulas. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-78127-1_6 | Pillars of Computer Science |
Keywords | Field | DocType |
rudimentary set theory,static set term,unified treatment,new unified framework,set theory,set term,legal set term,safety relation,finite set,axiomatic set theory,comprehension axiom,relational database system,interactive theorem proving,query language,axiom of choice | Axiom of choice,Discrete mathematics,Set theory,Finite set,Algebra,Zermelo–Fraenkel set theory,Axiom,Urelement,General set theory,Mathematics,Universal set | Conference |
Volume | ISSN | ISBN |
4800 | 0302-9743 | 3-540-78126-9 |
Citations | PageRank | References |
7 | 1.03 | 5 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Arnon Avron | 1 | 1292 | 147.65 |