Speaker: Arnon Avron
Abstract: We present formalizations of several axiomatic set theories (including $ZF$) which provide classes of abstraction {\em terms} denoting sets, and are based on purely syntactical (rather than semantic) considerations. Our framework allows for a static check of validity of terms, and makes it possible to reduce all extensions by definitions to abbreviations (Hence it should be convenient for mechanical manipulations, for interactive theorem proving, and for teaching). It also provides a unified treatment of comprehension axioms and of absoluteness properties of formulas. This is particularly important for predicative set theory, to which we shall pay a special attention in this talk.