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

Links

PhilArchive



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

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

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.
Explicit mathematics with the monotone fixed point principle.Michael Rathjen - 1998 - Journal of Symbolic Logic 63 (2):509-542.
Explicit mathematics with the monotone fixed point principle. II: Models.Michael Rathjen - 1999 - Journal of Symbolic Logic 64 (2):517-550.
Review: Solomon Feferman, J. N. Crossley, A Language and Axioms for Explicit Mathematics; Solomon Feferman, Maurice Boffa, Dirk van Dalen, Kenneth McAloon, Constructive Theories of Functions and Classes. [REVIEW]G. R. Renardel de Lavalette & A. S. Troelstra - 1984 - Journal of Symbolic Logic 49 (1):308-311.
Relating Quine's NF to Feferman's EM.Andrea Cantini - 1999 - Studia Logica 62 (2):141-162.
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.
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.
In the Light of Logic.Solomon Feferman - 1998 - New York and Oxford: Oxford University Press.
Monotone inductive definitions in explicit mathematics.Michael Rathjen - 1996 - Journal of Symbolic Logic 61 (1):125-146.
A theory of rules for enumerated classes of functions.Andreas Schlüter - 1995 - Archive for Mathematical Logic 34 (1):47-63.
Power types in explicit mathematics?Gerhard Jäger - 1997 - Journal of Symbolic Logic 62 (4):1142-1146.
What rests on what? The proof-theoretic analysis of mathematics.Solomon Feferman - 1993 - In J. Czermak (ed.), Philosophy of Mathematics. Hölder-Pichler-Tempsky. pp. 1--147.
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.

Analytics

Added to PP
2014-01-16

Downloads
10 (#1,194,153)

6 months
3 (#976,418)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

On power set in explicit mathematics.Thomas Glass - 1996 - Journal of Symbolic Logic 61 (2):468-489.
Universes over Frege structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.

View all 7 citations / Add more citations

References found in this work

Proof theory.Gaisi Takeuti - 1976 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Proof theory.K. Schütte - 1977 - New York: Springer Verlag.
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