28 found
Sort by:
  1. Florian Ranzi & Thomas Strahm (2014). A Note on the Theory SID<Ω of Stratified Induction. Mathematical Logic Quarterly 60 (6):487-497.
  2. 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 (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Daria Spescha & Thomas Strahm (2011). Realisability in Weak Systems of Explicit Mathematics. Mathematical Logic Quarterly 57 (6):551-565.
    This paper is a direct successor to 12. Its aim is to introduce a new realisability interpretation for weak systems of explicit mathematics and use it in order to analyze extensions of the theory PET in 12 by the so-called join axiom of explicit mathematics.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  4. 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 (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  5. Daria Spescha & Thomas Strahm (2009). Elementary Explicit Types and Polynomial Time Operations. Mathematical Logic Quarterly 55 (3):245-258.
    This paper studies systems of explicit mathematics as introduced by Feferman [9, 11]. In particular, we propose weak explicit type systems with a restricted form of elementary comprehension whose provably terminating operations coincide with the functions on binary words that are computable in polynomial time. The systems considered are natural extensions of the first-order applicative theories introduced in Strahm [19, 20].
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  6. Thomas Strahm (2008). Introduction. Dialectica 62 (2):145–147.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  7. 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.
    This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of the two subsystems of (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  8. Gerhard Jäger & Thomas Strahm (2005). Reflections on Reflections in Explicit Mathematics. Annals of Pure and Applied Logic 136 (1-2):116-133.
    We give a broad discussion of reflection principles in explicit mathematics, thereby addressing various kinds of universe existence principles. The proof-theoretic strength of the relevant systems of explicit mathematics is couched in terms of suitable extensions of Kripke–Platek set theory.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  9. Thomas Strahm (2003). Realization of Analysis Into Explicit Mathematics. [REVIEW] Bulletin of Symbolic Logic 9 (1):42-42.
     
    My bibliography  
     
    Export citation  
  10. 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.
    Direct download  
     
    My bibliography  
     
    Export citation  
  11. Christian Rüede & Thomas Strahm (2002). Intuitionistic Fixed Point Theories for Strictly Positive Operators. Mathematical Logic Quarterly 48 (2):195-202.
    In this paper it is shown that the intuitionistic .xed point theory equation image for α times iterated fixed points of strictly positive operator forms is conservative for negative arithmetic and equation image sentences over the theory equation image for α times iterated arithmetic comprehension without set parameters.This generalizes results previously due to Buchholz [5] and Arai [2].
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  12. Thomas Strahm (2002). How Is It That Infinitary Methods Can Be Applied To Finitary Mathematics? [REVIEW] Bulletin of Symbolic Logic 8 (3):435-435.
     
    My bibliography  
     
    Export citation  
  13. 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  
  14. 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  
  15. 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  
  16. Solomon Feferman & Thomas Strahm (2000). The Unfolding of Non-Finitist Arithmetic. Annals of Pure and Applied Logic 104 (1-3):75-96.
    The unfolding of schematic formal systems is a novel concept which was initiated in Feferman , Gödel ’96, Lecture Notes in Logic, Springer, Berlin, 1996, pp. 3–22). This paper is mainly concerned with the proof-theoretic analysis of various unfolding systems for non-finitist arithmetic . In particular, we examine two restricted unfoldings and , as well as a full unfolding, . The principal results then state: is equivalent to ; is equivalent to ; is equivalent to . Thus is proof-theoretically equivalent (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  17. 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} $.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  18. 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.
    This paper deals with the proof theory of first-order applicative theories with non-constructive μ operator and a form of the bar rule, yielding systems of ordinal strength Γ0 and 20, respectively. Relevant use is made of fixed-point theories with ordinals plus bar rule.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  19. 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  
  20. Gerhard Jäger & Thomas Strahm (1999). Bar Induction and Ω Model Reflection. Annals of Pure and Applied Logic 97 (1-3):221-230.
    We show that the principle of ω model reflection for Π1n − 1 formulas is equivalent over ACA0 to the scheme of Π1n bar induction. This extends and refines previous results of Friedman and Simpson.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  21. 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 (3 more)  
     
    My bibliography  
     
    Export citation  
  22. 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  
  23. 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  
  24. 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.
    The aim of this article is to give the proof-theoretic analysis of various subsystems of Feferman's theory T1 for explicit mathematics which contain the non-constructive μ-operator and join. We make use of standard proof-theoretic techniques such as cut-elimination of appropriate semiformal systems and asymmetrical interpretations in standard structures for explicit mathematics.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  25. 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 (3 more)  
     
    My bibliography  
     
    Export citation  
  26. 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  
  27. 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.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  28. Gerhard Jäger & Thomas Strahm (1995). Totality in Applicative Theories. Annals of Pure and Applied Logic 74 (2):105-120.
    In this paper we study applicative theories of operations and numbers with the non-constructive minimum operator in the context of a total application operation. We determine the proof-theoretic strength of such theories by relating them to well-known systems like Peano Arithmetic PA and the system <0 of second order arithmetic. Essential use will be made of so-called fixed-point theories with ordinals, certain infinitary term models and Church-Rosser properties.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation