How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study

AbstractInspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε0-recursive function []0: T → ω so that a reduces to b implies [a]0 > [b]0. The construction of [ ]0 is based on a careful analysis of the Howard-Schütte treatment of Gödel's T and utilizes the collapsing function ψ: ε0 → ω which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of [ ]0 is also crucially based on ideas developed in the 1995 paper “A proof of strongly uniform termination for Gödel's T by the method of local predicativity” by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper.Indeed, for given n let Tn be the subsystem of T in which the recursors have type level less than or equal to n + 2. (By definition, case distinction functionals for every type are also contained in Tn.) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the Tn-derivation lengths in terms of ω+2-descent recursive functions. The derivation lengths of type one functionals from Tn (hence also their computational complexities) are classified optimally in terms of <ωn+2 -descent recursive functions.In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T0 is primitive recursive, thus any type one functional a in T0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T1 in terms of multiple recursion.As proof-theoretic corollaries we reobtain the classification of the IΣn+1-provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Gödel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO(ε0) ⊢ Π20 − Refl(PA) and PRA + PRWO(ωn+2) ⊢ Π20 − Refl(IΣn+1), hence PRA + PRWO(ε0) ⊢ Con(PA) and PRA + PRWO(ωn+2) ⊢ Con(IΣn+1).For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity.

Download Full-text

A classification of the one-argument primitive recursive functions

Archive for Mathematical Logic ◽

10.1007/bf02023023 ◽

1983 ◽

Vol 23 (1) ◽

pp. 161-174 ◽

Cited By ~ 3

Author(s):

Jovan Naumović

Keyword(s):

Recursive Functions ◽

The One ◽

Primitive Recursive

Download Full-text

Syntactic translations and provably recursive functions

Journal of Symbolic Logic ◽

10.2307/2274322 ◽

1985 ◽

Vol 50 (3) ◽

pp. 682-688 ◽

Cited By ~ 22

Author(s):

Daniel Leivant

Keyword(s):

Cut Elimination ◽

Mathematical Apparatus ◽

Constructive Logic ◽

Similar Nature ◽

Recursive Functions ◽

Conservation Result ◽

Mathematical Techniques ◽

Primitive Recursive ◽

Potential Objection ◽

Intuitionistic Version

Syntactic translations of classical logic C into intuitionistic logic I are well known (see [Kol25], [Gli29], [Göd32], [Kre58b], [M063], [Cel69] and [Lei71]). Harvey Friedman [Fri78] used a translation of a similar nature, from I into itself, to reprove a theorem of Kreisel [Kre58a] that various theories based on I are closed under Markov's rule: if ¬¬∃x.α is a theorem, where x is a numeric variable and α is a primitive recursive relation, then ∃x.α is a theorem. Composing this with Gödel's translation from classical to intuitionistic theories, it follows that the functions provably recursive in the classical version of the theories considered are provably recursive already in their intuitionistic version. This conservation result is important in that it guarantees that no information about the convergence of recursive functions is lost when proofs are restricted to constructive logic, thus removing a potential objection to the use of constructive logic in reasoning about programs (see [C078] for example). Conversely, no objection can be raised by intuitionists to proofs of formulas that use classical reasoning, because such proofs can be converted to constructive proofs (this has been exploited extensively; see [Smo82]).Proofs of closure under Markov's rule had required, until Friedman's proof, a relatively sophisticated mathematical apparatus. The chief method used Godel's “Dialectica” interpretation (see [Tro73, §3]). Other proofs used cut-elimination, provable reflection for subsystems [Gir73], and Kripke models [Smo73]. Moreover, adapting these proofs to new theories had required that the underlying meta-mathematical techniques be adapted first, not always a trivial step.

Download Full-text

On definition trees of ordinal recursive functionals: Reduction of the recursion orders by means of type level raising

Journal of Symbolic Logic ◽

10.2307/2273149 ◽

1982 ◽

Vol 47 (2) ◽

pp. 395-402 ◽

Cited By ~ 8

Author(s):

Jan Terlouw

Keyword(s):

Lower Order ◽

Recursive Function ◽

Functional Interpretation ◽

Crucial Step ◽

Recursive Functions ◽

Order Types ◽

Primitive Recursive ◽

Primitive Recursive Functionals

It is known that every < ε0-recursive function is also a primitive recursive functional. Kreisel has proved this by means of Gödel's functional-interpretation, using that every < ε0-recursive function is provably recursive in Heyting's arithmetic [2, §3.4]. Parsons obtained a refinement of Kreisel's result by a further examination of Gödel's interpretation with regard to type levels [3, Theorem 5], [4, §4]. A quite different proof is provided by the research into extensions of the Grzegorczyk hierarchy as done by Schwichtenberg and Wainer: this yields another characterization of the < ε0-recursive functions from which easily appears that these are primitive recursive functionals (see [5] in combination with [6, Chapter II]).However, these proofs are indirect and do not show how, in general, given a definition tree of an ordinal recursive functional, transfinite recursions can be replaced (in a straightforward way) by recursions over wellorderings of lower order types. The argument given by Tait in [9, pp. 189–191] seems to be an improvement in this respect, but the crucial step in it is (at least in my opinion) not very clear.

Download Full-text

Ordinal recursion, and a refinement of the extended Grzegorczyk hierarchy

Journal of Symbolic Logic ◽

10.2307/2272973 ◽

1972 ◽

Vol 37 (2) ◽

pp. 281-292 ◽

Cited By ~ 24

Author(s):

S. S. Wainer

Keyword(s):

Natural Manner ◽

Recursive Functions ◽

Class A ◽

Primitive Recursive ◽

Theoretic Function ◽

Number Class

It is well known that iteration of any number-theoretic function f, which grows at least exponentially, produces a new function f′ such that f is elementary-recursive in f′ (in the Csillag-Kalmar sense), but not conversely (since f′ majorizes every function elementary-recursive in f). This device was first used by Grzegorczyk [3] in the construction of a properly expanding hierarchy {ℰn: n = 0, 1, 2, …} which provided a classification of the primitive recursive functions. More recently it was shown in [7] how, by iterating at successor stages and diagonalizing over fundamental sequences at limit stages, the Grzegorczyk hierarchy can be extended through Cantor's second number-class. A problem which immediately arises is that of classifying all recursive functions, and an answer to this problem is to be found in the general results of Feferman [1]. These results show that although hierarchies of various types (including the above extensions of Grzegorczyk's hierarchy) can be produced, which range over initial segments of the constructive ordinals and which do provide complete classifications of the recursive functions, these cannot be regarded as classifications “from below”, since the method of assigning fundamental sequences at limit stages must be highly noneffective. We therefore adopt the more modest aim here (as in [7], [12], [14]) of characterising certain well-known (effectively generated) subclasses of the recursive functions, by means of hierarchies generated in a natural manner, “from below”.

Download Full-text

Term rewriting theory for the primitive recursive functions

Annals of Pure and Applied Logic ◽

10.1016/s0168-0072(96)00015-2 ◽

1997 ◽

Vol 83 (3) ◽

pp. 199-223 ◽

Cited By ~ 12

Author(s):

E.A. Cichon ◽

A. Weiermann

Keyword(s):

Term Rewriting ◽

Recursive Functions ◽

Primitive Recursive

Download Full-text

A jump operator for subrecursion theories

Journal of Symbolic Logic ◽

10.2307/2586478 ◽

1999 ◽

Vol 64 (2) ◽

pp. 460-468

Author(s):

A.J. Heaton

Keyword(s):

Elementary Function ◽

Recursion Theory ◽

Jump Operator ◽

Fast Growing ◽

Recursive Functions ◽

Ordinal Notations ◽

Independence Results ◽

Image Position ◽

Hyperarithmetic Hierarchy

In classical recursion theory, the jump operator is an important concept fundamental in the study of degrees. In particular, it provides a way of defining the hyperarithmetic hierarchy by iterating over Kleene's O. In subrecursion theories, hierarchies (variants of the fast growing hierarchy) are also important in underlying the central concepts, e.g. in classifying provably recursive functions and associated independence results for given theories (see, e.g. [BW87], [HW96], [R84] and [Z77]). A major difference with the hyperarithmetic hierarchy is in the way each level of a subrecursive hierarchy is crucially dependent upon the system of ordinal notations used (see [F62]). This has been perhaps the major stumbling block in finding a classification of all general recursive functions using such hierarchies.Here we present a natural subrecursive analogue of the jump operator and prove that the hierarchy based on the ”subrecursive jump” is elementarily equivalent to the fast growing hierarchy.The paper is organised as follows. First the preliminary definitions are given together with a statement of the main theorem and a brief outline of its proof. The proof of the theorem is then given, with the more technical parts separated out as facts which are proven afterwards.We let {e}g(x) denote computation of the e-th partial recursion with oracle g, on input x. Furthermore [e] denotes the e-th elementary recursive function, defined so thatSimilarly, for a given oracle g the e-th relativized elementary function is denoted by [e]g.

Download Full-text

Note on a conjecture of Skolem

Journal of Symbolic Logic ◽

10.2307/2266735 ◽

1946 ◽

Vol 11 (3) ◽

pp. 73-74 ◽

Cited By ~ 1

Author(s):

Emil L. Post

Keyword(s):

Recursive Function ◽

Recursive Relation ◽

Natural Numbers ◽

Excellent Review ◽

Recursive Functions ◽

Diagonal Argument ◽

Primitive Recursive ◽

Recursive Relations

In his excellent review of four notes of Skolem on recursive functions of natural numbers Bernays states: “The question whether every relation y = f(x1,…, xn) with a recursive function ƒ is primitive recursive remains undecided.” Actually, the question is easily answered in the negative by a form of the familiar diagonal argument.We start with the ternary recursive relation R, referred to in the review, such that R(x, y, 0), R(x, y, 1), … is an enumeration of all binary primitive recursive relations.

Download Full-text

A note on the representation of general recursive functions and the μ quantifier

Mathematical Proceedings of the Cambridge Philosophical Society ◽

10.1017/s030500410003382x ◽

1959 ◽

Vol 55 (2) ◽

pp. 145-148

Author(s):

Alan Rose

Keyword(s):

Natural Number ◽

Recursive Function ◽

Natural Numbers ◽

General Recursive Function ◽

Recursive Functions ◽

Image Position ◽

Primitive Recursive

It has been shown that every general recursive function is definable by application of the five schemata for primitive recursive functions together with the schemasubject to the condition that, for each n–tuple of natural numbers x1,…, xn there exists a natural number xn+1 such that

Download Full-text

Classifying Predicates and Languages

International Journal of Foundations of Computer Science ◽

10.1142/s0129054197000033 ◽

1997 ◽

Vol 08 (01) ◽

pp. 15-41 ◽

Cited By ~ 10

Author(s):

Carl H. Smith ◽

Rolf Wiehagen ◽

Thomas Zeugmann

Keyword(s):

Learning Theory ◽

Classification Problems ◽

Attention In Learning ◽

Recursive Functions ◽

Standard Classification ◽

Resource Bound ◽

Multi Classification

The present paper studies a particular collection of classification problems, i.e., the classification of recursive predicates and languages, for arriving at a deeper understanding of what classification really is. In particular, the classification of predicates and languages is compared with the classification of arbitrary recursive functions and with their learnability. The investigation undertaken is refined by introducing classification within a resource bound resulting in a new hierarchy. Furthermore, a formalization of multi-classification is presented and completely characterized in terms of standard classification. Additionally, consistent classification is introduced and compared with both resource bounded classification and standard classification. Finally, the classification of families of languages that have attracted attention in learning theory is studied, too.

Download Full-text