17 found
Order:
  1.  14
    Epsilon Substitution Method for Elementary Analysis.Grigori Mints, Sergei Tupailo & Wilfried Buchholz - 1996 - Archive for Mathematical Logic 35 (2):103-130.
    We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   20 citations  
  2.  60
    Notation Systems for Infinitary Derivations.Wilfried Buchholz - 1991 - Archive for Mathematical Logic 30 (5-6):277-296.
  3.  36
    A Uniform Approach to Fundamental Sequences and Hierarchies.Wilfried Buchholz, Adam Cichon & Andreas Weiermann - 1994 - Mathematical Logic Quarterly 40 (2):273-286.
    In this article we give a unifying approach to the theory of fundamental sequences and their related Hardy hierarchies of number-theoretic functions and we show the equivalence of the new approach with the classical one.
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  4.  11
    Refined Program Extraction From Classical Proofs.Ulrich Berger, Wilfried Buchholz & Helmut Schwichtenberg - 2002 - Annals of Pure and Applied Logic 114 (1-3):3-25.
    The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  5.  4
    Proof-Theoretic Analysis of Termination Proofs.Wilfried Buchholz - 1995 - Annals of Pure and Applied Logic 75 (1-2):57-65.
  6.  16
    Explaining the Gentzen–Takeuti Reduction Steps: A Second-Order System.Wilfried Buchholz - 2001 - Archive for Mathematical Logic 40 (4):255-272.
    Using the concept of notations for infinitary derivations we give an explanation of Takeuti's reduction steps on finite derivations (used in his consistency proof for Π1 1-CA) in terms of the more perspicious infinitary approach from [BS88].
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  7.  12
    An Independence Result for (II11-CA)+BI.Wilfried Buchholz - 1987 - Annals of Pure and Applied Logic 33 (2):131-155.
  8.  20
    Anton Setzer. Well-Ordering Proofs for Martin-Löf Type Theory. Annals of Pure and Applied Logic, Vol. 92 , Pp. 113–159.Wilfried Buchholz - 2000 - Bulletin of Symbolic Logic 6 (4):478-479.
  9.  4
    An Intuitionistic Fixed Point Theory.Wilfried Buchholz - 1997 - Archive for Mathematical Logic 37 (1):21-27.
    . In this article we prove that a certain intuitionistic version of the well-known fixed point theory \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\widehat{\rm ID}_1$\end{document} is conservative over \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\mbox{\sf HA}$\end{document} for almost negative formulas.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  10.  17
    Finitary Treatment of Operator Controlled Derivations.Wilfried Buchholz - 2001 - Mathematical Logic Quarterly 47 (3):363-396.
    By combining the methods of two former papers of ours we develop a finitary ordinal analysis of the axiom system KPi of Kripke-P atek set theory with an inaccessible universe. As a main result we obtain an upper bound for the provably recursive functions of KPi.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  4
    Preface.Wilfried Buchholz & Reinhard Kahle - 2005 - Annals of Pure and Applied Logic 133 (1-3):1.
  12.  5
    Heindorf Lutz. Elementare Beweistheorie. Wissenschaftsverlag B. I., Mannheim, Leipzig, Wien, und Zürich, 1994, 240 S.Wilfried Buchholz - 1996 - Journal of Symbolic Logic 61 (3):1051-1052.
    Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  13.  14
    Induktive Definitionen Und Dilatoren.Wilfried Buchholz - 1988 - Archive for Mathematical Logic 27 (1):51-60.
    In this paper we give a new and comparatively simple proof of the following theorem by Girard [1]:“If ∀x∈ ${\cal O}$ ∃y∈ ${\cal O}$ ψ(x,y) (where the relationψ is arithmetic and positive in Kleene's ${\cal O}$ ), then there exists a recursive DilatorD such that ∀α≧ω∀x∈ ${\cal O}$ <α∃y∈ ${\cal O}$ (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  14.  10
    A Term Calculus for (Co-) Recursive Definitions on Streamlike Data Structures.Wilfried Buchholz - 2005 - Annals of Pure and Applied Logic 136 (1):75-90.
    We introduce a system of simply typed lambda terms and show that a rather comprehensive class of recursion equations on streams or non-wellfounded trees can be solved in our system. Moreover certain conditions are presented which guarantee that the defined functionals are primitive recursive. As a major example we give a co-recursive treatment of Mints’ continuous cut-elimination operator.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  15.  6
    Review: W. A. Howard, A System of Abstract Constructive Ordinals. [REVIEW]Wilfried Buchholz - 1985 - Journal of Symbolic Logic 50 (1):243-244.
  16.  1
    W. A. Howard. A System of Abstract Constructive Ordinals. The Journal of Symbolic Logic, Vol. 37 , Pp. 355–374.Wilfried Buchholz - 1985 - Journal of Symbolic Logic 50 (1):243-244.
  17.  6
    Notation Systems for Infinitary Derivations.Wilfried Buchholz & Sergei Tupailo - 2002 - Bulletin of Symbolic Logic 8 (3):437-439.