Constructive Set Theory with Operations

In Logic Colloquium 2004 (2008)
  Copy   BIBTEX


We present an extension of constructive Zermelo{Fraenkel set theory [2]. Constructive sets are endowed with an applicative structure, which allows us to express several set theoretic constructs uniformly and explicitly. From the proof theoretic point of view, the addition is shown to be conservative. In particular, we single out a theory of constructive sets with operations which has the same strength as Peano arithmetic.



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

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

Elementary Constructive Operational Set Theory.Andrea Cantini & Laura Crosilla - 2010 - In Ralf Schindler (ed.), Ways of Proof Theory. De Gruyter. pp. 199-240.
Set theory: Constructive and intuitionistic ZF.Laura Crosilla - 2010 - Stanford Encyclopedia of Philosophy.
A note on Bar Induction in Constructive Set Theory.Michael Rathjen - 2006 - Mathematical Logic Quarterly 52 (3):253-258.
Conservativity of Transitive Closure over weak operational set theory.Laura Crosilla & Andrea Cantini - 2012 - In Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation. De Gruyter.
Constructive notions of set: Part I. Sets in Martin–Löf type theory.Laura Crosilla - 2005 - Annali Del Dipartimento di Filosofia 11:347-387.
Inaccessible set axioms may have little consistency strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.
On the constructive Dedekind reals.Robert S. Lubarsky & Michael Rathjen - 2008 - Logic and Analysis 1 (2):131-152.
The natural numbers in constructive set theory.Michael Rathjen - 2008 - Mathematical Logic Quarterly 54 (1):83-97.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Non-deterministic inductive definitions.Benno van den Berg - 2013 - Archive for Mathematical Logic 52 (1-2):113-135.


Added to PP

18 (#785,610)

6 months
8 (#292,366)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Andrea Cantini
Università degli Studi di Firenze
Laura Crosilla
University of Oslo

Citations of this work

Set theory: Constructive and intuitionistic ZF.Laura Crosilla - 2010 - Stanford Encyclopedia of Philosophy.
The axiom of choice and combinatory logic.Andrea Cantini - 2003 - Journal of Symbolic Logic 68 (4):1091-1108.

Add more citations

References found in this work

No references found.

Add more references