25 found
Sort by:
  1. Dieter Probst & Thomas Strahm (2011). Admissible Closures of Polynomial Time Computable Arithmetic. Archive for Mathematical Logic 50 (5-6):643-660.
    We propose two admissible closures ${\mathbb{A}({\sf PTCA})}$ and ${\mathbb{A}({\sf PHCA})}$ of Ferreira’s system PTCA of polynomial time computable arithmetic and of full bounded arithmetic (or polynomial hierarchy computable arithmetic) PHCA. The main results obtained are: (i) ${\mathbb{A}({\sf PTCA})}$ is conservative over PTCA with respect to ${\forall\exists\Sigma^b_1}$ sentences, and (ii) ${\mathbb{A}({\sf PHCA})}$ is conservative over full bounded arithmetic PHCA for ${\forall\exists\Sigma^b_{\infty}}$ sentences. This yields that (i) the ${\Sigma^b_1}$ definable functions of ${\mathbb{A}({\sf PTCA})}$ are the polytime functions, and (ii) the ${\Sigma^b_{\infty}}$ definable (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. Daria Spescha & Thomas Strahm (2011). Realisability in Weak Systems of Explicit Mathematics. Mathematical Logic Quarterly 57 (6):551-565.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  3. Solomon Feferman & Thomas Strahm (2010). Unfolding Finitist Arithmetic. Review of Symbolic Logic 3 (4):665-689.
    The concept of the (full) unfolding of a schematic system is used to answer the following question: Which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted ? The program to determine for various systems of foundational significance was previously carried out for a system of nonfinitist arithmetic, ; it was shown that is proof-theoretically equivalent to predicative analysis. In the present paper we work out the unfolding notions for a basic schematic system (...)
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  4. Daria Spescha & Thomas Strahm (2009). Elementary Explicit Types and Polynomial Time Operations. Mathematical Logic Quarterly 55 (3):245-258.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  5. Thomas Strahm (2008). Introduction. Dialectica 62 (2):145–147.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  6. David Steiner & Thomas Strahm (2006). On the Proof Theory of Type Two Functionals Based on Primitive Recursive Operations. Mathematical Logic Quarterly 52 (3):237-252.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  7. Gerhard Jäger & Thomas Strahm (2005). Reflections on Reflections in Explicit Mathematics. Annals of Pure and Applied Logic 136 (1-2):116-133.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  8. Thomas Strahm (2003). Tupailo Sergei. Realization of Analysis Into Explicit Mathematics. The Journal of Symbolic Logic, Vol. 66 (2001), Pp. 1848–1864. [REVIEW] Bulletin of Symbolic Logic 9 (1):42-43.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  9. Christian Rüede & Thomas Strahm (2002). Intuitionistic Fixed Point Theories for Strictly Positive Operators. Mathematical Logic Quarterly 48 (2):195-202.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  10. Thomas Strahm (2002). Wellordering Proofs for Metapredicative Mahlo. 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 (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  11. Thomas Strahm (2002). Review: Andreas Weiermann, How Is It That Infinitary Methods Can Be Applied to Finitary Mathematics? Gödel's T: A Case Study. [REVIEW] Bulletin of Symbolic Logic 8 (3):435-436.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  12. Gerhard Jäger & Thomas Strahm (2001). Upper Bounds for Metapredicative Mahlo in Explicit Mathematics and Admissible Set Theory. Journal of Symbolic Logic 66 (2):935-958.
    In this article we introduce systems for metapredicative Mahlo in explicit mathematics and admissible set theory. The exact upper proof-theoretic bounds of these systems are established.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  13. Solomon Feferman & Thomas Strahm (2000). The Unfolding of Non-Finitist Arithmetic. Annals of Pure and Applied Logic 104 (1-3):75-96.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  14. Gerhard Jäger & Thomas Strahm (2000). Fixed Point Theories and Dependent Choice. Archive for Mathematical Logic 39 (7):493-508.
    In this paper we establish the proof-theoretic equivalence of (i) $\hbox {\sf ATR}$ and $\widehat{\hbox{\sf ID}}_{\omega}$ , (ii) $\hbox{\sf ATR}_0+ (\Sigma^1_1-\hbox{\sf DC})$ and $\widehat{\hbox {\sf ID}}_{<\omega^\omega} , and (iii) $\hbox {\sf ATR}+(\Sigma^1_1-\hbox{\sf DC})$ and $\widehat{\hbox {\sf ID}}_{<\varepsilon_0} $.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  15. Thomas Strahm (2000). The Non-Constructive Operator, Fixed Point Theories with Ordinals, and the Bar Rule. Annals of Pure and Applied Logic 104 (1-3):305-324.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  16. Gerhard Jäger, Reinhard Kahle, Anton Setzer & Thomas Strahm (1999). The Proof-Theoretic Analysis of Transfinitely Iterated Fixed Point Theories. 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 (6 more)  
     
    My bibliography  
     
    Export citation  
  17. Gerhard Jäger & Thomas Strahm (1999). Bar Induction and Ω Model Reflection. Annals of Pure and Applied Logic 97 (1-3):221-230.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  18. Thomas Strahm (1998). Review: Andrea Cantini, Logical Frameworks for Truth and Abstraction. An Axiomatic Study. [REVIEW] Journal of Symbolic Logic 63 (1):328-329.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  19. Markus Marzetta & Thomas Strahm (1997). The [Mathematical Formula] Quantification Operator in Explicit Mathematics with Universes and Iterated Fixed Point Theories with Ordinals. Archive for Mathematical Logic 5 (5-6):391-413.
    This paper is about two topics: 1. systems of explicit mathematics with universes and a non-constructive quantification operator $\mu$; 2. iterated fixed point theories with ordinals. We give a proof-theoretic treatment of both families of theories; in particular, ordinal theories are used to get upper bounds for explicit theories with finitely many universes.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  20. Thomas Strahm (1997). Polynomial Time Operations in Explicit Mathematics. Journal of Symbolic Logic 62 (2):575-594.
    In this paper we study (self)-applicative theories of operations and binary words in the context of polynomial time computability. We propose a first order theory PTO which allows full self-application and whose provably total functions on W = {0, 1} * are exactly the polynomial time computable functions. Our treatment of PTO is proof-theoretic and very much in the spirit of reductive proof theory.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  21. Thomas Glaß & Thomas Strahm (1996). Systems of Explicit Mathematics with Non-Constructive Μ-Operator and Join. Annals of Pure and Applied Logic 82 (2):193-219.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  22. Gerhard Jager & Thomas Strahm (1996). Some Theories with Positive Induction of Ordinal Strength $Varphiomega 0$. Journal of Symbolic Logic 61 (3):818-842.
    This paper deals with: (i) the theory $\mathrm{ID}^{\tt\#}_1$ which results from $\widehat{\mathrm{ID}}_1$ by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory $\mathrm{BON}(\mu)$ plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are $\Sigma$ in the ordinals. We show that these systems have proof-theoretic strength $\varphi\omega 0$.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  23. Gerhard Jäger & Thomas Strahm (1996). Some Theories with Positive Induction of Ordinal Strength Φω. Journal of Symbolic Logic 61 (3):818-842.
    This paper deals with: (i) the theory ID # 1 which results from $\widehat{\mathrm{ID}}_1$ by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory BON(μ) plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are Σ in the ordinals. We show that these systems have proof-theoretic strength φω 0.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  24. Gerhard Jäger & Thomas Strahm (1995). Second Order Theories with Ordinals and Elementary Comprehension. Archive for Mathematical Logic 34 (6):345-375.
    We study elementary second order extensions of the theoryID 1 of non-iterated inductive definitions and the theoryPA Ω of Peano arithmetic with ordinals. We determine the exact proof-theoretic strength of those extensions and their natural subsystems, and we relate them to subsystems of analysis with arithmetic comprehension plusΠ 1 1 comprehension and bar induction without set parameters.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  25. Gerhard Jäger & Thomas Strahm (1995). Totality in Applicative Theories. Annals of Pure and Applied Logic 74 (2):105-120.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation