Switch to: References

Add citations

You must login to add citations.
  1. Mass problems and randomness.Stephen G. Simpson - 2005 - Bulletin of Symbolic Logic 11 (1):1-27.
    A mass problem is a set of Turing oracles. If P and Q are mass problems, we say that P is weakly reducible to Q if every member of Q Turing computes a member of P. We say that P is strongly reducible to Q if every member of Q Turing computes a member of P via a fixed Turing functional. The weak degrees and strong degrees are the equivalence classes of mass problems under weak and strong reducibility, respectively. We (...)
    Download  
     
    Export citation  
     
    Bookmark   28 citations  
  • Transfinite induction within Peano arithmetic.Richard Sommer - 1995 - Annals of Pure and Applied Logic 76 (3):231-289.
    The relative strengths of first-order theories axiomatized by transfinite induction, for ordinals less-than 0, and formulas restricted in quantifier complexity, is determined. This is done, in part, by describing the provably recursive functions of such theories. Upper bounds for the provably recursive functions are obtained using model-theoretic techniques. A variety of additional results that come as an application of such techniques are mentioned.
    Download  
     
    Export citation  
     
    Bookmark   24 citations  
  • Herbrand analyses.Wilfried Sieg - 1991 - Archive for Mathematical Logic 30 (5-6):409-441.
    Herbrand's Theorem, in the form of $$\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\exists } $$ -inversion lemmata for finitary and infinitary sequent calculi, is the crucial tool for the determination of the provably total function(al)s of a variety of theories. The theories are (second order extensions of) fragments of classical arithmetic; the classes of provably total functions include the elements of the Polynomial Hierarchy, the Grzegorczyk Hierarchy, and the extended Grzegorczyk Hierarchy $\mathfrak{E}^\alpha $ , α < ε0. A subsidiary aim of the paper is to show (...)
    Download  
     
    Export citation  
     
    Bookmark   22 citations  
  • Proof theory and ordinal analysis.W. Pohlers - 1991 - Archive for Mathematical Logic 30 (5-6):311-376.
    In the first part we show why ordinals and ordinal notations are naturally connected with proof theoretical research. We introduce the program of ordinal analysis. The second part gives examples of applications of ordinal analysis.
    Download  
     
    Export citation  
     
    Bookmark   20 citations  
  • A model-theoretic approach to ordinal analysis.Jeremy Avigad & Richard Sommer - 1997 - Bulletin of Symbolic Logic 3 (1):17-52.
    We describe a model-theoretic approach to ordinal analysis via the finite combinatorial notion of an α-large set of natural numbers. In contrast to syntactic approaches that use cut elimination, this approach involves constructing finite sets of numbers with combinatorial properties that, in nonstandard instances, give rise to models of the theory being analyzed. This method is applied to obtain ordinal analyses of a number of interesting subsystems of first- and second-order arithmetic.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Proof lengths for instances of the Paris–Harrington principle.Anton Freund - 2017 - Annals of Pure and Applied Logic 168 (7):1361-1382.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • How to characterize provably total functions by local predicativity.Andreas Weiermann - 1996 - Journal of Symbolic Logic 61 (1):52-69.
    Inspired by Pohlers' proof-theoretic analysis of KPω we give a straightforward non-metamathematical proof of the (well-known) classification of the provably total functions of $PA, PA + TI(\prec\lceil)$ (where it is assumed that the well-ordering $\prec$ has some reasonable closure properties) and KPω. Our method relies on a new approach to subrecursion due to Buchholz, Cichon and the author.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Ackermann’s substitution method.Georg Moser - 2006 - Annals of Pure and Applied Logic 142 (1):1-18.
    We aim at a conceptually clear and technically smooth investigation of Ackermann’s substitution method [W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie, Math. Ann. 117 162–194]. Our analysis provides a direct classification of the provably recursive functions of , i.e. Peano Arithmetic framed in the ε-calculus.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Slow reflection.Anton Freund - 2017 - Annals of Pure and Applied Logic 168 (12):2103-2128.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Ordinal recursion, and a refinement of the extended Grzegorczyk hierarchy.S. S. Wainer - 1972 - Journal of Symbolic Logic 37 (2):281-292.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Minimal realizability of intuitionistic arithmetic and elementary analysis.Zlatan Damnjanovic - 1995 - Journal of Symbolic Logic 60 (4):1208-1241.
    A new method of "minimal" realizability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)--functions f such that HA $\vdash \forall x\exists!yA(x, y)\Rightarrow$ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of L(HA) with only x, y free--are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the $ -recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Classifying the provably total functions of pa.Andreas Weiermann - 2006 - Bulletin of Symbolic Logic 12 (2):177-190.
    We give a self-contained and streamlined version of the classification of the provably computable functions of PA. The emphasis is put on illuminating as well as seems possible the intrinsic computational character of the standard cut elimination process. The article is intended to be suitable for teaching purposes and just requires basic familiarity with PA and the ordinals below ε0. (Familiarity with a cut elimination theorem for a Gentzen or Tait calculus is helpful but not presupposed).
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Informal versus formal mathematics.Francisco Antonio Doria - 2007 - Synthese 154 (3):401-415.
    We discuss Kunen’s algorithmic implementation of a proof for the Paris–Harrington theorem, and the author’s and da Costa’s proposed “exotic” formulation for the P = NP hypothesis. Out of those two examples we ponder the relation between mathematics within an axiomatic framework, and intuitive or informal mathematics.
    Download  
     
    Export citation  
     
    Bookmark  
  • Inductive Full Satisfaction Classes.Henryk Kotlarski & Zygmunt Ratajczyk - 1990 - Annals of Pure and Applied Logic 47 (1):199--223.
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • A decidable subclass of the minimal gödel class with identity.Warren D. Goldfarb, Yuri Gurevich & Saharon Shelah - 1984 - Journal of Symbolic Logic 49 (4):1253-1261.
    Download  
     
    Export citation  
     
    Bookmark  
  • Classifying the phase transition threshold for Ackermannian functions.Eran Omri & Andreas Weiermann - 2009 - Annals of Pure and Applied Logic 158 (3):156-162.
    It is well known that the Ackermann function can be defined via diagonalization from an iteration hierarchy which is built on a start function like the successor function. In this paper we study for a given start function g iteration hierarchies with a sub-linear modulus h of iteration. In terms of g and h we classify the phase transition for the resulting diagonal function from being primitive recursive to being Ackermannian.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones. [REVIEW]Andreas Weiermann - 1995 - Archive for Mathematical Logic 34 (5):313-330.
    Let T(Ω) be the ordinal notation system from Buchholz-Schütte (1988). [The order type of the countable segmentT(Ω)0 is — by Rathjen (1988) — the proof-theoretic ordinal the proof-theoretic ordinal ofACA 0 + (Π 1 l −TR).] In particular let ↦Ω a denote the enumeration function of the infinite cardinals and leta ↦ ψ0 a denote the partial collapsing operation on T(Ω) which maps ordinals of T(Ω) into the countable segment TΩ 0 of T(Ω). Assume that the (fast growing) extended Grzegorczyk (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations