A Logical Framework for Set Theories

Arnon Avron
(Tel-Aviv University )

Axiomatic set theory is almost universally accepted as the basic theory which provides the foundations of mathematics, and in which the whole of present day mathematics can be developed. As such, it is the most natural framework for Mathematical Knowledge Management. However, in order to be used for this task it is necessary to overcome serious gaps that exist between the "official" formulations of set theory (as given e.g. by formal set theory ZF) and actual mathematical practice.

In this work 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.

Invited Presentation in Simona Ronchi della Rocca and Elaine Pimentel: Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2011), Belo Horizonte, Brazil, 27 August 2011, Electronic Proceedings in Theoretical Computer Science 81, pp. 3–15.
Published: 24th March 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.81.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org