- New
-
Topics
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- Journals
- Submit material
- More
Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe
Annals of Pure and Applied Logic 120 (1-3):165-196 (2003)
Abstract
We define a realizability interpretation of Aczel's Constructive Set Theory CZF into Explicit Mathematics. The final results are that CZF extended by Mahlo principles is realizable in corresponding extensions of T 0 , thus providing relative lower bounds for the proof-theoretic strength of the latterMy notes
Similar books and articles
Upper Bounds for metapredicative mahlo in explicit mathematics and admissible set theory.Gerhard Jäger & Thomas Strahm - 2001 - Journal of Symbolic Logic 66 (2):935-958.
Realization of analysis into explicit mathematics.Sergei Tupailo - 2001 - Journal of Symbolic Logic 66 (4):1848-1864.
Relationships between constructive, predicative and classical systems of analysis.Solomon Feferman - unknown
Explicit mathematics with the monotone fixed point principle. II: Models.Michael Rathjen - 1999 - Journal of Symbolic Logic 64 (2):517-550.
Realizing Mahlo set theory in type theory.Michael Rathjen - 2003 - Archive for Mathematical Logic 42 (1):89-101.
Extending Martin-Löf Type Theory by one Mahlo-universe.Anton Setzer - 2000 - Archive for Mathematical Logic 39 (3):155-181.
Constructive mathematics in theory and programming practice.Douglas Bridges & Steeve Reeves - 1999 - Philosophia Mathematica 7 (1):65-104.
Consistency of strictly impredicative NF and a little more ….Sergei Tupailo - 2010 - Journal of Symbolic Logic 75 (4):1326-1338.
Explicit mathematics with the monotone fixed point principle.Michael Rathjen - 1998 - Journal of Symbolic Logic 63 (2):509-542.
Extending the system T0 of explicit mathematics: the limit and Mahlo axioms.Gerhard Jäger & Thomas Studer - 2002 - Annals of Pure and Applied Logic 114 (1-3):79-101.
Operational set theory and small large cardinals.Solomon Feferman with with R. L. Vaught - manuscript
Mathematical proof theory in the light of ordinal analysis.Reinhard Kahle - 2002 - Synthese 133 (1/2):237 - 255.
Analytics
Added to PP
2014-01-16
Downloads
28 (#555,203)
6 months
3 (#992,474)
2014-01-16
Downloads
28 (#555,203)
6 months
3 (#992,474)
Historical graph of downloads
Citations of this work
Does reductive proof theory have a viable rationale?Solomon Feferman - 2000 - Erkenntnis 53 (1-2):63-96.
A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is Π 1 -equivalent to KP.Kentaro Sato & Rico Zumbrunnen - 2015 - Annals of Pure and Applied Logic 166 (2):121-186.
A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman's explicit mathematics T 0.Kentaro Sato - 2015 - Annals of Pure and Applied Logic 166 (7-8):800-835.
Characterizing the interpretation of set theory in Martin-Löf type theory.Michael Rathjen & Sergei Tupailo - 2006 - Annals of Pure and Applied Logic 141 (3):442-471.
Reflections on reflections in explicit mathematics.Gerhard Jäger & Thomas Strahm - 2005 - Annals of Pure and Applied Logic 136 (1-2):116-133.
References found in this work
The Type Theoretic Interpretation of Constructive Set Theory.Peter Aczel, Angus Macintyre, Leszek Pacholski & Jeff Paris - 1984 - Journal of Symbolic Logic 49 (1):313-314.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Proof-theoretic analysis of KPM.Michael Rathjen - 1991 - Archive for Mathematical Logic 30 (5-6):377-403.
Proof theory of reflection.Michael Rathjen - 1994 - Annals of Pure and Applied Logic 68 (2):181-224.
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-7c76586df8-4c2ch uwo