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

1982 ◽  
Vol 47 (2) ◽  
pp. 395-402 ◽  
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.

Grzegorcyk's hierarchy and IepΣ1

1994 ◽  
Vol 59 (4) ◽  
pp. 1274-1284 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Computational Complexity ◽  
Weak Form ◽  
Complexity Class ◽  
Conservative Extension ◽  
Recursive Functions ◽  
Theoretic Characterization ◽  
Definable Functions ◽  
Primitive Recursive

A proof-theoretic characterization of the primitive recursive functions is the Σ1-definable functions in IΣ1 as is shown in Mints [4], Parsons [5], and [8].Then what is a proof-theoretic characterization of Grzegorzyk's hierarchy? First we discuss a related previous work. In Clote and Takeuti [2], we introduced a theory TAC that corresponds to the computational complexity class AC. TAC has a very weak form of induction. We assign a rank to a proof in TAC in the following way. The rank of a proof P in TAC is the nesting number of inductions used in P. Then TACi is defined to be the subtheory of TAC whose proof has a rank ≤ i. We proved that TACi corresponds to the class ACi.In this paper we introduce a theory IepΣ1 which is equivalent to IΣ1. Then we define the rank of a proof in IepΣ1 as the nesting number of inductions in the proof and prove that the proofs with rank ≤ i correspond to Grzegorcyk's hierarchy for i > 0.We also prove that the system that has proofs with rank 0 is actually equivalent to I Δ0. These facts are interesting since it is proved in [10] that the theory isomorphic to TAC∘ by RSUV isomorphism is a conservative extension of I Δo. Therefore there is some analogy between the class AC and the primitive recursive functions.

A system of abstract constructive ordinals

1972 ◽  
Vol 37 (2) ◽  
pp. 355-374 ◽  
Author(s):  
W. A. Howard
Keyword(s):  
Finite Type ◽  
Free Variable ◽  
Transfinite Induction ◽  
Functional Interpretation ◽  
Variable Theory ◽  
Inductive Definitions ◽  
Heyting Arithmetic ◽  
Abstract Notion ◽  
Primitive Recursive ◽  
Primitive Recursive Functionals

As Gödel [6] has pointed out, there is a certain interchangeability between the intuitionistic notion of proof and the notion of constructive functional of finite type. He achieves this interchange in the direction from logic to functionals by his functional interpretation of Heyting arithmetic H in a free variable theory T of primitive recursive functionals of finite type. In the present paper we shall extend Gödel's functional interpretation to the case in which H and T are extended by adding an abstract notion of constructive ordinal. In other words, we obtain the Gödel functional interpretation of an intuitionistic theory U of numbers (i.e., nonnegative integers) and constructive ordinals in a free variable theory V of finite type over both numbers and constructive ordinals. This allows us to obtain an analysis of noniterated positive inductive definitions [8].The notion of constructive ordinal to be treated is as follows. There is given a function J which embeds the nonnegative integers in the constructive ordinals. A constructive ordinal of the form Jn is said to be minimal. There is also given a function δ which associates to each constructive ordinal Z and number n a constructive ordinal δZn which we denote by Zn. When Z is nonminimal, each Zn is called an immediate predecessor of Z. The basic principle for forming constructive ordinals says: for every function f from numbers n to constructive ordinals, there exists a constructive ordinal Z such that Zn = fn for all n. The principle of transfinite induction with respect to constructive ordinals says: if a property Q(Z) of constructive ordinals Z holds for minimal Z, and if ∀nQ(Zn) → Q(Z) holds for all Z, then Q(Z) holds for all Z.

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

1998 ◽  
Vol 63 (4) ◽  
pp. 1348-1370 ◽  
Author(s):  
Andreas Weiermann
Keyword(s):  
Recursive Function ◽  
Term Rewriting ◽  
Careful Analysis ◽  
Recursion Theory ◽  
Cut Elimination ◽  
Complexity Bounds ◽  
Recursive Functions ◽  
Collapsing Function ◽  
Primitive Recursive

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.

Note on a conjecture of Skolem

1946 ◽  
Vol 11 (3) ◽  
pp. 73-74 ◽  
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.

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

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

scholarly journals Drug delivery applications of poly-γ-glutamic acid

2021 ◽  
Vol 7 (1) ◽  
Author(s):  
Olalekan A. Balogun-Agbaje ◽  
Olubusola A. Odeniyi ◽  
Michael A. Odeniyi
Keyword(s):  
Drug Delivery ◽  
Glutamic Acid ◽  
Site Characterization ◽  
Fermentation Medium ◽  
Production Optimization ◽  
Main Body ◽  
Crucial Step ◽  
Drug Delivery Application ◽  
Made In

Abstract Background Poly-γ-glutamic acid (γ-PGA) is a biopolymer of microbial origin, consisting of repeating units of l-glutamic acid and/or D-glutamic acid. The biopolymer has found use in the fields of agriculture, food, wastewater, and medicine, owing to its non-toxic, biodegradable, and biocompatible properties. Due to its biodegradability, γ-PGA is being tipped to dislodge synthetic plastics in drug delivery application. High cost of production, relative to plastics, is however a clog in the wheel of achieving this. Main body of abstract This review looked at the production, nanoparticles fabrication, and drug delivery application of γ-PGA. γ-PGA production optimization by modifying the fermentation medium to tailor towards the production of desirable polymer at reduced cost and techniques for the formulation of γ-PGA nanoparticle as well as its characterization were discussed. This review also evaluated the application of γ-PGA and its nanoparticles in the delivery of drugs to action site. Characterization of γ-PGA and its nanoparticles is a crucial step towards determining the applicability of the biopolymer. γ-PGA has been used in the delivery of active agents to action sites. Conclusion This review highlights some of the efforts that have been made in the appraisal of γ-PGA and its nanoparticles for drug delivery. γ-PGA is a candidate for future extensive use in drug delivery.

Sign in / Sign up

Export Citation Format

Share Document