44 found
Order:
  1.  15
    Upper Bounds for Metapredicative Mahlo in Explicit Mathematics and Admissible Set Theory.Gerhard Jäger & Thomas Strahm - 2001 - 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 (7 more)  
     
    Export citation  
     
    My bibliography   13 citations  
  2.  14
    The Unfolding of Non-Finitist Arithmetic.Solomon Feferman & Thomas Strahm - 2000 - 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)  
     
    Export citation  
     
    My bibliography   10 citations  
  3.  2
    Elementary Explicit Types and Polynomial Time Operations.Daria Spescha & Thomas Strahm - 2009 - 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)  
     
    Export citation  
     
    My bibliography   5 citations  
  4. Polynomial Time Operations in Explicit Mathematics.Thomas Strahm - 1997 - 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 (9 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  5.  10
    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  
     
    My bibliography   9 citations  
  6.  8
    Totality in Applicative Theories.Gerhard Jäger & Thomas Strahm - 1995 - 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)  
     
    Export citation  
     
    My bibliography   9 citations  
  7.  10
    Second Order Theories with Ordinals and Elementary Comprehension.Gerhard Jäger & Thomas Strahm - 1995 - 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)  
     
    Export citation  
     
    My bibliography   7 citations  
  8. Unfolding Feasible Arithmetic andWeak Truth.Thomas Strahm & Sebastian Eberhard - 2015 - In Kentaro Fujimoto, José Martínez Fernández, Henri Galinon & Theodora Achourioti (eds.), Unifying the Philosophy of Truth. Springer Verlag.
     
    Export citation  
     
    My bibliography   1 citation  
  9.  28
    Unfolding Finitist Arithmetic.Solomon Feferman & Thomas Strahm - 2010 - 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)  
     
    Export citation  
     
    My bibliography   2 citations  
  10.  1
    Reflections on Reflections in Explicit Mathematics.Gerhard Jäger & Thomas Strahm - 2005 - 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)  
     
    Export citation  
     
    My bibliography   4 citations  
  11.  8
    Realisability in Weak Systems of Explicit Mathematics.Daria Spescha & Thomas Strahm - 2011 - 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 (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  12.  16
    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 (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  13.  2
    First Steps Into Metapredicativity in Explicit Mathematics.Thomas Strahm, S. Barry Cooper & John K. Truss - 2002 - Bulletin of Symbolic Logic 8 (4):535-536.
  14.  8
    Fixed Point Theories and Dependent Choice.Gerhard Jäger & Thomas Strahm - 2000 - 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)  
     
    Export citation  
     
    My bibliography   4 citations  
  15.  1
    Systems of Explicit Mathematics with Non-Constructive Μ-Operator and Join.Thomas Glaß & Thomas Strahm - 1996 - 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)  
     
    Export citation  
     
    My bibliography   5 citations  
  16.  9
    Some Theories with Positive Induction of Ordinal Strength Φω.Gerhard Jäger & Thomas Strahm - 1996 - 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 (5 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  17.  6
    The [Mathematical Formula] Quantification Operator in Explicit Mathematics with Universes and Iterated Fixed Point Theories with Ordinals.Markus Marzetta & Thomas Strahm - 1997 - 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.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  18. The $\Mu$ Quantification Operator in Explicit Mathematics with Universes and Iterated Fixed Point Theories with Ordinals.Markus Marzetta & Thomas Strahm - 1998 - Archive for Mathematical Logic 37 (5):391-413.
    No categories
    Direct download  
     
    Export citation  
     
    My bibliography   3 citations  
  19.  4
    Bar Induction and Ω Model Reflection.Gerhard Jäger & Thomas Strahm - 1999 - 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)  
     
    Export citation  
     
    My bibliography   2 citations  
  20.  1
    The Non-Constructive Μ Operator, Fixed Point Theories with Ordinals, and the Bar Rule.Thomas Strahm - 2000 - 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)  
     
    Export citation  
     
    My bibliography   2 citations  
  21.  37
    Admissible Closures of Polynomial Time Computable Arithmetic.Dieter Probst & Thomas Strahm - 2011 - 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)  
     
    Export citation  
     
    My bibliography  
  22.  5
    Intuitionistic Fixed Point Theories for Strictly Positive Operators.Christian Rüede & Thomas Strahm - 2002 - 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 (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  23.  13
    Theories of Proof-Theoretic Strength Ψ.Thomas Strahm, Gerhard Jäger & Ulrik Buchholtz - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter. pp. 115-140.
    Direct download  
     
    Export citation  
     
    My bibliography  
  24.  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.
    Direct download  
     
    Export citation  
     
    My bibliography   1 citation  
  25.  3
    Katalin Bimbó. Proof Theory: Sequent Calculi and Related Formalisms. CRC Press, Boca Raton, 2014, X + 374 Pp. [REVIEW]Thomas Strahm - 2016 - Bulletin of Symbolic Logic 22 (2):288-289.
    Direct download  
     
    Export citation  
     
    My bibliography  
  26. Autonomous Fixed Point Progressions and Fixed Point Transfinite Recursion.Thomas Strahm - 2001 - Bulletin of Symbolic Logic 7 (4):535-536.
    Direct download  
     
    Export citation  
     
    My bibliography   1 citation  
  27.  4
    On the Proof Theory of Type Two Functionals Based on Primitive Recursive Operations.David Steiner & Thomas Strahm - 2006 - 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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  28.  3
    A Note on the Theory SID<Ω of Stratified Induction.Florian Ranzi & Thomas Strahm - 2014 - Mathematical Logic Quarterly 60 (6):487-497.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  29.  7
    Introduction.Thomas Strahm - 2008 - Dialectica 62 (2):145–147.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  30.  3
    Review: Andrea Cantini, Logical Frameworks for Truth and Abstraction. An Axiomatic Study. [REVIEW]Thomas Strahm - 1998 - Journal of Symbolic Logic 63 (1):328-329.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  31.  1
    Upper Bounds for Metapredicative Mahlo in Explicit Mathematics and Admissible Set Theory.Gerhard Jager & Thomas Strahm - 2001 - 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  
     
    Export citation  
     
    My bibliography  
  32.  2
    Tupailo Sergei. Realization of Analysis Into Explicit Mathematics. The Journal of Symbolic Logic, Vol. 66 (2001), Pp. 1848–1864. [REVIEW]Thomas Strahm - 2003 - Bulletin of Symbolic Logic 9 (1):42-43.
    Direct download  
     
    Export citation  
     
    My bibliography  
  33.  1
    Cantini Andrea. Logical Frameworks for Truth and Abstraction. An Axiomatic Study. Studies in Logic and the Foundations of Mathematics, Vol. 135. Elsevier, Amsterdam Etc. 1996, Xii + 461 Pp. [REVIEW]Thomas Strahm - 1998 - Journal of Symbolic Logic 63 (1):328-329.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  34.  3
    Review: Andreas Weiermann, How Is It That Infinitary Methods Can Be Applied to Finitary Mathematics? Gödel's T: A Case Study. [REVIEW]Thomas Strahm - 2002 - Bulletin of Symbolic Logic 8 (3):435-436.
  35.  1
    Some Theories with Positive Induction of Ordinal Strength $Varphiomega 0$.Gerhard Jager & Thomas Strahm - 1996 - 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)  
     
    Export citation  
     
    My bibliography  
  36. Polynomial Time Operations in Explicit MathematicsFeasible Operations and Applicative Theories Based on Λη.Fernando Ferreira, Thomas Strahm & Andrea Cantini - 2002 - Bulletin of Symbolic Logic 8 (4):534.
  37. How Is It That Infinitary Methods Can Be Applied To Finitary Mathematics? [REVIEW]Thomas Strahm - 2002 - Bulletin of Symbolic Logic 8 (3):435-435.
  38. Introduction.Thomas Strahm - 2008 - Dialectica 62 (2):145-147.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  39. Polynomial Time Operations in Explicit Mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
    In this paper we study -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 $\mathbb{W} = \{0, 1\}^\ast$ 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  
     
    Export citation  
     
    My bibliography  
  40. Polynomial Time Operations in Explicit Mathematics.Thomas Strahm & Andrea Cantini - 2002 - Bulletin of Symbolic Logic 8 (4):534-535.
    Direct download  
     
    Export citation  
     
    My bibliography  
  41. Realization of Analysis Into Explicit Mathematics. [REVIEW]Thomas Strahm - 2003 - Bulletin of Symbolic Logic 9 (1):42-42.
  42. The Journal of Symbolic Logic.Thomas Strahm - 2003 - Bulletin of Symbolic Logic 9 (1):42-43.
  43. Weiermann Andreas. How is It That Infinitary Methods Can Be Applied to Finitary Mathematics? Gödel's T: A Case Study. The Journal of Symbolic Logic, Vol. 63 , Pp. 1348–1370. [REVIEW]Thomas Strahm - 2002 - Bulletin of Symbolic Logic 8 (3):435-436.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  44. Wellordering Proofs for Metapredicative Mahlo.Thomas Strahm - 2002 - Journal of Symbolic Logic 67 (1):260-278.
    Direct download  
     
    Export citation  
     
    My bibliography