Ordinal analysis of terms of finite type

1980 ◽  
Vol 45 (3) ◽  
pp. 493-504 ◽  
Author(s):  
W. A. Howard
Keyword(s):  
Finite Type ◽  
Axiom Of Choice ◽  
Transfinite Induction ◽  
Critical Number ◽  
Ordinal Analysis ◽  
Primitive Recursion ◽  
Successor Relation ◽  
Ordinal Notations ◽  
Primitive Recursive ◽  
Primitive Recursive Functionals

Sanchis [Sa] and Diller [Di] have introduced an interesting relation between terms for primitive recursive functionals of finite type in order to obtain a computability proof. The method is as follows. First the relation is shown to be well-founded. Then computability of each term is obtained by transfinite induction over the relation.Their relation is given by various clauses which define the (immediate) successors of a term. Hence, starting with a term H and repeatedly applying the successor relation one generates the tree of H (say). The problem is to prove that the trees are well-founded. In their proofs Sanchis and Diller use the axiom of bar induction. Diller also gives a proof using transfinite induction: each tree is shown to have a length b < φω(0) (the first ω-critical number) and the induction is over ordinals less than or equal to b.For proof-theoretic purposes it would be desirable to employ a method of proof which is more elementary than the axiom of bar induction and also to obtain a smaller ordinal bound. The purpose of the following is to provide such a method. We show that for a primitive recursive term H of finite type the tree generated by the relation of Sanchis and Diller has length less than ε0. Our method is similar to that used by Tait [Ta] in his theory of infinite terms. The immediately natural metamathematics is elementary intuitionistic analysis with the axiom of choice and transfinite induction over the relevant ordinal notations. We give several versions of the basic list of successor clauses, and for one version we show how to carry out the treatment in Skolem arithmetic (with primitive recursion of lowest type).

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.

A hierarchy for the 1-section of any type two object

1974 ◽  
Vol 39 (1) ◽  
pp. 88-94 ◽  
Author(s):  
S. S. Wainer
Keyword(s):  
Affirmative Answer ◽  
The Other ◽  
Uniqueness Property ◽  
Hyperarithmetical Hierarchy ◽  
Other Hand ◽  
Primitive Recursion ◽  
Ordinal Notations ◽  
Definition Of ◽  
Image Position ◽  
Primitive Recursive

Shoenfield [6] constructed a hierarchy for any type two object F in which 2E is recursive by generalizing the hyperarithmetical hierarchy, using a jump operation jF defined by(A similar hierarchy was constructed independently by Hinman [3].) In order to construct a hierarchy for an arbitrary type two F we must first associate with F an operator which, on one hand will always be recursive in F, and on the other hand will generate all the functions recursive in F when iterated over a simultaneously generated set of ordinal notations OF. Clearly the use of 2E in the above definition of jF(f) can be avoided if, instead of diagonalizing F over all functions recursive in f, we only diagonalize F over, say, the functions primitive recursive in f. If furthermore we code in a function which enumerates all functions primitive recursive in f then the resulting operation will certainly generate a primitive recursively expanding hierarchy of functions recursive in F. The problem that remains is whether this hierarchy will exhaust the 1-section of F. But this reduces to an effectiyized version of the following problem: If g is recursive in some level of the hierarchy, is g primitive recursive in some higher level ? An affirmative answer is suggested by the completeness results of Feferman [2], and our main theorem below will be proved by combining his ideas with those of Shoenfield [6]. The result is a hierarchy which applies to all type two objects, and which replaces the notion of recursion in F by the simpler notion of primitive recursion in certain functions generated by F. Unfortunately, in contrast with the Shoenfield hierarchy, the hierarchy developed here cannot always be expected to have the uniqueness property (even w.r.t. ≤T), and for this reason the proof of our main theorem is rather more complicated than the corresponding proof in [6].

scholarly journals Primitive recursive algebraic theories and program schemes

1977 ◽  
Vol 17 (2) ◽  
pp. 207-233 ◽  
Author(s):  
W. Kühnel ◽  
J. Meseguer ◽  
M. Pfender ◽  
I. Sols
Keyword(s):  
Programming Language ◽  
Generation Process ◽  
Recursive Functions ◽  
Algebraic Theories ◽  
Primitive Recursion ◽  
Recursive Theory ◽  
Carry Over ◽  
Primitive Recursive

We introduce primitive recursion as a generation process for arrows of algebraic theories in the sense of Lawvere and carry over important results on algebraic theories and functorial semantics to the enriched setting of “primitive recursive algebra”: existence of free primitive recursive theories and of theories presented by operations and equations on primitive recursive functions; existence of free models presented by generators and equations. Finally semantical correctness of translations is reduced to correctness for the basic operations. There is a connection to the theory of program schemes: program schemes involving primitive recursion correspond to arrows of a primitive recursive theory freely generated over a graph of basic operations. This theory T can be viewed as a programming language with “arithmetics” given by the basic operations and with DO-loops. A machine loaded with a compiler for T can be interpreted as a T-model in Lawvere's sense, preserving primitive recursion.

A formalization of the theory of ordinal numbers

1965 ◽  
Vol 30 (3) ◽  
pp. 295-317 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Set Theory ◽  
Natural Extension ◽  
Mathematical Induction ◽  
Predicate Calculus ◽  
Transfinite Induction ◽  
First Order ◽  
Recursive Functions ◽  
Ordinal Numbers ◽  
Primitive Recursive ◽  
Order Predicate Calculus

Although Peano's arithmetic can be developed in set theories, it can also be developed independently. This is also true for the theory of ordinal numbers. The author formalized the theory of ordinal numbers in logical systems GLC (in [2]) and FLC (in [3]). These logical systems which contain the concept of ‘arbitrary predicates’ or ‘arbitrary functions’ are of higher order than the first order predicate calculus with equality. In this paper we shall develop the theory of ordinal numbers in the first order predicate calculus with equality as an extension of Peano's arithmetic. This theory will prove to be easy to manage and fairly powerful in the following sense: If A is a sentence of the theory of ordinal numbers, then A is a theorem of our system if and only if the natural translation of A in set theory is a theorem of Zermelo-Fraenkel set theory. It will be treated as a natural extension of Peano's arithmetic. The latter consists of axiom schemata of primitive recursive functions and mathematical induction, while the theory of ordinal numbers consists of axiom schemata of primitive recursive functions of ordinal numbers (cf. [5]), of transfinite induction, of replacement and of cardinals. The latter three axiom schemata can be considered as extensions of mathematical induction.In the theory of ordinal numbers thus developed, we shall construct a model of Zermelo-Fraenkel's set theory by following Gödel's construction in [1]. Our intention is as follows: We shall define a relation α ∈ β as a primitive recursive predicate, which corresponds to F′ α ε F′ β in [1]; Gödel defined the constructible model Δ using the primitive notion ε in the universe or, in other words, using the whole set theory.

scholarly journals Power Kripke–Platek set theory and the axiom of choice

2020 ◽  
Vol 30 (1) ◽  
pp. 447-457
Author(s):  
Michael Rathjen
Keyword(s):  
Set Theory ◽  
Axiom Of Choice ◽  
Selection Mechanism ◽  
Ordinal Analysis ◽  
Inner Model ◽  
Power Set ◽  
The Axiom Of Choice ◽  
The Relationship ◽  
Set Operation

Abstract While power Kripke–Platek set theory, ${\textbf{KP}}({\mathcal{P}})$, shares many properties with ordinary Kripke–Platek set theory, ${\textbf{KP}}$, in several ways it behaves quite differently from ${\textbf{KP}}$. This is perhaps most strikingly demonstrated by a result, due to Mathias, to the effect that adding the axiom of constructibility to ${\textbf{KP}}({\mathcal{P}})$ gives rise to a much stronger theory, whereas in the case of ${\textbf{KP}}$, the constructible hierarchy provides an inner model, so that ${\textbf{KP}}$ and ${\textbf{KP}}+V=L$ have the same strength. This paper will be concerned with the relationship between ${\textbf{KP}}({\mathcal{P}})$ and ${\textbf{KP}}({\mathcal{P}})$ plus the axiom of choice or even the global axiom of choice, $\textbf{AC}_{\tiny {global}}$. Since $L$ is the standard vehicle to furnish a model in which this axiom holds, the usual argument for demonstrating that the addition of ${\textbf{AC}}$ or $\textbf{AC}_{\tiny {global}}$ to ${\textbf{KP}}({\mathcal{P}})$ does not increase proof-theoretic strength does not apply in any obvious way. Among other tools, the paper uses techniques from ordinal analysis to show that ${\textbf{KP}}({\mathcal{P}})+\textbf{AC}_{\tiny {global}}$ has the same strength as ${\textbf{KP}}({\mathcal{P}})$, thereby answering a question of Mathias. Moreover, it is shown that ${\textbf{KP}}({\mathcal{P}})+\textbf{AC}_{\tiny {global}}$ is conservative over ${\textbf{KP}}({\mathcal{P}})$ for $\varPi ^1_4$ statements of analysis. The method of ordinal analysis for theories with power set was developed in an earlier paper. The technique allows one to compute witnessing information from infinitary proofs, providing bounds for the transfinite iterations of the power set operation that are provable in a theory. As the theory ${\textbf{KP}}({\mathcal{P}})+\textbf{AC}_{\tiny {global}}$ provides a very useful tool for defining models and realizability models of other theories that are hard to construct without access to a uniform selection mechanism, it is desirable to determine its exact proof-theoretic strength. This knowledge can for instance be used to determine the strength of Feferman’s operational set theory with power set operation as well as constructive Zermelo–Fraenkel set theory with the axiom of choice.

Functionals defined by transfinite recursion

1965 ◽  
Vol 30 (2) ◽  
pp. 155-174 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Functional Equations ◽  
Partial Ordering ◽  
Closure Properties ◽  
Primitive Recursive Arithmetic ◽  
Primitive Recursion ◽  
Definition Of ◽  
Second Order Systems ◽  
Transfinite Recursion ◽  
Primitive Recursive ◽  
Elementary Closure

This paper deals mainly with quantifier-free second order systems (i.e., with free variables for numbers and functions, and constants for numbers, functions, and functionals) whose basic rules are those of primitive recursive arithmetic together with definition of functionals by primitive recursion and explicit definition. Precise descriptions are given in §2. The additional rules have the form of definition by transfinite recursion up to some ordinal ξ (where ξ is represented by a primitive recursive (p.r.) ordering). In §3 we discuss some elementary closure properties (under rules of inference and definition) of systems with recursion up to ξ. Let Rξ denote (temporarily) the system with recursion up to ξ. The main results of this paper are of two sorts:Sections 5–7 are concerned with less elementary closure properties of the systems Rξ. Namely, we show that certain classes of functional equations in Rη can be solved in Rη for some explicitly determined η < ε(η) (the least ε-number > ξ). The classes of functional equations considered all have roughly the form of definition by recursion on the partial ordering of unsecured sequences of a given functional F, or on some ordering which is obtained from this by simple ordinal operations. The key lemma (Theorem 1) needed for the reduction of these equations to transfinite recursion is simply a sharpening of the Brouwer-Kleene idea.

Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice

2019 ◽  
Vol 29 (4) ◽  
pp. 519-554 ◽  
Author(s):  
Thomas Powell
Keyword(s):  
Large Family ◽  
Classical Analysis ◽  
Wide Range ◽  
Simple Corollary ◽  
The Many ◽  
Primitive Recursive ◽  
Dependent Choice ◽  
Primitive Recursive Functionals ◽  
Negative Translation

Abstract During the last 20 years or so, a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work, we present the many variants of bar recursion used in this context as instantiations of a parametrized form of backward recursion, and give a uniform proof that under certain conditions this recursor realizes a corresponding family of parametrized dependent choice principles. From this proof, the soundness of most of the existing bar recursive realizability interpretations of choice, including those based on the Berardi–Bezem–Coquand functional, modified realizability and the more recent products of selection functions of Escardó and Oliva, follows as a simple corollary. We achieve not only a uniform framework in which familiar realizability interpretations of choice can be compared, but show that these represent just simple instances of a large family of potential interpretations of dependent choice principles.

Sign in / Sign up

Export Citation Format

Share Document