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 proof-theoretic characterization of the primitive recursive set functions

1992 ◽  
Vol 57 (3) ◽  
pp. 954-969 ◽  
Author(s):  
Michael Rathjen
Keyword(s):  
Set Theory ◽  
Elementary Proof ◽  
Weak Version ◽  
Definable Set ◽  
Set Functions ◽  
Theoretic Characterization ◽  
Universe Of Sets ◽  
Set Function ◽  
Primitive Recursive

AbstractLet KP− be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V ≔ universe of sets) be a Δ0-definable set function, i.e. there is a Δ0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and V ⊨ ∀x∃!yφ(x, y). In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the collection of those functions which are Σ1-definable in KP− + Σ1-Foundation + ∀x∃!yφ(x, y). Moreover, we show that this is still true if one adds Π1-Foundation or a weak version of Δ0-Dependent Choices to the latter theory.

Computational complexity, speedable and levelable sets

1977 ◽  
Vol 42 (4) ◽  
pp. 545-563 ◽  
Author(s):  
Robert I. Soare
Keyword(s):  
Computational Complexity ◽  
Jump Operator ◽  
Information Theoretic ◽  
Recursively Enumerable ◽  
Index Sets ◽  
Close Relationship ◽  
Speed Up ◽  
Theoretic Characterization ◽  
Large Speed

One of the most interesting aspects of the theory of computational complexity is the speed-up phenomenon such as the theorem of Blum [6, p. 326] which asserts the existence of a 0, 1-valued total recursive function with arbitrarily large speed-up. Blum and Marques [10] extended the speed-up definitions from total to partial recursive functions, or equivalently, to recursively enumerable (r.e.) sets, and introduced speedable and levelable sets. They classified the effectively speedable sets as the subcreative sets but remarked that “the characterizations we provided for speedable and levelable sets do not seem to bear a close relationship to any already well-studied class of recursively enumerable sets.” The purpose of this paper is to give an “information theoretic” characterization of speedable and levelable sets in terms of index sets resembling the jump operator. From these characterizations we derive numerous consequences about the degrees and structure of speedable and levelable sets.

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.

LAMBDA-REPRESENTABLE FUNCTIONS OVER TERM ALGEBRAS

2001 ◽  
Vol 12 (01) ◽  
pp. 3-29 ◽  
Author(s):  
MASAKO TAKAHASHI
Keyword(s):  
Related Topic ◽  
Natural Numbers ◽  
Simple Formulation ◽  
Recursive Functions ◽  
Standard Notion ◽  
Theoretic Characterization

In this paper, we study λ→-representability of functions over (open or closed) term algebras. First, by extending the standard notion of λ→-representation of closed (or variable-free) terms to open terms and extending the notion of λ→-representable functions accordingly, we give a recursion-theoretic characterization of the class of λ→-representable functions over open term algebras. Then, based on this result, we obtain two characterizations of the class of λ→-representable functions over closed term algebras (i.e., free structures). As a related topic, in the Appendix we give a simple formulation of the recursive word functions, and study their properties in relation to recursive functions on natural numbers and type-free pure λ-calculus.

Minimal readability of intuitionistic arithmetic and elementary analysis

1995 ◽  
Vol 60 (4) ◽  
pp. 1208-1241 ◽  
Author(s):  
Zlatan Damnjanovic
Keyword(s):  
Finite Type ◽  
Peano Arithmetic ◽  
New Method ◽  
Recursive Functions ◽  
Heyting Arithmetic ◽  
Elementary Analysis ◽  
Skolem Functions ◽  
Definable Functions ◽  
Intuitionistic Arithmetic

AbstractA new method of “minimal” readability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)—functions f such that HA ⊢ ∀x∃!yA(x, y) ⇒ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of ℒ(HA) with only x,y free—are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the < ε0-recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be < ε0-recursive. The method is extended to intuitionistic finite-type arithmetic, , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived.

scholarly journals A lattice-theoretic characterization of pure subgroups of Abelian groups

2021 ◽  
Author(s):  
M. Ferrara ◽  
M. Trombetti
Keyword(s):  
Abelian Group ◽  
Abelian Groups ◽  
Subgroup Lattice ◽  
General Definition ◽  
Short Paper ◽  
Theoretic Characterization ◽  
Definition Of

AbstractLet G be an abelian group. The aim of this short paper is to describe a way to identify pure subgroups H of G by looking only at how the subgroup lattice $$\mathcal {L}(H)$$ L ( H ) embeds in $$\mathcal {L}(G)$$ L ( G ) . It is worth noticing that all results are carried out in a local nilpotent context for a general definition of purity.

Information-theoretic characterization of eye-tracking signals with relation to cognitive tasks

2021 ◽  
Vol 31 (3) ◽  
pp. 033107
Author(s):  
F. R. Iaconis ◽  
A. A. Jiménez Gandica ◽  
J. A. Del Punta ◽  
C. A. Delrieux ◽  
G. Gasaneo
Keyword(s):  
Eye Tracking ◽  
Cognitive Tasks ◽  
Information Theoretic ◽  
Theoretic Characterization
Sign in / Sign up

Export Citation Format

Share Document