12 found
Order:
  1. The Provably Terminating Operations of the Subsystem of Explicit Mathematics.Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (11):934-947.
    In Spescha and Strahm [15], a system of explicit mathematics in the style of Feferman [6] and [7] is introduced, and in Spescha and Strahm [16] the addition of the join principle to is studied. Changing to intuitionistic logic, it could be shown that the provably terminating operations of are the polytime functions on binary words. However, although strongly conjectured, it remained open whether the same holds true for the corresponding theory with classical logic. This note supplements a proof of (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  2.  29
    The Proof-Theoretic Analysis of Transfinitely Iterated Quasi Least Fixed Points.Dieter Probst - 2006 - Journal of Symbolic Logic 71 (3):721 - 746.
    The starting point of this article is an old question asked by Feferman in his paper on Hancock's conjecture [6] about the strength of ${\rm ID}_{1}^{\ast}$. This theory is obtained from the well-known theory ID₁ by restricting fixed point induction to formulas that contain fixed point constants only positively. The techniques used to perform the proof-theoretic analysis of ${\rm ID}_{1}^{\ast}$ also permit to analyze its transfinitely iterated variants ${\rm ID}_{\alpha}^{\ast}$. Thus, we eventually know that $|\widehat{{\rm ID}}_{\alpha}|=|{\rm ID}_{\alpha}^{\ast}|$.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  3.  21
    The Suslin Operator in Applicative Theories: Its Proof-Theoretic Analysis Via Ordinal Theories.Gerhard Jäger & Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (8):647-660.
    The Suslin operator is a type-2 functional testing for the well-foundedness of binary relations on the natural numbers. In the context of applicative theories, its proof-theoretic strength has been analyzed in Jäger and Strahm [18]. This article provides a more direct approach to the computation of the upper bounds in question. Several theories featuring the Suslin operator are embedded into ordinal theories tailored for dealing with non-monotone inductive definitions that enable a smooth definition of the application relation.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  4.  38
    On the Relationship Between Fixed Points and Iteration in Admissible Set Theory Without Foundation.Dieter Probst - 2005 - Archive for Mathematical Logic 44 (5):561-580.
    In this article we show how to use the result in Jäger and Probst [7] to adapt the technique of pseudo-hierarchies and its use in Avigad [1] to subsystems of set theory without foundation. We prove that the theory KPi0 of admissible sets without foundation, extended by the principle (Σ-FP), asserting the existence of fixed points of monotone Σ operators, has the same proof-theoretic ordinal as KPi0 extended by the principle (Σ-TR), that allows to iterate Σ operations along ordinals. By (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  56
    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 (7 more)  
     
    Export citation  
     
    Bookmark  
  6.  18
    On Contraction and the Modal Fragment.Kai Brünnler, Dieter Probst & Thomas Studer - 2008 - Mathematical Logic Quarterly 54 (4):345-349.
    We observe that removing contraction from a standard sequent calculus for first-order predicate logic preserves completeness for the modal fragment.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  7.  10
    Corrigendum to “Variation on a Theme of Schütte”.Gerhard Jäger & Dieter Probst - 2005 - Mathematical Logic Quarterly 51 (6):642-642.
    We give a corrected definition for the paper [1] mentioned in the title.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  8.  5
    Contents.Peter Schuster & Dieter Probst - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter.
    Direct download  
     
    Export citation  
     
    Bookmark  
  9.  4
    Frontmatter.Peter Schuster & Dieter Probst - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  10.  4
    Introduction.Peter Schuster & Dieter Probst - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter. pp. 1-4.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  11.  4
    Preface.Peter Schuster & Dieter Probst - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter.
    Direct download  
     
    Export citation  
     
    Bookmark  
  12. Concepts of Proof in Mathematics, Philosophy, and Computer Science.Peter Schuster & Dieter Probst (eds.) - 2016 - De Gruyter.
     
    Export citation  
     
    Bookmark