Interpretations of Transfinite Recursion and Parametric Abstraction in Types

Mariko Yasugi^{1)} and Susumu Hayashi^{2)}

1) Faculty of Science, Kyoto Sangyo University, Kyoto 603, Japan 2) Department of Applied Mathematics and Informatics, Ryukoku University, Ohtsu 520-21, Japan

1 Introduction

In our previous work Yasugi^{3}, the first author defined a system of generalized types, which has transfinite recursion and parametric abstraction among formation rules of types. A system of terms with these types (now called TRM) was then introduced. It contains parametric abstraction,lambdaabstraction and bar recursion among formation rules of terms. Our purpose there was to realize the modified realizability interpretation of a constructive system of arithmetic, now called TRDB, which contains universal quantification over functions, definition of predicates by transfinite recursion and bar induction. The significance of these systems is explained in Yasugi^{3}.

Strong normalizability and the Church-Rosser property of these types (called type-forms) as well as of the terms (called term-forms) have been established in Yasugi-Hayashi^{4}. There, a map from TRDB to TRM is defined, by which the modified realizability interpretation of TRDB is better presented, and also the computational meaning of TRDB is explicated. In this article, we continue to investigate some properties of TRM. First, a set model of type-forms is presented, and the term-forms are interpreted as functions in the image sets of type-forms (Theorem 1). Since a map from TRDB to TRM is defined in Yasugi-Hayashi^{4}, this means that TRDB also has a set model. Another theme is to translate TRM into TRDB (Theorem 2). This is the reversal of a result in Yasugi-Hayashi^{4}.

The article is more or less self-contained, although familiarity with Yasugi^{3} will help understanding its background. Howard-Kreisel^{1} and Troelstra^{2} are useful in learning bar induction and systems of constructive arithmetic.

2 Set-model of type-forms

Type-forms are types with parametric variables. They are briefly described below. We do not elaborate with details, since they are thoroughly discussed in Yasugi^{3} and Yasugi-Hayashi^{4}.

Definition 2.1. Let I ≡ (I, <_{I}) be a primitive recursive well-ordered structure (on natural numbers). This will be the basis of the subsequent arguments.

(1) The basic language BL consists of the following. (1.1) Constant symbols of the following kind are prepared. Let C_{n} be the set of constants representing all the number-theoretic functions of arity n, where C_{0} denotes the set of natural numbers. Let C be the union of C_{n} for all n = 0,1,2,3,.... Constant symbols of BL are those of C. (1.2) Propositional connectives are ∧, ∨ and ⊃. (1.3) Constant symbols denoting some primitive recursive predicates such as =, <, <_{I} are assumed. (1.4) Countably many variables of arity n are prepared for each n = 0, 1, 2, . . .. A variable of arity n is supposed to range over C_{n}.

Now BL-terms and BL-formulas are defined as usual from these symbols. (A ⊃ 0 = 1 will be abbreviated to ¬A.) We assume that elementary properties of I can be expressed in BL.

(2) Type-forms are defined below, based on the language BL. (2.1) Symbols N and 1 are (atomic) type-forms. (2.2) If α and β are type-forms, then so are α → β (function space), {x}α (parametric abstraction), π(α; t) (projection) and cond[A; α, β] (case definition), where x is a variable of BL, t is a BL-term and A is a BL-formula. (2.3) R[i, t] (transfinite recursion) is a type-form, where R is a special letter denoting recursion operator, i is a BL-term which is supposed to be an element of I and t is a BL-term. (R[i, t] is characterized by a fixed type-form η, which is defined without R. See (1.4) of Definition 2.2 below.) (2.4) ρ[j <_{I} i; R[j, s]] (restriction) is a type-form, where j and i are BL-terms which are supposed to be elements of I and s is a BL-term.

(3) A type-form without free variables is called a type.

(4) Type will denote the collection of type-forms together with the reduction rules defined in the next definition.

Note. BL in the present context is stronger than the original one, since it contains constsnts corresponding to all the number-theoretic functions while previously we assumed constants corresponding to those which are primitive recursive in a parameter. It does not affect the validity of the argument that follows, since our interest at this time is a set model of type-forms.

Definition 2.2. (1) Conversion rules of type-forms, say α to β, denoted by α ⇒ β, are the following. (1.1) π({x}α; t) ⇒ α[t/x],where α[t/x] represents substitution of t for x in α. (1.2) cond[A; α_{1}, α_{2}] ⇒ β, where β is α_{1} if A is a true sentence in the standard interpretation of the symbols, and β is α_{2} if A is a false sentence. (1.3) ρ[j <_{I} i; R[j, s]] ⇒ β, where β is R[j, s] if j <_{I} i is a true sentence, and it is 1 if j <_{I} i is a false sentence. (1.4) Let Ξ be a designated symbol which is temporarily regarded as an atomic type, let η be a type-form with Ξ but without R, whose free variables are k and w, where k is of arity 0 and w is of an arbitrary arity. η[i/k, t/w] will denote simultaneous substitution of i for k and t for w, and R(i) will abbreviate {j}{x}ρ[j <_{I} i; R[j, x]].

R[i, t] ⇒ η[i/k; t/w][R(i)/Ξ],

where X[Y/Ξ] represents the result of replacement of Ξ by Y in X.

(2) α is said to be 1-reduced to β if β is obtained from α by one conversion applied to a subtype of α, with the strategy that conversions (1.3) and (1.4) enjoy priorities; that is, one does not go inside ρ and R. α is said to be reducible to β if there is a sequence of reductions (possibly empty) from α to β.

Note. It is obvious that the reducts of a type-form are again type-forms, and that free variables do not increase by reductions.

Let F_{n} denote the collection of all the number-theoretic functions of arity n, where F_{0} will denote the set of natural numbers, and let F be the union of F_{n}, n = 0, 1, 2, ....

We are now to present an interpretation of Type in V_{θ}, the universe of sets of rank below θ, where θ is a limit regular ordinal (hence a cardinal) such that F ∈ V_{θ} (hence F_{n} ∈ V_{θ} for every n). The definition below is carried out in ZFC relativized to V_{θ}.

Definition 2.3. Let V ar be the collection of variables of BL, and let ρ be a map:V ar → F, where a variable of arity n is assigned a function in F_{n}. [[α]]_{ρ}, to be defined below, will express the interpretation of α in V_{θ} under the assignment ρ. Let ι denote a designated set in V_{θ} (different from the elements of F).

(1) For any BL-term t, [[t]]_{ρ} is defined to be the natural interpretation of t under assignment ρ. In order to spare notational complications, we write t^{∗} for [[t]]_{ρ}.

(2) [[N]]_{ρ} = F_{0} (the set of natural numbers); [[1]]_{ρ} = {ι} (the singleton ι); [[α → β]]_{ρ} = [[β]]_{ρ}^{[[α]]_{ρ}} (function space); [[{x}α]]_{ρ} = ∏_{v∈F_{n}}[[α]]_{ρ[v/x]} (Cartesian product) if x is a variable of arity n; [[π(α; t)]]_{ρ} = {v|∃f ∈ [[α]]_{ρ}(v = f′t^{∗})} (Here a′b is defined to be c if there is a unique set c such that ⟨b, c⟩ ∈ a, and it is ι otherwise.); [[cond[A; α, β]]]_{ρ} = {a ∈ [[α]]_{ρ} ∪[[β]]_{ρ}|(A^{∗} ⊃ a ∈ [[α]]_{ρ})∧(¬A^{∗} ⊃ a ∈ [[β]]_{ρ})} (A^{∗} is a set-theoretic formula obtained from A by interpreting its terms under ρ.).

(3) To interpret R, we proceed as follows. Let η be the type-form (without R) as in (1.4) of Definition 2.2. Put ρ(Ξ) = z for a set variable z.Then [[η]]_{ρ} (denoted by g(z)) can be defined according to (1) and (2) above.We can define a subset h of V_{θ} such that h′c = g(c) for any set c in V_{θ}. It is a fact that the principle of transfinite recursion holds for h along I^{∗}.That is,there is a set F in V_{θ} such that F is a unique function over I^{∗} satisfying ∀i ∈ I^{∗}[F′i = h′(F′′i)]. Now put [[R[i, t]]]_{ρ} = (F′i^{∗})′t^{∗}. (F′′i is F with domain restricted to the elements below i.)

[[ρ[j <_{I} i; R[j, s]]]_{ρ}

= {a ∈ (F′j^{∗})′s^{∗} ∪ {ι}; (j^{∗} <_{I} i^{∗} ⊃ a ∈ (F′f^{∗})′s^{∗}) ∧ (¬j^{∗} <_{I} i^{∗} ⊃ a = ι)}.

Note. The apparently unnatural interpretation of π and ρ is to guarantee that interpretation sets be nonempty, and only for this purpose. (See the proposition below.)

Proposition 2.1. (1) [[α[t/x]]]_{ρ} = [[α]]_{ρ[t^{∗}/x]}.

(2) [[α]]_{ρ} ∈ V_{θ}.

(3) [[α]]_{ρ} is nonempty.

(4) If α ⇒ β, then [[α]]_{ρ} = [[β]]_{ρ}. That is,[[π({x}α; t)]]_{ρ} = [[α[t/x]]]_{ρ}; [[cond[A; α, β]]]_{ρ} = [[α]]_{ρ} if A is a true sentence, and = [[β]]_{ρ} if A is a false sentence; similarly for ρ[j <_{I} i; R[j, s]];

[[R[i, t]]]_{ρ} = ((h′(F′′i^{∗}))′t^{∗} = [[η[R(i)/Ξ]]]_{ρ′} = [[η[i/k; t/w][R(i)/Ξ]]]_{ρ},

where ρ′ = ρ[i^{∗}/k, t^{∗}/w].

(5) If α is reduced to β, then [[α]]_{ρ}=[[β]]_{ρ}.

(6) An element of [[α]]_{ρ} can be regarded as a function if ι is regarded as a function of arity 0.

(7) If α is a type (a type-form without free parameters), then its interpretation is independent of assignment ρ. We write it as [[α]].

The proof is carried out in ZFC. It is a routine work, using transfinite induction along I^{∗} and induction on the construction of type-forms.

3 Term-forms and objects

The entity of a type is the collection of terms having that type. Similarly, the entity of a set is the collection of its elements. The system of term-forms (TRM) in Yasugi^{3} gives a substance to Type, and it is the purpose of this section to interpret each term-form with a function belonging to the image set of its type-form.

We first outline the definition of term-forms for the reader’s convenience.

Definition 3.1. (1) If either α is reduced to β or β is reduced to α, then α and β are said to be related. In this section, we restrict ourselves to regular type-forms, where a type-form is said to be regular if it does not contain any subtype of the form π({x}α; t). (Since this is immediately reduced to the related type-form α[t/x], such a restriction is not an essential one.)

(2) Term-forms are defined below. ϕ : α will express that term-form ϕ is of type-form α. If α and β are related, then we let ϕ : α imply ϕ : β. (2.1) For each n, n = 0, 1, 2, 3, ..., and for each β, X_{n}^{β} (the n-th variable of type-form β) is an atomic term-form. (2.2) ∗ is an atomic term-form and ∗:1. (2.3) A BL-term t of arity n (n = 0, 1, 2, 3, ...) is a term-form and t : {y_{1}}...{y_{n}}N,where y_{1}, ..., y_{n} are of arity 0. (2.4) If ϕ : γ, then λx.ϕ : {x}γ. If ϕ : γ, then λX_{n}^{β}.ϕ : β → γ, where the condition Γ(ϕ, β) below is assumed. Γ(ϕ, β) For each X_{n}^{β}, where β and δ are related, any free parameter x in δ occurring free in ϕ is not bound by λx in ϕ. (2.5) If ϕ : {x}γ, then app(ϕ; t) : γ[t/x]. If ϕ : β → γ and ψ : β, then app(ϕ; ψ) : γ.

We abbreviate these as ϕt and ϕψ respectively. (2.6) If ϕ : β and ψ : γ, then cond[A; ϕ, ψ] : cond[A; β, γ]. (2.7) If ϕ : R[j, s], then σ[j <_{I} i; ϕ] : ρ[j <_{I} i; R[j, s]].

(3) A term-form which has no free parameters is called a term.

(4) Conversion rules of term-forms are the following. (4.1) (λx.ϕ)t ⇒ ϕ[t/x]. (4.2) (λX_{n}^{β}.ϕ)ψ ⇒ ϕ[ψ/X_{n}^{δ}], where β and δ are related and X_{n}^{δ} is free in ϕ. (ψ is substituted for X_{n}^{δ} for any such X_{n}^{δ}.) (4.3) cond[A; ϕ, ψ] ⇒ χ, where χ is ϕ if A is a true sentence and χ is ψ if A is a false sentence. (4.4) σ[j <_{I} i; ϕ] ⇒ χ, where χ is ϕ if j <_{I} i is a true sentence and χ is ∗ if j <_{I} i is a false sentence.

(5) We can define “ϕ 1-reduces to ψ” and “ϕ is reducible to ψ” similarly to Definition 2.1, with the strategy that σ has priority of reduction.

(6) The collection of term-forms together with conversion rules will be denoted by Term.

Corollary. If ϕ : α and ϕ is reducible to ψ, then ψ : α.

Definition 3.2. Let ρ be as in Definition 2.3. We extend ρ to an assignment to term variables. That is, ρ(X_{n}^{β}) is an element of [[β]]_{ρ}. With such an extended assignment ρ, we define an interpretation of term-forms under assignment ρ. The interpretation of ϕ under ρ is denoted by [[ϕ]]_{ρ}. It will be defined so that if ϕ : α, then [[ϕ]]_{ρ} ∈ [[α]]_{ρ}, [[ϕ[t/x]]]_{ρ} = [[ϕ]]_{ρ[t∗/x]} and [[ϕ[ψ/X]]]_{ρ} = [[ϕ]]_{ρ[[[ψ]]_{ρ}/X]}. Recall that [[α]]_{ρ} is nonempty and that [[α]]_{ρ} = [[β]]_{ρ} if α and β are related. (See (3) and (5) of Proposition 2.1.)

(1) [[∗]]_{ρ} = ι; [[t]]_{ρ} = t*; [[X_{n}^{β}]]_{ρ} = ρ(X_{n}^{β}).

(2) [[λx.ϕ]]_{ρ} = ⟨[[ϕ]]_{ρ[f/x]}|f ∈ F_{n}⟩ if x is of arity n; [[λX_{n}^{β}.ϕ]]_{ρ} = Ψ, where Ψ′W = [[ϕ]]_{ρ[W/X_{n}^{β}]} for all W ∈ [[β]]_{ρ}.

(3) [[ϕt]]_{ρ} = [[ϕ]]′_{ρ}t*; [[ϕψ]]_{ρ} = [[ϕ]]′_{ρ}[[ψ]]_{ρ}.

(4) [[cond[A; ϕ, ψ]]]_{ρ} = a, where a is defined as follows. Let

D = {b|(A ⊃ b = [[ϕ]]_{ρ}) ∧ ((¬A ⊃ b = [[ψ]]_{ρ})}.

We can prove that there is a unique element in D. Then a is that unique element, and hence a satisfies that

(A ⊃ a = [[ϕ]]_{ρ}) ∧ (¬A ⊃ a = [[ψ]]_{ρ}).

[[σ[j <_{I} i; ϕ]]]_{ρ} = a, where a satisfies

(j <_{I} i ⊃ a = [[ϕ]]_{ρ}) ∧ (¬j <_{I} i ⊃ a = ι).

We can easily show the following.

Proposition 3.1. (1) The map [[ϕ]]_{ρ} is well-defined, satisfying the desired conditions.

(2) If ϕ is reducible to ψ, then [[ϕ]]_{ρ} = [[ψ]]_{ρ} (equal elements).

(3) If ϕ is a closed term (a term-form without free occurrences of parameters and variables), then the interpretation of ϕ is independent of assignment ρ. We write it as [[ϕ]].

Summing up the preceding results, we can state the conclusion.

Theorem 1. There is a natural set-theoretic interpretation of types and terms, denoted by [[ ]] such that, if ϕ is a term of type α, then [[ϕ]] is a function belonging to the set [[α]].

We can extend Term to a wider class of terms, still preserving the property in Theorem 1 above. We give an example of such.

Definition 3.3 (1) To Term above, we add the following. (1.1) A functional constant μ of type {f}N, where f is a unary function variable. (μ represents a modulus of finiteness functional of the order <_{I}.) (1.2) Bar recursion. Let b denote a functional evaluating a barred tree. If ϕ : {z}γ and ψ : {z}({s}[z∗s/z] → γ), then B[b; ϕ, ψ, m, f] : γ[f′′m/z],where m and f are BL−terms of arities respectively 0 and 1. The conversion rule for B is as follows.

B[b; ϕ, ψ, m, f] ⇒ app(ϕ; f′′m),

if bf ≤ m is a true sentence with b added to BL, and

B[b; ϕ, ψ, m, f] ⇒ B{m + 1},

if bf > m is a true sentence, where B{m + 1} abbreviates

app(app(ψ; f′′m); λkB[b; ϕ, ψ, m + 1, (f′′m) ∗ k]).

Reductions of thus extended term-forms can be defined similarly as before with the added strategy that B has priority.

(2) [[μ]]_{ρ} = μ; [[B[b; ϕ, ψ, m, f]]]_{ρ} = S, where S is obtained from the interpretaions of ϕ, ψ,m, f by an application of (informal) bar recursion.

The proposition below can be proved by using the bar induction.

Proposition 3.2. The map extended as above is well-defined, satisfying the desired properties.

4 From type-forms to admissible formulas

In Yasugi^{3} and Yasugi-Hayashi^{4}, we defined a map from “admissible” formulas to type-forms. Here we will show that a reverse map is possible.

Definition 4.1. (1) The language L is the language of Heyting arithmetic augmented by ∀f of function variables, constant symbols of BL and H a predicate constant (for definition by transfinite recursion along I).

L-formulas are defined as usual, where H(i, t) is an atomic formula. Here i is a BL-term of arity 0 which is supposed to denote an element of I and t is a BL-term. An L-formula is said to be admissible if H does not occur in the scope of ∃ and ∨. (Details are seen in Yasugi^{4}.) Formula will denote the collection of admissible formulas.

(2) A type-form π(α; t) where α is not of the form {x}β is said to be irrelevant. In the following, Type′ will denote the family of type-forms which are not irrelevant.

The map form from Type′ to Formula is defined as follows. (2.1) form(N) ≡ ∃x(x = x), where x is of arity 0; form(1) ≡ 0 = 1. (2.2) form(α → β) ≡ form(α) ⊃ form(β); form({x}α) ≡ ∀xform(α); form(π({x}α; t)) ≡ form(α)[t/x]; form(cond[A; α, β]) ≡ (A ⊃ form(α)) ∧ (¬A ⊃ form(β)). (2.3) form(R[i, t]) ≡ H(i, t); form(ρ[j <_{I} i; R[j, s]) ≡ (j <_{I} i ⊃ H(j, s)) ∧ (¬j <_{I} i ⊃ 0 = 1).

Proposition 4.1. (1) α and form(α) have the same free variables.

(2) form(α[t/x]) = form(α)[t/x].

Note. (1) The map from Formula to Type′ defined in Yasugi-Hayashi^{4} and the reverse map form are not mutual inverses, since the former crushes.

(2) The restriction of Type to Type′ (non-irrelevant type-forms) does not reduce the significance of our treatment, since an irrelevant type-form is either reduced to a non-irrelevant one or else it has no computational meaning.

5 From term-forms to proofs

The set of term-forms in whose formations only non-irrelevant type-forms are involved will be denoted by Term′. (See Definitions 3.1 and 4.1.) Here we define a map from Term′ to proofs. In what follows, the arguments goes through consistently with such restriction.

Definition 5.1. System S is Heyting arithmetic based on language L, as defined above, formulated in natural deduction, augmented by ∀−introduction and ∀ − elimination on function variables as well as the rules of transfinite recursion listed below. (We write ⟨A; B⟩ and ⟨P; B⟩ to denote respectively an inference which derives B from formula A and an inference to drive B from the conclusion of proof P.)

H − introduction ⟨G(i, t, H[i]); H(i, t)⟩
H − elimination ⟨H(i, t); G(i, t, H[i])⟩

G(i, t, H[i]) is an admissible formula (specified for S) and H[i] is an abstract (a meta-expression) of the form {j, b}((j <_{I} i ⊃ H(j, b))∧(¬j <_{I} i ⊃ 0 = 1)). (See, for example, Troelstra^{2} for arithmetic systems based on NJ. S is a subsystem of system TRDB in Yasugi-Hayashi^{4}.)

⟨A; ; B⟩ and ⟨P; ; B⟩ will denote a succession of inferences to obtain B respectively from A and P .

Proposition 5.1. If type-form α is reducible to β, then there is a proof of form(β) from assumption form(α) in S, and vice versa.

Proof. Consider conversion rules according to Definition 2.2, referring to Definitions 4.1 and 5.1. (1.2) Suppose, for example, A is a true sentence. Then A is a theorem of S. Since

form(cond[A; α, β]) ≡ (A ⊃ form(α)) ∧ (¬A ⊃ form(β)),

we can easily deduce form(α) from form(cond[A; α, β]). Conversely, this follows from form(α) and assumption ¬A. (1.4) Immediate from the rules on H.

Definition 5.2. Suppose ϕ ∈ Term′, α ∈ Type′ and ϕ : α. (See Definition 3.1. Recall that α is not unique.) We define prf(ϕ; α) as a proof in S which proves form(α) (possibly with live assumptions) when ϕ : α. (By virtue of Proposition 5.1, it suffices to define prf(ϕ; α) for a “typical” type-form α which ϕ belongs to.)

(1) prf(X_{n}^{β}; β) ≡ [n; form(β)] (the assumption form(β) with label n); prf(t; N) ≡ ⟨t = t; ∃x(x = x)⟩; prf(∗; 1) ≡ [0; 0 = 1] (the assumption 0 = 1 with label 0).

(2) Suppose t is of nary type, say ν. Then

prf(t; ν) ≡ ⟨ty_{1} … y_{n} = ty_{1} … y_{n}; ; ∀y_{1} … ∀y_{n}∃x(x = x)⟩.

(3) prf(λx.ϕ; {x}γ) ≡ ⟨prf(ϕ; γ); ∀xform(γ)⟩ (by ∀ − introduction)

(4) prf(λX_{n}^{α}.ϕ; α → β) is defined as follows. Let P be prf(ϕ; β), and let δ be related to α, where X_{n}^{δ} occurs free in ϕ. Let Q be constructed ¿from P by adding to it the proof of form(δ) from assumption [n; form(α)] for each such δ. (See Proposition 5.1.) Then the desired proof is ⟨Q; form(α) ⊃ form(β)⟩, where the inference is ⊃ −introduction.

(5) Suppose ϕ : {x}α and P ≡ prf(ϕ; {x}α). P proves form({x}α), which is ∀xF, where form(α) ≡ F. Now define prf(app(ϕ; t); α[t/x]) to be ⟨P; F [t/x]⟩ by ∀ − elimination. This makes sense since

F [t/x] ≡ form(α)[t/x] ≡ form(α[t/x])

by Proposition 4.1. (Notice that app(ϕ; t) can be formed only when ϕ : {x}α for some α. See (2.5) of Definition 3.1.) prf(app(ϕ; ψ); γ) is defined as

⟨prf(ψ; β), prf(ϕ; β → γ); form(γ)⟩

by ⊃ −elimination.

(6) prf(cond[A; ϕ, ψ]; cond[A; α, β]) is defined successively as follows, by ⊃ −introduction and ∧ − introduction. From prf(ϕ; α) and prf(ψ; β), we obtain A ⊃ form(α) and ¬A ⊃ form(β) respectively. From these we deduce (A ⊃ form(α)) ∧ (¬A ⊃ form(β)). We can add μ and B (See Definition

3.3) to prf-constructions.

Definition 5.3. (1) System TRDB is S augmented by the following. (1.1) Axiom W F (μ; I), which is a formula expressing that μ is a modulus of finiteness functional for <_{I}. (1.2) Bar induction BI ⟨∀z(R(z) ⊃ B(z)), ∀z(∀kB(z ∗ k) ⊃ B(z)); B(t)⟩ Here, z ∗ k = ⟨z_{1}, ..., z_{l}, k⟩ if z = ⟨z_{1}, ..., z_{l}⟩, t is a BL-term of arity 0 expressing a sequence number, B(z) is an admissible formula and R(z) is free of quantifiers and H. It is also assumed that ∀f∃nR(f′′n) and ∀u∀v((“v is an extension of u” ∧ R(u)) ⊃ R(v)).

(2) prf(μ; ν) ≡ W F (μ; I), where ν is the type of μ.

(3) Write Proof for the collection of proofs, either of S or of TRDB.

(4) Suppose ϕ : {z}γ, ψ : {z}({s}γ[z ∗ s/z] → γ)(≡ β), P ≡ prf(ϕ; {z}γ) proving ∀zC(z) and Q ≡ prf(ψ; β) proving ∀z(∀sC(z ∗ s) ⊃ C(z)). Then prf(B[b; ϕ, ψ, m, f]; γ[t/x]) is defined as follows. Let P′ be a proof of the formula ∀z(R(z) ⊃ C(z)) obtained from P . Then C(t) can be obtained from P′ and Q by BI. Let the entire proof be the desired one.

Note. (1) The relation between the bar induction and bar recursion is discussed in Yasugi-Hayashi^{4} in detail.

(2) A map from Proof to Term′ is investigated in Yasugi-Hayashi^{4}. This and prf are not mutual inverses.

Proposition 5.2. (1) prf(ϕ; α) is a proof of a sentence if and only if α is a type (a closed type-form).

(2) If ϕ does not contain ∗ and free occurrences of variables, then prf(ϕ; α) is a proof of form(α) without live assumptions.

Proposition 5.3. If ϕ : α and ϕ ⇒ ψ, then either (i) prf(ϕ; α) is reduced to prf(ψ; α), (ii) prf(ψ; α) is a part of prf(ϕ; α) or (iii) prf(ψ; α) is obtained from a part of prf(ϕ; α) with eliminations. (We do not elaborate with reductions of proofs. See, for example, Troelstra^{2} for reductions in a system formulated in natural deduction. )

Proof. (i) applies to (4.1) and (4.2) of Definition 3.1, (ii) applies to (4.3) and (4.4), and (iii) applies to bar recursion (Definition 3.3).

Summing up the results in Sections 4 and 5, we can state the following.

Theorem 2. There is a pair of maps from Type′ to Formula and from Term′ to Proof, say < form, prf >, such that, if ϕ : α, then prf(ϕ; α) is a proof of form(α).

References [1] W.A. Howard and G. Kreisel, Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis, J. Symbolic Logic 31(1966) 325-358.

[2] A. S. Troelstra, Mathematical investigations of intuitionistic arithmetic and analysis, Lecture Notes in Math. 344(Springer-Verlag, Berlin, 1973).

[3] M. Yasugi, Hyper-principle and the functional structure of ordinal diagrams, Comment. Math. Univ. St. Pauli 34(1985) 227-263(the opening part); 35(1986) 1-37(the concluding part).

[4] M. Yasugi and S. Hayashi, A functional system with transfinitely defined types and bar recursion, manuscript.