Systems of explicit mathematics with non-constructive μ-operator and join

&
Annals of Pure and Applied Logic 82 (2):193-219 (1996)
  Copy   BIBTEX

Abstract

The aim of this article is to give the proof-theoretic analysis of various subsystems of Feferman's theory T1 for explicit mathematics which contain the non-constructive μ-operator and join. We make use of standard proof-theoretic techniques such as cut-elimination of appropriate semiformal systems and asymmetrical interpretations in standard structures for explicit mathematics.

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(96)00005-x

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,127

External links

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

Through your library

My notes

Similar books and articles

Understanding uniformity in Feferman's explicit mathematics.Thomas Glaß - 1995 - Annals of Pure and Applied Logic 75 (1-2):89-106.
Systems of explicit mathematics with non-constructive μ-operator. Part I.Solomon Feferman & Gerhard Jäger - 1993 - Annals of Pure and Applied Logic 65 (3):243-263.
Systems of explicit mathematics with non-constructive μ-operator. Part II.Solomon Feferman & Gerhard Jäger - 1996 - Annals of Pure and Applied Logic 79 (1):37-52.
Reflections on reflections in explicit mathematics.Gerhard Jäger & Thomas Strahm - 2005 - Annals of Pure and Applied Logic 136 (1-2):116-133.
The [mathematical formula] quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals.Markus Marzetta & Thomas Strahm - 1997 - Archive for Mathematical Logic 36 (6):391-413.
The non-constructive μ operator, fixed point theories with ordinals, and the bar rule.Thomas Strahm - 2000 - Annals of Pure and Applied Logic 104 (1-3):305-324.
Realisability in weak systems of explicit mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
On power set in explicit mathematics.Thomas Glass - 1996 - Journal of Symbolic Logic 61 (2):468-489.
On the proof-theoretic strength of monotone induction in explicit mathematics.Thomas Glaß, Michael Rathjen & Andreas Schlüter - 1997 - Annals of Pure and Applied Logic 85 (1):1-46.
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.

Analytics

Added to PP
2014-01-16

Downloads
16 (#935,433)

6 months
20 (#139,007)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The unfolding of non-finitist arithmetic.Solomon Feferman & Thomas Strahm - 2000 - Annals of Pure and Applied Logic 104 (1-3):75-96.
The proof-theoretic analysis of Σ11 transfinite dependent choice.Christian Rüede - 2003 - Annals of Pure and Applied Logic 122 (1-3):195-234.
Universes over Frege structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.

View all 10 citations / Add more citations

References found in this work

Subsystems of Second Order Arithmetic.Stephen G. Simpson - 1999 - Studia Logica 77 (1):129-129.
A well-ordering proof for Feferman's theoryT 0.Gerhard Jäger - 1983 - Archive for Mathematical Logic 23 (1):65-77.

View all 15 references / Add more references