Search

The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this manuscript we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means.

The basis of this work is Leivant’s [6] theory of ramified induction over N, which has elementary recursive strength. It has been redeveloped and extended in various ways by many people; for example, Spoors and Wainer [13] built a hierarchy of ramified theories whose strengths correspond to the levels of the Grzegorczyk hierarchy. Here, a further extension of this hierarchy is developed, in terms of a predicatively generated infinitary calculus with stratifications of numerical inputs up to and including level \(\omega \). The autonomous ordinals are those below \(\Gamma _0\), but they are generated according to a weak (though quite natural) notion of transfinite induction whose computational strength is “slow” rather than “fast” growing. It turns out that the provably computable functions are now those elementary recursive in the Ackermann function (i.e. Grzegorczyk’s \(\omega \)th level). All this is closely analogous to recent works of Jager and Probst [5] and Ranzi and Strahm [9] on iterated stratified inductive definitions, but their theories have full, complete induction as basis, whereas ours have only a weak, ramified form of numerical induction at bottom.

Subrecursive hierarchy classifications are used to compare the complexities of recursive functions according to (i) their derivations in a version of Kleene's equation calculus, and (ii) their computations by term-rewriting. In each case ordinal bounds are assigned, and it turns out that the respective complexity measures are given by (i) a version of the Fast Growing Hierarchy, and (ii) the Slow Growing Hierarchy. Known comparisons between the two hierarchies then provide ordinal trade-offs between (i) derivation and (ii) computation. Characteristics of some well-known subrecursive classes are also read off.

This chapter develops the classification theory of the provably recursive functions of arithmetic. The topic has a long history tracing back to Kreisel [1951], [1952] who, in setting out his “no-counter-example” interpretation, gave the first explicit characterization of the functions “computable in” arithmetic, as those definable by recursions over standard well-orderings of the natural numbers with order types less than e 0 . Such a characterization seems now, perhaps, not so surprising in light of the groundbreaking work of Gentzen [1936], [1943], showing that these well orderings are just the ones over which one can prove transfinite induction in arithmetic, and hence prove the totality of functions defined by recursions over them. Subsequent work of the present authors [1970], [1971], [1972], extending previous results of Grzegorczyk [1953] and Robbin [1965], then provided other complexity characterizations in terms of natural, simply defined hierarchies of so-called “fast growing” bounding functions. What was surprising was the deep connection later discovered, first by Ketonen and Solovay [1981], between these bounding functions and a variety of combinatorial results related to the “modified” finite Ramsey theorem of Paris and Harrington [1977]. It is through this connection that one gains immediate access to a range of mathematically meaningful independence results for arithmetic and stronger theories. Thus, classifying the provably recursive functions of a theory not only gives a measure of its computational power; it also serves to delimit its mathematical power in providing natural examples of true mathematical statements it cannot prove.

Driven by the question, 'What is the computational content of a (formal) proof?', this book studies fundamental interactions between proof theory and computability. It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science. Part I covers basic proof theory, computability and Gödel's theorems. Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to Π11–CA0. Ordinal analysis and the (Schwichtenberg–Wainer) subrecursive hierarchies play a central role and are used in proving the 'modified finite Ramsey' and 'extended Kruskal' independence results for PA and Π11–CA0. Part III develops the theoretical underpinnings of the first author's proof assistant MINLOG. Three chapters cover higher-type computability via information systems, a constructive theory TCF of computable functionals, realizability, Dialectica interpretation, computationally significant quantifiers and connectives and polytime complexity in a two-sorted, higher-type arithmetic with linear logic.

A ”linear — style” sequent calculus makes it possible to explore the close structural relationships between primitive recursive programs and their inductive termination proofs, and between program transformations and their corresponding proof transformations. In this context the recursive — to — tail — recursive transformation corresponds proof theoretically to a certain kind of cut elimination, called here ”call by value cut elimination”.

These lecture notes extend and revise an earlier joint paper: Wainer and Wallen (1992). The intension is to introduce some of the most fundamental concepts and results of proof theory, and to illustrate their relevance to the theory of computation.Each lecture contains one main theorem, given in its simplest and most basic form. The aim is to convey the essential ideas behinf their proofs, keeping the syntactic detail to a minimum so as not to obscure their underlying structure. Some of these results are use elsewhere in this volume, sometimes implicitly and sometimes explicitly, but often in more sophisticated forms. As with car sales, the hope is that once having driven the basic version, the reader will quickly appreciate the more streamlined models.

We explore, from the point of view of mathematical logic, the structural relationships between recursive programs and their termination proofs, and between program transformation and proof transformation, particularly in the case of the recursive- to-tail-recursive transformation. Ideas from proof theory and recursion theory are applied, so as to measure in an abstract way, the logical cost of such transformations.

In this paper we use methods of proof theory to assign ordinals to classes of (terminating) programs, the idea being that the ordinal assignment provides a uniform way of measuring computational complexity “in the large”. We are not concerned with placing prior (e.g. polynomial) bounds on computation-length, but rather with general methods of assessing the complexity of natural classes of programs according to the ways in which they are constructed. We begin with an overview of the method in section 2, the crucial idea being supplied by Buchholz’s ω+–rule. Section 3 introduces a large class of higher-order programs based on Plotkin’s PCF, but with “bounded” fixed point operators controlled by given well-ordering. A Tait-style computability proof then ensures termination. In section 4 the details of the ordinal assignment method are worked out for the case where the given well-ordering is just the ordering of the natural numbers. The complexity bounds thus obtained turn out to be the slow-growing functions G α with α below the Bachmann-Howard ordinal. Thus the functions computed by PCF

The history of primitive recursion traces back to Dedekind, Hubert, Godel, Ackermann, Herbrand, Peter and Kleene. Some may consider it ‘old-hat’ but it is no less important for all that. The aim in these lectures is merely to present the basic ideas and four different characterizations, illustrating fundamental connections with complexity, term-rewriting and proof theory.

The basis of this short course is the strong analogy between programs and proofs (of their specifications). The main theme is the classification of computable number-theoretic functions according to the logical complexity of their formal specification or termination proofs. A significant sub-branch of mathematical logic has grown around this theme since the 1950’s and new ideas are presently giving rise to further developments. The methods employed are chiefly those from proof theory, particularly “normalization” as presented in the accompanying lectures of Helmut Schwichtenberg, and “ordinal assignments”. Since program-termination corresponds to well-foundedness of computation trees, it is hardly surprising that transfinite ordinals and their constructive representations play a crucial role, measuring the logical complexity of programs and of the functions which they compute.