Extending constructive operational set theory by impredicative principles

Mathematical Logic Quarterly 57 (3):299-322 (2011)
  Copy   BIBTEX


We study constructive set theories, which deal with operations applying both to sets and operations themselves. Our starting point is a fully explicit, finitely axiomatized system ESTE of constructive sets and operations, which was shown in 10 to be as strong as PA. In this paper we consider extensions with operations, which internally represent description operators, unbounded set quantifiers and local fixed point operators. We investigate the proof theoretic strength of the resulting systems, which turn out to be impredicative . © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim



    Upload a copy of this work     Papers currently archived: 91,102

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

18 (#747,034)

6 months
3 (#643,273)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Andrea Cantini
Università degli Studi di Firenze

References found in this work

Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Foundations of Constructive Analysis.John Myhill - 1972 - Journal of Symbolic Logic 37 (4):744-747.
Choice Implies Excluded Middle.N. Goodman & J. Myhill - 1978 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 24 (25-30):461-461.

View all 19 references / Add more references