Annals of Pure and Applied Logic 115 (1-3):33-70 (2002)

Laura Crosilla
University of Oslo
The paper investigates inaccessible set axioms and their consistency strength in constructive set theory. In ZFC inaccessible sets are of the form Vκ where κ is a strongly inaccessible cardinal and Vκ denotes the κth level of the von Neumann hierarchy. Inaccessible sets figure prominently in category theory as Grothendieck universes and are related to universes in type theory. The objective of this paper is to show that the consistency strength of inaccessible set axioms heavily depend on the context in which they are embedded. The context here will be the theory CZF− of constructive Zermelo–Fraenkel set theory but without -Induction . Let INAC be the statement that for every set there is an inaccessible set containing it. CZF−+INAC is a mathematically rich theory in which one can easily formalize Bishop style constructive mathematics and a great deal of category theory. CZF−+INAC also has a realizability interpretation in type theory which gives its theorems a direct computational meaning. The main result presented here is that the proof theoretic ordinal of CZF−+INAC is a small ordinal known as the Feferman–Schütte ordinal Γ0
Keywords Constructive set theory  Proof theory  Predicativity  Inaccessible set
Categories (categorize this paper)
DOI 10.1016/s0168-0072(01)00083-5
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 63,295
Through your library

References found in this work BETA

Constructive Set Theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.
The Strength of Some Martin-Löf Type Theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Fixed Points in Peano Arithmetic with Ordinals.Gerhard Jäger - 1993 - Annals of Pure and Applied Logic 60 (2):119-132.

View all 7 references / Add more references

Citations of this work BETA

Quotient Topologies in Constructive Set Theory and Type Theory.Hajime Ishihara & Erik Palmgren - 2006 - Annals of Pure and Applied Logic 141 (1):257-265.
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.

View all 6 citations / Add more citations

Similar books and articles

The Consistency Strength of an Infinitary Ramsey Property.George Kafkoulis - 1994 - Journal of Symbolic Logic 59 (4):1158-1195.
On the Axiom of Union.Greg Oman - 2010 - Archive for Mathematical Logic 49 (3):283-289.
A Maximal Bounded Forcing Axiom.David Asperó - 2002 - Journal of Symbolic Logic 67 (1):130-142.
Proper Forcing Extensions and Solovay Models.Joan Bagaria & Roger Bosch - 2004 - Archive for Mathematical Logic 43 (6):739-750.
Localizing the Axioms.Athanassios Tzouvaras - 2010 - Archive for Mathematical Logic 49 (5):571-601.
Forcing Indestructibility of Set-Theoretic Axioms.Bernhard König - 2007 - Journal of Symbolic Logic 72 (1):349 - 360.
Stretchings.O. Finkel & J. P. Ressayre - 1996 - Journal of Symbolic Logic 61 (2):563-585.
Consistency Strength of Higher Chang’s Conjecture, Without CH.Sean D. Cox - 2011 - Archive for Mathematical Logic 50 (7-8):759-775.
On the Consistency Strength of Two Choiceless Cardinal Patterns.Arthur W. Apter - 1999 - Notre Dame Journal of Formal Logic 40 (3):341-345.


Added to PP index

Total views
38 ( #283,125 of 2,448,707 )

Recent downloads (6 months)
2 ( #302,846 of 2,448,707 )

How can I increase my downloads?


My notes