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.

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).

Choice principles, the bar rule and autonomously iterated comprehension schemes in analysis

1983 ◽  
Vol 48 (1) ◽  
pp. 63-70 ◽  
Author(s):  
S. Feferman ◽  
G. Jäger
Keyword(s):  
General Result ◽  
Recursive Relation ◽  
Transfinite Induction ◽  
Conservative Extension ◽  
Main Result Theorem ◽  
Functional Interpretation ◽  
Result Theorem ◽  
Primitive Recursive ◽  
Comprehension Axiom

In [10] Friedman showed that (-AC) is a conservative extension of (-CA)<ε0for-sentences wherei= min(n+ 2, 4), i.e.,i= 2, 3, 4 forn= 0, 1, 2 +m. Feferman [5], [7] and Tait [11], [12] reobtained this result forn= 0, 1 and even with (-DC) instead of (-AC). Feferman and Sieg established in [9] the conservativeness of (-DC) over (-CA)<ε0for-sentences (ias above) for alln. In each paper, different methods of proof have been used. In particular, Feferman and Sieg showed how to apply familiar proof-theoretical techniques by passing through languages with Skolem functionals.In this paper we study the same choice principles in the presence of theBar Rule(BR), which permits one to infer the scheme of transfinite induction on a primitive recursive relation ≺ when it has been proved that ≺ is wellfounded. The main result (Theorem 1 below) characterizes (-DC) + (BR) as a conservative extension of a system of the autonomously iterated-comprehension axiom for-sentences (idepending onnas above). Forn= 0 this has been proved by Feferman in the form that (-DC) + (BR) is a conservative extension of (-CA)<Γ0; this was first done in [8] by use of the Gödel functional interpretation for the stronger systemZω+μ+ (QF-AC) + (BR) and then more recently by the simpler methods of [9]. Jäger showed how the latter methods could also be used to obtain the general result of Theorem 1 below.

scholarly journals Functional interpretation and inductive definitions

2009 ◽  
Vol 74 (4) ◽  
pp. 1100-1120 ◽  
Author(s):  
Jeremy Avigad ◽  
Henry Towsner
Keyword(s):  
Finite Type ◽  
Functional Interpretation ◽  
Inductive Definitions ◽  
Transfinite Recursion

AbstractExtending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

An introduction to well-ordering proofs in Martin-Löf’s type theory

1998 ◽  
Author(s):  
Anton Setzer
Keyword(s):  
Lower Bound ◽  
Classical Theory ◽  
Type Theory ◽  
Direct Method ◽  
Order Type ◽  
Transfinite Induction ◽  
Linear Orderings ◽  
Heyting Arithmetic ◽  
Primitive Recursive Arithmetic ◽  
Primitive Recursive

The proof-theoretic strength α of a theory is the supremum of all ordinals up to which we can prove transfmite induction in that theory. Whereas for classical theories the main problem is to show that α is an upper bound for the strength—this usually means to reduce the theory to a weak theory like primitive recursive arithmetic or Heyting arithmetic extended by transfmite induction up to α, which can be considered to be more constructive than the classical theory itself—for constructive theories this is in most cases not difficult, since we can easily build a term model in a classical theory of known strength. For constructive theories in general the main problem is to show that α is a lower bound: that despite the restricted principles available one has a proof-theoretically strong theory. In this article we will concentrate on the direct method for showing that α is a lower bound, namely well-ordering proofs: to carry out in the theory a sequence of proofs of the well-foundedness of linear orderings of order type αn, such that supn∈ω αn = α. Such proofs can be considered to be the logically most complex proofs which one can carry out in the theory; in most cases, in addition to transfinite induction up to αn for each n, only primitive recursive arithmetic is needed in order to analyze the theory proof-theoretically and in order to prove the same Π02-sentences. Griffor and Rathjen (1994) have used the more indirect method of interpreting theories of known strength in type theory for obtaining lower bounds for the strength of it. Apart from the fact that in the case of one universe and W-type Griffor and Rathjens’ approach did not yield sharp bounds, we believe that the direct method has the advantage of giving a deeper insight into the theory, since one examines the principles of the theory directly without referring to the analysis of another theory, and that the programs obtained by it are of independent interest. In Setzer (1995) and Setzer (1996) we have carried out well-ordering proofs for Martin-Löf’s type theory with W-type and one universe and for the Mahlo universe.

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.

A NEW COMPUTATION OF THE Σ-ORDINAL OF KPω

2014 ◽  
Vol 79 (01) ◽  
pp. 306-324 ◽  
Author(s):  
FERNANDO FERREIRA
Keyword(s):  
Finite Type ◽  
Order Theory ◽  
Second Order ◽  
Not Given ◽  
Functional Interpretation ◽  
Recursive Tree ◽  
Image Position ◽  
Primitive Recursive

Abstract We define a functional interpretation of KP ω using Howard’s primitive recursive tree functionals of finite type and associated terms. We prove that the Σ-ordinal of KP ω is the least ordinal not given by a closed term of the ground type of the trees (the Bachmann-Howard ordinal). We also extend KP ω to a second-order theory with Δ 1-comprehension and strict- ${\rm{\Pi }}_1^1$ reflection and show that the Σ-ordinal of this theory is still the Bachmann-Howard ordinal. It is also argued that the second-order theory is Σ1-conservative over KPω.

Ordinal analysis of simple cases of bar recursion

1981 ◽  
Vol 46 (1) ◽  
pp. 17-30 ◽  
Author(s):  
W. A. Howard
Keyword(s):  
Free Variable ◽  
Recursion Operator ◽  
Ordinal Analysis ◽  
Functional Interpretation ◽  
Free Variables ◽  
Ordinal Measure ◽  
Level 3 ◽  
Transfinite Recursion ◽  
Primitive Recursive

The purpose of the following is to give an ordinal analysis of bar recursion of type 0 for the cases in which the bar recursion operator has type level 3 or 4. We show that the associated ordinals are the ε0th epsilon number and the first ε0-critical number, respectively. Also we analyze a restricted bar recursion operator of level 3 which provides the Gödel functional interpretation of an intuitionistic form of König's lemma. The ordinal in this case is ε0.Let + BR0 be Gödel's theory of primitive recursive functional of finite type extended by functors Φ for bar recursion of type zero. To make bar recursion resemble transfinite recursion more closely, and thereby facilitate the ordinal analysis, we extend + BR0 to a system of terms . By Theorem 1.1a term of + BR0 which is computable by the rules of is already computable by the rules of + BR0, so it is sufficient to give an ordinal analysis of the terms of .A term H of is said to be semi-closed if its free variables have level not exceeding 1. If, in addition, H has level not exceeding 2, then an ordinal measure for H is given by a length for one of its computation trees. We call this a computation size for H. Let F(X) be a term whose free variables have level not exceeding 2, and suppose the variable X of type 2 is the only free variable of level 2.

Sign in / Sign up

Export Citation Format

Share Document