Order:
  1.  48
    The proof-theoretic analysis of transfinitely iterated fixed point theories.Gerhard JÄger, Reinhard Kahle, Anton Setzer & Thomas Strahm - 1999 - Journal of Symbolic Logic 64 (1):53-67.
    This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{ the exact proof-theoretic ordinals of these systems are presented.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   22 citations  
  2. The Proof-Theoretic Analysis of Transfinitely Iterated Fixed Point Theories.Gerhard Jager, Reinhard Kahle, Anton Setzer & Thomas Strahm - 1999 - Journal of Symbolic Logic 64 (1):53-67.
    This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{<\alpha};$ the exact proof-theoretic ordinals of these systems are presented.
     
    Export citation  
     
    Bookmark   12 citations  
  3.  68
    Extending Martin-Löf Type Theory by one Mahlo-universe.Anton Setzer - 2000 - Archive for Mathematical Logic 39 (3):155-181.
    We define a type theory MLM, which has proof theoretical strength slightly greater then Rathjen's theory KPM. This is achieved by replacing the universe in Martin-Löf's Type Theory by a new universe V having the property that for every function f, mapping families of sets in V to families of sets in V, there exists a universe inside V closed under f. We show that the proof theoretical strength of MLM is $\geq \psi_{\Omega_1}\Omega_{{\rm M}+\omega}$ . This is slightly greater than (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  4.  38
    Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
    We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, of the version à (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  5.  58
    Induction–recursion and initial algebras.Peter Dybjer & Anton Setzer - 2003 - Annals of Pure and Applied Logic 124 (1-3):1-47.
    Induction–recursion is a powerful definition method in intuitionistic type theory. It extends inductive definitions and allows us to define all standard sets of Martin-Löf type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive–recursive definitions by modeling them as initial algebras in slice categories. (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  8
    An Extended Predicative Definition of the Mahlo Universe.Reinhard Kahle & Anton Setzer - 2010 - In Ralf Schindler (ed.), Ways of Proof Theory. De Gruyter. pp. 315-340.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  7.  23
    Hindley J. Roger. Basic simple type theory. Cambridge tracts in theoretical computer science, no. 42. Cambridge University Press, Cambridge, New York, and Oakleigh, Victoria, 1997, xi + 186 pp. [REVIEW]Anton Setzer - 1999 - Journal of Symbolic Logic 64 (4):1832-1833.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  8.  15
    Review: J. Roger Hindley, Basic Simple Type Theory. [REVIEW]Anton Setzer - 1999 - Journal of Symbolic Logic 64 (4):1832-1833.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark