Understanding uniformity in Feferman's explicit mathematics

Annals of Pure and Applied Logic 75 (1-2):89-106 (1995)
  Copy   BIBTEX

Abstract

The aim of this paper is the analysis of uniformity in Feferman's explicit mathematics. The proof-strength of those systems for constructive mathematics is determined by reductions to subsystems of second-order arithmetic: If uniformity is absent, the method of standard structures yields that the strength of the join axiom collapses. Systems with uniformity and join are treated via cut elimination and asymmetrical interpretations in standard structures.

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(94)00058-b

Other Versions

No versions found

Links

PhilArchive

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

Systems of explicit mathematics with non-constructive μ-operator and join.Thomas Glaß & Thomas Strahm - 1996 - Annals of Pure and Applied Logic 82 (2):193-219.
On power set in explicit mathematics.Thomas Glass - 1996 - Journal of Symbolic Logic 61 (2):468-489.
Realisability in weak systems of explicit mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
Proof Theory of Constructive Systems: Inductive Types and Univalence.Michael Rathjen - 2017 - In Gerhard Jäger & Wilfried Sieg, Feferman on Foundations: Logic, Mathematics, Philosophy. Cham: Springer. pp. 385-419.
Explicit mathematics with the monotone fixed point principle.Michael Rathjen - 1998 - Journal of Symbolic Logic 63 (2):509-542.
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.
Universes in explicit mathematics.Gerhard Jäger, Reinhard Kahle & Thomas Studer - 2001 - Annals of Pure and Applied Logic 109 (3):141-162.
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.
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.
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.

Analytics

Added to PP
2014-01-16

Downloads
73 (#803,521)

6 months
4 (#1,750,773)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Universes over Frege structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.
On power set in explicit mathematics.Thomas Glass - 1996 - Journal of Symbolic Logic 61 (2):468-489.
A theory of rules for enumerated classes of functions.Andreas Schlüter - 1995 - Archive for Mathematical Logic 34 (1):47-63.

View all 7 citations / Add more citations

References found in this work

Proof theory.K. Schütte - 1977 - New York: Springer Verlag.
Proof theory.Gaisi Takeuti - 1987 - Mineola, New York: Dover Publications.
Partial realizations of Hilbert's program.Stephen G. Simpson - 1988 - Journal of Symbolic Logic 53 (2):349-363.

View all 9 references / Add more references