Switch to: Citations

Add references

You must login to add references.
  1. Bezem, M., see Barendsen, E.G. M. Bierman, M. DZamonja, S. Shelah, S. Feferman, G. Jiiger, M. A. Jahn, S. Lempp, Sui Yuefei, S. D. Leonhardi & D. Macpherson - 1996 - Annals of Pure and Applied Logic 79 (1):317.
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   3 citations  
  • Understanding Uniformity in Feferman's Explicit Mathematics.Thomas Glaß - 1995 - Annals of Pure and Applied Logic 75 (1-2):89-106.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • Monotone Inductive Definitions in a Constructive Theory of Functions and Classes.Shuzo Takahashi - 1989 - Annals of Pure and Applied Logic 42 (3):255-297.
    In this thesis, we study the least fixed point principle in a constructive setting. A constructive theory of functions and sets has been developed by Feferman. This theory deals both with sets and with functions over sets as independent notions. In the language of Feferman's theory, we are able to formulate the least fixed point principle for monotone inductive definitions as: every operation on classes to classes which satisfies the monotonicity condition has a least fixed point. This is called the (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  • The Strength of Some Martin-Löf Type Theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
    One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with Δ 2 1 comprehension and bar induction. As Martin-Löf intended to formulate a system of constructive (intuitionistic) mathematics that has a sound philosophical basis, this yields a constructive consistency proof of a (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   35 citations  
  • Subsystems of Second-Order Arithmetic.Stephen G. Simpson - 2004 - Studia Logica 77 (1):129-129.
     
    Export citation  
     
    Bookmark   96 citations