Switch to: References

Add citations

You must login to add citations.
  1. Wellordering proofs for metapredicative Mahlo.Thomas Strahm - 2002 - Journal of Symbolic Logic 67 (1):260-278.
    In this article we provide wellordering proofs for metapredicative systems of explicit mathematics and admissible set theory featuring suitable axioms about the Mahloness of the underlying universe of discourse. In particular, it is shown that in the corresponding theories EMA of explicit mathematics and KPm 0 of admissible set theory, transfinite induction along initial segments of the ordinal φω00, for φ being a ternary Veblen function, is derivable. This reveals that the upper bounds given for these two systems in the (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • The strength of Martin-Löf type theory with a superuniverse. Part I.Michael Rathjen - 2000 - Archive for Mathematical Logic 39 (1):1-39.
    Universes of types were introduced into constructive type theory by Martin-Löf [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say $\mathcal{C}$ . The universe then “reflects” $\mathcal{C}$ .This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]).It is proved that Martin-Löf type theory (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Universes over Frege structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.
    In this paper, we study a concept of universe for a truth predicate over applicative theories. A proof-theoretic analysis is given by use of transfinitely iterated fixed point theories . The lower bound is obtained by a syntactical interpretation of these theories. Thus, universes over Frege structures represent a syntactically expressive framework of metapredicative theories in the context of applicative theories.
    Download  
     
    Export citation  
     
    Bookmark   5 citations