Inductive Definitions with Decidable Atomic Formulas

Anton Setzer ^{⋆}

Department of Mathematics, Uppsala University, P. O. Box 480, S-75106 Uppsala,

                      Sweden. email: setzer@math.uu.se

Abstract. We introduce a type theory for infinitely branching trees, called the theory of free algebras. In this type theory we define an extensional equality based on decidable atomic formulas only. We show, that equality axioms, which add full extensionality to the theory, yield a conservative extension of the (intensional) type theory for formulas having types of level ≤ 1. Types like nat → nat and well-founded trees with branching over the natural numbers (Kleene’s O) have this property. We can therefore extract constructive proofs and programs from classical proofs of Π_{2}-sentences with this restriction on the types.

1 Introduction

In a series of articles [Be93], [Be95], [BS95a], [BS95b], [BS96], [Sch91], [Sch92], [Sch93a], [Sch93b], [Sch94], [Sch95] Schwichtenberg and Berger have studied the extraction of programs from classical proofs. This method relies on the fact, that in Π_{1} assumptions, only decidable atomic formulas are used. When working in HA^{ω} we have no problems, since we can define an extensional equality easily based on decidable prime formulas.

Together with U. Berger, the author has introduced an extension of HA^{ω} by adding free algebras or well founded trees with branching over arbitrary types. This extension was necessary in order to treat term systems used for representing for instance non-deterministic terminating computation trees, infinitary term systems or, for implementations of proof theoretical techniques, infinitary formulas and proofs. The latter allows to extract programs from proof theoretical proofs and to work with infinitary logic in type theory. As expected, it turned out that some inductive definition can be defined directly in this theory and that we have the full proof theoretical strength of finitely iterated inductive definitions, as shown by the author ([Se94]).

To make use of this theory for the extraction of programs from classical proofs using equality, such an equality needs to be defined. Since we want to use

⋆ Part of this research was supported by the EU-supported Twinning Project “Proofs and Computation”, Leeds-Munich-Oslo. The research was written up, while the author, at that time based in Munich, was visiting the universities of Stockholm and Uppsala. The author wants to thank P. Martin-Löf for inviting him and making this fruitful visit possible and the logic group in Uppsala for providing such a creative and thoughtful environment.

such an equality in assumptions as well, we need an equality based on decidable prime formulas. In this article we show, that, such an equality can be defined in this extension and that we can prove it is extensional (however, we don’t have all equality axioms available).

The definition of the equality is quite transparent, and uses ideas the author developed for well-ordering proofs in [Se93], [Se95]: We define the type of branches in a free algebra which is a list of indices, where each index potentially leads to a subtree of a term in a free algebra. If t is a term of the free algebra and b is a branch, then we define t[b] to be the subtree reached following this branch to subtrees in t. Now t and t′ are equal, if at every branch b t[b] and t′[b] are locally equal: the constructors are the same and all labels are the same: t =_{σ} t′ ↔ ∀x^{branch(σ)}.loceq_{σ}(t[x], t′[x]). This definition is quite simple, and can be easily implemented.

However, the equality axioms can not be shown. This is no problem, since we can show, that adding such axioms yields a conservative extension of the original theory with respect to formulas using types of level ≤ 1 only.

The content of this article is as follows: In Sect. 2 we introduce the theory of free algebras FA. In order to make proofs easily, we restrict it to non simultaneous inductive definitions (and get the theory FA_{1}). The equality in FA_{1} is introduced in Sect. 3 and we show, that we have full extensionality. In Sect. 4 we introduce equality axioms. We then show, that these equality axioms can be cut out: adding the equality axioms yields a conservative extension of FA_{1} for formulas of type level ≤ 1. It follows, that adding to FA_{1} an extensional equality yields a conservative extension for these formulas, and that we can extract constructive proofs and programs from classical proofs of Π_{2}-sentences of this level using the extensional equality defined in this article.

Related work. The treatment of strictly positive inductive definitions by introducing labeled trees is used in many type systems. For instance C. Paulin-Mohring has introduced similar inductive structures in the system Coq ([PM93]). The W -type of Martin-Löf (see his book [ML84]) is very close to the free algebras, and Petersson and Synek have extended it to labeled trees (very well described in [NPS90], Chap. 16). U. Berger has in [Be94] given a treatment of non strictly positive inductive definitions as well. The treatment of an equality based on atomic prime formulas in such type systems is to our knowledge new.

Elimination of extensionality was first studied by R. Gandy ([Ga56], [Ga59]). Afterwards H. Luckhardt improved these results ([Lu73]). A very good treatment of elimination of extensionality in HA^{ω}, written by A. Troelstra and based on ideas of W. Howard can be found in [Tr73], pp. 155 ff.

2 Definition of Free Algebras

The idea of free algebras of the strength in consideration is to generalize the principle of free algebras to trees with infinite branching.

The usual definition of a free algebra σ is, that we have several constructors C_{i}, each of which has some type C_{i} : α_{1} → ⋯ → α_{n} → σ^{k} → σ.

The semantics of this free algebra is the least set of closed terms, closed under these constructors. Typical examples are:

– The type B of boolean truth values with constructors true : B, false : B.

– The type nat having constructors 0 : nat, S : nat → nat.

– The type with k elements \underline{n}_{k}, having constructors i_{k} : \underline{n}_{k} for i < k.

– If α_{1}, …, α_{n} are types, then α_{1} × ⋯ × α_{n} is defined by one constructor p_{α_{1},...,α_{n}} : α_{1} → ⋯ → α_{n} → (α_{1} × ⋯ × α_{n}).

– α_{1} + ⋯ + α_{n} is defined as the type having constructors i_{α_{1},...,α_{n},i} : α_{i} → (α_{1} × ⋯ × α_{n}) (i = 1, …, n).

– If α is a type, the type list(α) is defined by the constructors Nil_{α} : list(α), Cons_{α} : α → list(α) → list(α).

(We will use these types later and omit the index α in Nil and Cons, and α_{1}, …, α_{n} in p and i).

In applications we often define several algebras simultaneously. For instance, we can introduce set terms and set formulas by the following definition: Variables are terms, if r, s are terms, then {r, s} and r∪s are set terms, and if ϕ is a formula, a a set term, x a variable, then {x ∈ a | ϕ} is a set term. Formulas are r ∈ s for r, s set terms, and if ϕ, ψ are set terms, x a variable, then ϕ ∧ ψ, ϕ ∨ ψ and ∀x.ϕ are formulas. This can be defined (if representing variables as natural numbers) as the free algebra with the following constructors:

– Var : nat → term.

– {·} : term → term → term.

– ∪ : term → term → term.

– Separation : nat → term → for → term.

– ∈: term → term → for.

– ∧, ∨ : for → for → for.

– ∀ : nat → for → for.

This language has only limited expressiveness: nearly no comprehension is definable yet. In order to express at least restricted comprehension, we are immediately led to the idea of using infinitary formulas and terms: If ϕ_{n} is a formula for n : nat, then ⋀_{n:nat} ϕ_{n} is a formula, and if a_{n} is a set term for n : nat, then ⋃_{n:nat} a_{n} is a set term, and and we need constructors:

– ⋀ : (nat → for) → for.

– ⋃ : (nat → term) → term.

In order carry out some proof theoretical treatment of set theory in type theory, we need therefore free algebras with infinite branching.

In a theory using free algebras with infinitary branching, we can define for instance Kleene’s O with the constructors Nil : O, Succ : O → O, Lim : (nat → O) → O.

We can define trees with finite or countable branching, by forming lists of trees l : treelist and defining from l a tree Succtree(l) having as subtrees the elements of the list l:

– Nil : treelist,

– Cons_{tree} : tree → treelist → treelist,

– Succ_{tree} : treelist → tree.

– Lim : (nat → tree) → tree.

The general concept of forming free algebras is, that, if we have constructors, where the type to be defined occurs strictly positive, than we get a new type. The semantics of this type in the term model is the least set of closed terms closed under these constructors. A rigorous definition of free algebras, which does not make use of the adding of new symbols is as follows:

Definition 1 of the type theory FA. (a) We inductively define the \underline{set of} \underline{types} of FA: We first define the \underline{constructor types} together with their free variables: Let x_{i} for i ∈ N be special symbols. If α_{i}, τ_{i,j} are types, n ∈ ω, m_{i} ∈ ω, then

α_{1} → ⋯ → α_{n}

→ (τ_{1,1} → ⋯ → τ_{1,n_{1}} → x_{m_{1}}) → ⋯ → (τ_{k,1} → ⋯ → τ_{k,n_{k}} → x_{m_{k}})

→ x_{l}

is a constructor type with free variables {x_{m_{1}}, …, x_{m_{k}}, x_{l}}. Now, if ρ_{1}, …, ρ_{m} are constructor types, FV(ρ_{j}) ⊂ {x_{1}, …, x_{n}}, 1 ≤ j ≤ n, then

μx_{j}.μx_{1}. · · · μx_{j−1}.μx_{j+1}. · · · μx_{n}.(ρ_{1}, …, ρ_{m})

is a type. We call this type a \underline{free algebra}. If σ, τ are types, then (σ → τ) is a type. We have the usual conventions about omitting parenthesis.

(b) We define for every free algebra its \underline{constructors} together with the \underline{type of} \underline{each constructor}: If σ_{j} = μx_{j}.μx_{1}. · · · μx_{j−1}.μx_{j+1}. · · · μx_{n}.(ρ_{1}, …, ρ_{m}), then C(σ_{1}, …, σ_{n}, i) (1 ≤ i ≤ m) are the constructors of σ_{1}, …, σ_{n}. If

ρ_{i} = α_{1} → ⋯ → α_{n}

→ (τ_{1,1} → ⋯ → τ_{1,n_{1}} → x_{m_{1}}) → ⋯ → (τ_{k,1} → ⋯ → τ_{k,n_{k}} → x_{m_{k}})

→ x_{l} ,

then C(σ_{1}, …, σ_{n}, i) has type

α_{1} → ⋯ → α_{n}

→ (τ_{1,1} → ⋯ → τ_{1,n_{1}} → σ_{m_{1}}) → ⋯ → (τ_{k,1} → ⋯ → τ_{k,n_{k}} → σ_{m_{k}})

→ σ_{l} .

(c) In the following we will introduce free algebras (σ_{j})_{1≤j≤n} by giving names for σ_{j} together with names for their constructors (C_{i})_{1≤i≤m} and by giving the types ρ_{i} of the constructors C_{i}. In this situation we say, that \underline{(σ_{j})_{1≤j≤n}} \underline{are defined by the constructors (C_{i} : ρ_{i})_{1≤i≤m}}.

Functions can now be introduced by recursion over the definition of a free algebra. We could add the recursion operator. However, in a practical implementation in the proof assistant MINLOG, it turned out that one needs to add new functions which remain visible after normalization took place. Therefore we add functions defined by giving their step terms following the inductive definition of the free algebras. These functions will depend on terms.

Definition 2 of the terms of FA. (a) We define for every sequence of types γ⃗ = γ_{1}, …, γ_{n} and for simultaneously defined free algebras σ⃗ = σ_{1}, …, σ_{n} the \underline{step type for each constructor}: If σ_{i} is the free algebra, defined by the constructors C_{i} of type

C_{i} : α_{1} → ⋯ → α_{n}

→ (τ_{1,1} → ⋯ → τ_{1,n_{1}} → σ_{m_{1}}) → ⋯ → (τ_{k,1} → ⋯ → τ_{k,n_{k}} → σ_{m_{k}})

→ σ_{l} ,

the step type of C_{i} with respect to γ⃗ is

α_{1} → ⋯ → α_{n} → (τ_{1,1} → ⋯ → τ_{1,n_{1}} → σ_{m_{1}}) → ⋯ → (τ_{k,1} → ⋯ → τ_{k,n_{k}} → σ_{m_{k}}) → (τ_{1,1} → ⋯ → τ_{1,n_{1}} → γ_{m_{1}}) → ⋯ → (τ_{k,1} → ⋯ → τ_{k,n_{k}} → γ_{m_{k}})

→ γ_{l} .

(b) Inductive definition of the \underline{set of terms together with their type} (we write \underline{t : σ} or \underline{t^{σ}} for t is a term of type σ): Let for every type σ be infinitely many variables be given. We denote variables of type σ by x^{σ}, y^{σ}, . . .. If x is a variable of type σ, then x : σ. If s : σ → ρ, t : σ then (st) : ρ. If s : ρ, x a variable of type σ, then (λx.s) : σ → ρ. If C is a constructor of type α, C : α. If σ_{1}, …, σ_{n} are free algebras simultaneously defined by the constructors C_{1}, …, C_{m}, ρ⃗ = ρ_{1}, …, ρ_{n} is a sequence of types, β_{i} is the step type of C_{i} with respect to ρ⃗, t_{i} : β_{i}, then fun_{i}(C_{1} : t_{1}, …, C_{m} : t_{m}) is a term of type σ_{i} → ρ_{i}.

(c) We will write f(r_{1}, …, r_{n}) instead of f r_{1} ⋯ r_{n}, if f : γ_{1} → ⋯ γ_{n} → ρ. This does not cause any confusion with the product of terms, which is written as pr_{1}, …, r_{n} or in the new notation p(r_{1}, …, r_{n}).

(d) We define \underline{α-equality}, \underline{β-conversion} and \underline{η-conversion} as usual.

Further we define the \underline{one-step R-conversion} by:

If f_{i} := fun_{i}(C_{1} : t_{1}, …, C_{m} : t_{m}), and C_{i} of the type as in (a), then

f_{l}(C_{i}(l_{1}, …, l_{n}, s_{1}, …, s_{k})) →_{R}^{1}
t_{i}(l_{1}, …, l_{n}, s_{1}, …, s_{k},
(λx_{1}^{τ_{1,1}}. · · · λx_{n_{1}}^{τ_{1,n_{1}}} .f_{m_{1}}(s_{1}(x_{1}, …, x_{n_{1}}))), …,
(λx_{1}^{τ_{k,1}}. · · · λx_{n_{1}}^{τ_{k,n_{k}}} .f_{m_{k}}(s_{k}(x_{1}, …, x_{n_{k}}))))

for suitable variables x_{i}. Further if t →_{R}^{1} t′, then s[x := t] →_{R}^{1} s[x := t′]. Let \underline{≅} is the reflexive, symmetric and transitive closure of α- β, η conversion and →_{R}. We will in the following identify ≅-equivalent terms.

(e) We will usually introduce functions by giving their convertibility-rules.

All the examples of types mentioned above can now be defined in FA.

Formulas can now be formed from atom(t) for t : B (so atom(true) is the verum and atom(false) is the falsum) and we get a logic built on induction over free algebras:

Definition 3 of the logic in FA. (a) We define the \underline{formulas of FA}: If t : B, then atom(t) is an (atomic) formula. If ϕ_{1}, ϕ_{n} are formulas, x^{σ} a variable, then (ϕ_{1} → ϕ_{2}), (ϕ_{1} ∧ ϕ_{2}), (ϕ_{1} ∨^{∗} ϕ_{2}), (∀x^{σ}.ϕ_{1}), (∃^{∗}x^{σ}.ϕ_{1}) are formulas. Note, that we identify ≅-equivalent terms. We will introduce formulas in the form of ϕ(x) for some variable x. After having introduced it in this way, let ϕ(t) := ϕ[x := t].

(b) \underline{⊥} := atom(false), \underline{¬ϕ} := ϕ → ⊥.

(c) The \underline{rules of FA} are the rules of minimal logic (intuitionistic logic without ex falsum quodlibet) with the strong exist quantifier ∃^{∗}, strong disjunction ∨^{∗}, and an axiom atom(true). Additionally, we have the \underline{axioms of induction} over free algebras: Assume σ_{i} are free algebras, defined by the constructors C_{1} ⋯ C_{m}, C_{i} is of type as in Def. 2 (a) Then the \underline{induction step of C_{i} with respect to} \underline{ϕ_{1}(x^{σ_{1}}), …, ϕ_{n}(x^{σ_{n}})} is

∀x_{1}^{α_{1}}. · · · ∀x_{n}^{α_{n}}.∀y_{1}^{τ_{1,1}→···→τ_{1,n_{1}} →σ_{m_{1}}} . · · · ∀y_{k}^{τ_{k,1}→···→τ_{k,n_{k}} →σ_{m_{k}}} .
(∀z_{1}^{τ_{1,1}}. · · · ∀z_{n_{1}}^{τ_{1,n_{1}}} .ϕ_{m_{1}}(y_{1}(z_{1}, …, z_{n_{1}}))) → ⋯
→ (∀z_{1}^{τ_{k,1}}. · · · ∀z_{n_{k}}^{τ_{k,n_{k}}} .ϕ_{m_{k}}(y_{k}(z_{1}, …, z_{n_{k}})))
→ ϕ_{l}(C_{i}(x_{1}, …, x_{n}, y_{1}, …, y_{k})) .

If now ψ_{1}, …, ψ_{m} are the induction steps of C_{1}, …, C_{m} with respect to the formulas ϕ_{i} as above, then

ψ_{1} → ⋯ → ψ_{m} → ((∀x^{σ_{1}}.ϕ_{1}(x^{σ_{1}})) ∧ ⋯ ∧ (∀x^{σ_{n}}.ϕ_{n}(x^{σ_{n}})))

is an axiom of FA.

\underline{Proofs in FA} are formed by the axioms using the rules. Each proof has a \underline{set of free assumptions} and a \underline{set of free variables}. (The free variables are the free (object-)variables in corresponding Curry-Howard terms, i.e. the free variables in the terms used for ∀-elimination and ∃^{∗}-introduction, not bound later by ∀-introduction and ∃^{∗}-elimination). \underline{Closed proofs} are proofs that contain no free assumptions and only free variables occurring in the derived formula.^{2}

Note, that we have ex falsum quodlibet and stability for atomic formulas by induction over B, and therefore ex falsum quodlibet for all formulas, and stability for all formulas, which have no occurrence of ∨^{∗} or ∃^{∗}.

We can simplify the free algebras by reducing simultaneous inductive definitions to non simultaneous ones. This is done by not distinguishing between the types defined before simultaneously: If σ_{1}, …, σ_{n} are free algebras, defined by the constructors C_{1}, …, C_{m}, let σ be a free algebra defined by the constructors C′_{1}, …, C′_{m}, where, if C_{i} is of type as in Def. 2 (a),

C′_{i} : α_{1} → ⋯ → α_{k}

→ (τ_{1,1} → ⋯ → τ_{1,n_{1}} → σ) → ⋯ → (τ_{r,1} → ⋯ → τ_{r,n_{r}} → σ) → σ .

We define f_{σ_{i},σ} : σ_{i} → σ by

f_{σ_{l},σ}(C_{i}(l_{1}, …, l_{k}, s_{1}, …, s_{r})) ≅
C′_{i}(l_{1}, …, l_{k}, (λx_{1}. · · · x_{n_{1}}.f_{σ_{m_{1}} ,σ}(s_{1}(x_{1}, …, x_{n_{1}}))), …,
(λx_{1}. · · · x_{n_{r}}.f_{σ_{mr} ,σ}(s_{1}(x_{1}, …, x_{n_{r}})))) .

We can reduce the equality on σ_{i} to the equality on the type σ by applying f_{σ_{i},σ}.

Further, we can replace τ_{i,1} → ⋯ → τ_{i,m_{i}} → σ by (τ_{i,1} × ⋯ × τ_{i,m_{i}}) → σ, if m_{i} ≥ 1, and define again an embedding. (We could reduce it even more, but this would lead to case distinctions, which are more complicated to deal with).

Therefore, it suffices to study in the following the following set of types:

Definition 4 of the type theory FA_{1}. (a) We define the \underline{set of types of FA_{1}} as a subset of FA:

2 In the theories usually considered, every type is inhabited and we can replace free

variables occuring in the proof and not occuring in free assumptions or the derived

formula always by closed terms of the corresponding type, therefore the set of vari-

ables can be neglected. FA has empty types, and we have to take care of the free

variables. Independently R. Stärk and the unknown referee – we would like to thank

both for their comments – pointed out, that there are proofs of ⊥ in FA: take the

induction axiom ∀x^{\underline{n}^{0}}.⊥, where \underline{n}_{0} is the empty type with no constructors, and use

an ∀-elimination with the term x^{\underline{n}^{0}}. However, this proof depends on the free variable

x^{\underline{n}^{0}}, is therefore not closed – the consistency of FA is not violated.

Assume σ is a free algebra, defined by constructors C_{i}, s.t. each constructor C_{i} has type

α_{1}^{i} → ⋯ → α_{m_{i}}^{i}
→ (τ_{1}^{i} → σ) → ⋯ → (τ_{n_{i}}^{i} → σ) → σ^{p_{i}} → σ ,

where σ^{p_{i}} → σ abbreviates \underbrace{σ → ⋯ → σ}_{p_{i}times} → σ and α_{j}^{i}, τ_{j}^{i} are types of FA_{1}.

Then σ is a type of FA_{1}.

If σ, ρ are types of FA_{1}, then (σ → ρ) is a type of FA_{1}.

(b) If C_{i} has the type as in (a), the arguments of type α_{j}^{i} will be denoted by l_{j} (for label), of type τ_{j}^{i} → σ by s_{j} and the remaining arguments by t_{j}, all possibly with accents etc. We denote the arguments by r_{j}, if we don’t care about the distinction between the groups of arguments. Further let in the following, as arguments of C_{i}, l⃗ = (l_{1}, …, l_{m_{i}}), s⃗ = (s_{1}, …, s_{n_{i}}), t⃗ = (t_{1}, …, t_{p_{i}}), l⃗′ = (l′_{1}, …, l′_{m_{i}}), etc.

(c) \underline{Terms}, \underline{formulas of FA_{1}} are the terms, formulas of FA which contain only FA_{1}-types. The \underline{rules} and \underline{axioms of FA_{1}} are those of FA which use only FA_{1}-types.

(d) In the following, if not mentioned differently, C_{i} will have the type as denoted in Def. (a).

3 Definition of the Equality

As we noted in the introduction, the equality for free algebras is defined as: t =_{σ} t′ if t[b] and t′[b] are locally equal, for every branch b. Local equality means, that the last constructor is the same and the labels on t[b] and t′[b] are the same. Now the labels at t[b], t[b′] depend on the constructor used. Since we have no dependent types, we need to extract a label, even, if the last constructor does not contain such a label. We deal with this problem by deciding, whether a type is empty or not. If it is empty, we do not need to extract a label of that type. If it is non empty, we have one fixed element, and use, in case the constructor contains no label, this fixed element (ϵ^{σ}) as the result of the label-extracting function.

Definition 5 of E^{σ→ρ} and ϵ^{ρ}. For each type of FA_{1} we define, \underline{whether it is} \underline{empty or not}, and define if σ is non empty, a closed term \underline{ϵ^{σ}} and if σ is empty, for each type ρ a closed term \underline{E^{σ→ρ}} (E stands for ex falsum quodlibet), and a proof of ∀x^{σ}.ϕ(x) for any formula ϕ(x^{σ}): Case σ is a free algebra, defined by constructors C_{i}: If for one constructor C_{i} we have for all j α_{j}^{i} are non empty, τ_{j}^{i} are empty, p_{i} = 0, then σ is non empty. If i is minimal such that C_{i} is such a constructor, then

ϵ^{σ} := C_{i}(ϵ^{α_{1}^{i}}, …, ϵ^{α_{m_{i}}^{i}} , E^{τ_{1}^{i}→σ}, …, E^{τ_{n_{i}}^{i} →σ}) .

Otherwise σ is empty, and we define E^{σ→ρ} as the function σ → ρ such that if C_{i} has a type as above,

E^{σ→ρ}(C_{i}(l⃗, s⃗, t⃗) ≅

E^{α_{j}^{i}→ρ}(l_{j})  if α_{j}^{i} is empty, j minimal,
E^{σ→ρ}(s_{j}(ϵ^{τ_{j}^{i}})) otherwise, if τ_{j}^{i} is non empty, j miminal,
E^{σ→ρ}(t_{1})  otherwise.

Case σ → τ: If σ is empty, σ → τ is non empty, ϵ^{σ→τ} := E^{σ→τ}. Otherwise, if τ non empty, then σ → τ is non empty, ϵ^{σ→τ} := λx^{σ}.ϵ^{τ}. Otherwise σ → τ is empty, E^{(σ→τ)→ρ} := λx^{σ→τ} .E^{τ→ρ}(x(ϵ^{σ})).

The proofs of ∀x^{σ}.ϕ(x) for σ empty can be defined in a similar way as E^{σ→ρ}, replacing recursion by induction.

We define now the equality on the types. Free algebras, hereditarily built from free algebras with no branching over types, have decidable equality, which we can define as a boolean valued function by recursion over the type:

Definition 6 of the decidable equality. We define inductively the \underline{set of} \underline{types σ with decidable equality} together with \underline{=_{σ}^{B}: σ → σ → B} (usually written infix). If σ is empty, then σ has decidable equality, =_{σ}^{B}:= λx, y.true. If σ is a non empty free algebra, defined by constructors C_{i}, such that, for each constructor C_{i} of the usual typing n_{i} = 0 and for all j α_{j}^{i} has decidable equality, then σ has decidable equality, and we define =_{σ}^{B} by

C_{i}(r⃗) =_{σ}^{B} C_{j}(r′) ≅ false if i ≠ j ,

and

C_{i}(l⃗, t⃗) =_{σ}^{B} C_{i}(l⃗′, t⃗′)
≅ l_{1} =_{α_{1}^{i}}^{B} l′_{1} ∧_{B} ⋯ ∧_{B} l_{m_{i}} =_{α_{m_{i}}^{i}}^{B} l′_{m_{i}} ∧_{B} t_{1} =_{σ}^{B} t′_{1} ∧_{B} ⋯ ∧_{B} t_{p_{i}} =_{σ}^{B} t′_{p_{i}} .

where \underline{∧_{B}} is the boolean valued function corresponding to the logical connective ∧.

The crucial case are free algebras with branching indexed over types. For these trees we define index(σ) as the union of all types, over which we can reach an immediate subtree. We can define for non empty types its immediate predecessor with respect to an element of index(σ). branch(σ) is the list of indices, and by induction over this list we reach every subtree:

Definition 7 of label, constr, pred, r[b], index, branch(σ), ι, ν. Assume σ is defined by constructors C_{1}, …, C_{m} with the usual typing and non empty.

(a) If α_{j}^{i} is non empty (1 ≤ i ≤ m, 1 ≤ j ≤ m_{i}) we define \underline{label_{i,j}^{σ}} : σ → α_{j}^{i} as

label_{i,j}^{σ}(C_{k}(l⃗, s⃗, t⃗)) ≅ \{ \begin{matrix}l_{j} & if i = k \\ ϵ^{α_{j}^{i}} & otherwise. \end{matrix}

(b) If 1 ≤ i ≤ m, define \underline{constr_{i}}^{σ} : σ → B,

constr_{i}^{σ}(C_{j}(r⃗)) ≅ \{ \begin{matrix}true & if i = j \\ false & otherwise . \end{matrix}

(c) Let \underline{index(σ)} be the free algebra defined by constructors \underline{ι_{i,j}^{σ}} : τ_{j}^{i} → index(σ) (1 ≤ i ≤ m, 1 ≤ j ≤ n_{i}), and \underline{ν_{i,j}^{σ}} : index(σ) (1 ≤ i ≤ m, 1 ≤ j ≤ p_{i}), i.e. index(σ) is the disjoint union of τ_{j}^{i}, and of a type with one element for 1 ≤ i ≤ m, 1 ≤ j ≤ p_{i}.

(d) Define the function \underline{pred^{σ}} : σ → index(σ) → σ, assigning the immediate subtree of a tree t^{σ}, indexed by l : index(σ) as follows: If s := C_{i}(l⃗, s⃗, t⃗), then

pred^{σ}(s, ι_{i′,j}(r)) ≅ \{ \begin{matrix}s_{j}(r) & if i = i′ \\ ϵ^{σ} & otherwise, \end{matrix}
pred^{σ}(s, ν_{i′,j}) ≅ \{ \begin{matrix}t_{j} & if i = i′ \\ ϵ^{σ} & otherwise. \end{matrix}

(e) Let \underline{branch(σ)} := list(index(σ)).

(f) Define \underline{·[·]}^{σ} : σ → branch(σ) → σ, written as s[b]^{σ} for ·[·]^{σ}(s, b), such that

s[Nil]^{σ} ≅ s
s[Cons(i, b)]^{σ} ≅ pred_{σ}(s, i)[b] .

We will usually omit the superscript σ in all constructors and functions defined above.

Two trees are equal, if the subtrees reached using the same branch are locally equal. Locally equal means, that the constructors are the same and the labels are the same:

Definition 8 of the equality \underline{=_{σ}} on the type σ. The definition is by recursion on definition of σ.

– Case σ has decidable equality. Then s =_{σ} t := atom(s =_{σ}^{B} t).

– Case σ is a free algebra with non decidable equality, defined by constructors C_{i} with the usual typing:

• If s : σ, t : σ, then \underline{loceq_{σ}(s, t)} (local equality) is the formula, which is the conjunction of label_{i,j}^{σ}(s) =_{α_{j}^{i}} label_{i,j}^{σ}(t) for 1 ≤ i ≤ m, 1 ≤ j ≤ m_{i}, τ_{j}^{i} non empty and constr_{i}(s) =_{B} constr_{i}(t) (1 ≤ i ≤ m).

• s =_{σ} t := ∀x^{branch(σ)}.loceq_{σ}(s[x], t[x]).

– Case σ = ρ → τ, with non decidable equality: s =_{σ} t := ∀x^{ρ}.s(x) =_{τ} t(x).

Theorem 9. We can prove the following in FA_{1}:

(a) =_{σ} is reflexive, symmetric and transitive.

(b) If σ is defined by constructors C_{i}, j ≠ l, then ¬(C_{j}(r⃗) =_{σ} C_{l}(s⃗)).

(c) If σ is defined by constructors C_{i}, r_{i}, r′_{i} : σ_{i}, then

C_{i}(r_{1}, …, r_{k}) =_{σ} C_{i}(r′_{1}, …, r′_{k}) ↔ (r_{1} =_{σ_{1}} r′_{1} ∧ ⋯ ∧ r_{k} =_{σ_{k}} r′_{k}) .

Proof. (a) Immediate by Meta-induction on the types.

(b) Trivial.

(c) The case, where σ has decidable equality is immediate. Non decidable case: Let s := C_{i}(r⃗) =: C_{i}(l⃗, s⃗, t⃗), s′ := C_{i}(r′) =: C_{i}(l⃗′, s′, t⃗′). Then loceq(s[Nil], s′[Nil]) iff l_{j} = l′_{j} for 1 ≤ j ≤ m_{i}. If u : τ_{j}^{i}, x : branch(σ), then

loceq(s[Cons(ι_{i,j}(u), x)], s′[Cons(ι_{i,j}(u), x)]) ↔ loceq((s_{j}(u))[x], (s′_{j}(u))[x])

for k ≠ i,

loceq(s[Cons(ι_{k,j}(u), x)], s′[Cons(ι_{k,j}(u), x)]) ↔ loceq(ϵ^{σ}[x], ϵ^{σ}[x])

where the right side holds by reflexivity. We have similar statements for s[Cons(ν_{k,j}, x)] and it follows

∀x^{branch(σ)}loceq(s[x], s′[x])

↔ ⋀_{1≤j≤m_{i}} l_{j} =_{α_{j}^{i}} l′_{j} ∧ ⋀_{1≤j≤n_{i}} ∀u^{τ_{j}^{i}}∀x^{branch(σ)}loceq(s_{j}(u)[x], s′_{j}(u)[x])∧

⋀_{1≤j≤p_{i}} ∀x^{branch(σ)}loceq(t_{j}[x], t′_{j}[x])

↔ l⃗ = l⃗′ ∧ s⃗ = s′ ∧ t⃗ = t⃗′ .

4 Equality Axioms

In order to make use of our equality, we need equality axioms, which are not provable in FA_{1} (or at least this should be the case by extending proofs for HA^{ω}). We show, that FA_{1} − Eq is conservative over FA_{1} for formulas with no occurrences of types of level ≥ 2 (we could allow negative occurrences of ∀x^{σ} and positive occurrences of ∃^{∗}x^{σ} for level(σ) ≥ 2).

Definition 10 of FA_{1} − Eq. Let \underline{FA_{1} − Eq} be defined as FA_{1}, but with the additional \underline{axioms for the extensional equality}: For any types ρ, σ:

∀x^{ρ}, y^{ρ}, z^{ρ→σ}.x =_{ρ} y → z(x) =_{σ} z(y) .

For proving our conservativity result, we will follow the approach we found in [Sch94], pp. 52 – 53 for the case of the typed lambda calculus and which again goes back to [Tr73], pp. 155 ff., and adapt it to the situation of free algebras.

The method used, is to define the formula r ∼_{σ} s meaning: r and s are hereditarily extensional equal. If ϕ^{∼} is the result of restricting a quantifier ∀x and ∃^{∗}x to x ∼ x, we can show, that if FA_{1} − Eq ⊢ ϕ, then FA_{1} ⊢ ϕ^{∼}. Now for formulas having the restriction to types of level ≤ 1, ϕ ↔ ϕ^{∼} is provable in FA_{1} and we are done.

Definition 11 of ∼. We define \underline{r ∼_{σ} s} for every type σ, and r, s : σ by recursion on the definition of the types: If σ has decidable equality, then r ∼_{σ} s := r =_{σ} s. Assume now σ has a non decidable equality. If σ is a free algebra defined by constructors C_{i} with the usual typing, then let loceq_{σ}^{∼}(s, t) be the conjunction of label_{i,j}^{σ}(s) ∼_{α_{j}^{i}} label_{i,j}^{σ}(t) for 1 ≤ i ≤ m, 1 ≤ j ≤ m_{i}, τ_{j}^{i} non empty and constr_{i}(s) ∼_{B} constr_{i}(t) (1 ≤ i ≤ m).

s ∼_{σ} t := ∀x^{branch(σ)}, y^{branch(σ)}.x ∼_{branch(σ)} y → loceq_{σ}^{∼}(s[x], t[y]) .

If σ = ρ → τ, then

t ∼_{σ} t′ := (∀x^{ρ}, y^{ρ}.x ∼_{ρ} y → tx ∼_{τ} t′y) .

Remark. More precisely, in the above definition we have to proceed as follows, since branch(σ) is in general more complex than σ: index(index(σ)) has no constructors, therefore decidable equality, therefore as well branch(index(σ)) = list(index(index(σ))), and then we can define ∼_{branch(index(σ))} and, using ∼_{τ_{i,j}}, ∼_{index(σ)}. index(branch(σ)) has only constructors ν_{i′,j′}^{branch(σ)} : index(branch(σ)), therefore decidable equality, therefore as well branch(branch(σ)), and we get a definition of ∼_{branch(branch(σ))} and, using ∼_{index(branch(σ))} as well of ∼_{branch(σ)}. Now we can define ∼_{σ}.

Lemma 12. ∼_{σ} is symmetric and transitive.^{3}

Proof. easy.

Definition 13 of level of types, N- and P-formulas. (a) We define the \underline{level} of types \underline{level(σ)} by recursion on the inductive definition of the type σ: If σ has decidable equality, then level(σ) := 0. If σ is a free algebra with non decidable equality, defined by the constructors C_{i}, typed as usual, then

level(σ) := max{level(α_{j}^{i}) | 1 ≤ i ≤ m, 1 ≤ j ≤ m_{i}}
∪{level(τ_{j}^{i}) + 1 | 1 ≤ i ≤ m, 1 ≤ j ≤ n_{i}} .

3 Note that reflexivity of ∼_{σ} is not provable. By symmetry and transitivity follows x ∼_{σ} y → x ∼_{σ} x

If σ = ρ → τ with non decidable equality, then

level(σ) := max{level(ρ) + 1, level(τ)} .

(b) We define the \underline{P-} and \underline{N-formulas}:

atom(r) is a P and an N-formula.

If ϕ, ψ are P (N-)formulas, then ϕ ∧ ψ, ϕ ∨^{∗} ψ are P- (N-)formulas.

If ϕ is a P- (N-), ψ is an N- (P-)formula, then ψ → ϕ is a P- (N-)formula. If ϕ is a P-formula then ∃^{∗}x^{σ}ϕ is a P-formula, and, if level(σ) ≤ 1, ∀x^{σ}.ϕ is a P-formula. If ϕ is an N-formula then ∀x^{σ}.ϕ is an N-formula, and, if level(σ) ≤ 1, ∃^{∗}x^{σ}.ϕ is an N-formula.

Lemma 14. If σ has decidable equality, τ is a type, then ∀x^{σ}, y^{σ}.x =_{σ} y → ∀f^{σ→τ} .((∀z^{σ}.f(z) ∼_{τ} f(z)) → f(x) ∼_{τ} f(y)).

Proof by Meta-induction on the definition of the types. If σ is empty, this follows immediately. If σ is a free algebra, defined the constructors C_{i} with usual typing, α_{j}^{i} have decidable equality, n_{i} = 0, we show the assertion by induction on x^{σ}, side-induction on y^{σ}. Assume x ≡ C_{i}(l⃗, t⃗), l_{i} =_{α_{j}^{i}} l′_{i}, t_{i} =_{σ} t′_{i} and assume the assertion for t_{i}. Let

g_{j} := λx_{j}^{α_{j}^{i}}.f(C_{i}(l′_{1}, …, l′_{j−1}, x_{j}, l_{j+1}, …, l_{m_{i}}, t_{1}, …, t_{p_{i}})) ,
h_{j} := λx_{j}^{σ}.f(C_{i}(l′_{1}, …, l′_{m_{i}}, t′_{1}, …, t′_{j−1}, x_{j}, t_{j+1}, …, t_{p_{i}})) .

By Meta-IH we have g_{j}(l_{j}) ∼_{τ} g_{j}(l′_{j}) and by IH for t_{j}, h_{j}(t_{j}) ∼_{τ} h_{j}(t′_{j}). By the transitivity of ∼ follows the assertion.

It causes slight technical problems that r ∼_{σ} s depends on r ∼_{branch(σ)} s, where branch(σ) is in general more complicated than σ. In the following lemma we overcome this difficulty:

Lemma 15. (a) Assume σ with non decidable equality, σ be defined by constructors C_{i} with the usual typing, ϵ^{α_{j}^{i}} ∼_{α_{j}^{i}} ϵ^{α_{j}^{i}}, if α_{j}^{i} is non empty. Then

∀x^{branch(σ)}.loceq_{σ}^{∼}(ϵ^{σ}[x], ϵ^{σ}).

(b) For all non empty types σ, ϵ^{σ} ∼ ϵ^{σ}, and for all empty types σ and all types ρ, E^{σ→ρ} ∼ E^{σ→ρ}.

(c) If branch(σ) has decidable equality, then r ∼_{σ} r′ ↔ ∀x^{branch(σ)}.loceq_{σ}^{∼}(r[x], r′[x]).

(d) Assume σ defined by constructors C_{i} with usual typing. Then

ι_{i,j}(r) ≁_{index(σ)} ι_{i′,j′}(r′) , if i ≠ i′ ∨ j ≠ j′,
ι_{i,j}(r) ∼_{index(σ)} ι_{i,j}(r′) ↔ r ∼_{τ_{j}^{i}} r′ ,
ν_{i,j} ≁_{index(σ)} ν_{i′,j′} , if i ≠ i′ ∨ j ≠ j′.
ν_{i,j} ∼_{index(σ)} ν_{i,j} .

(e) Assume σ defined by constructors C_{i} with usual typing. Then

Nil ∼_{branch(σ)} Nil , Nil ≁_{branch(σ)} Cons(i, b) ,
Cons(i, b) ∼_{branch(σ)} Cons(i′, b′) ↔ i ∼_{index(σ)} i′ ∧ b ∼_{branch(σ)} b′ .

Proof. (a) ϵ^{σ} = C_{i}(ϵ^{α_{1}^{i}}, …, ϵ^{α_{m_{i}}^{i}} , E^{τ_{1}^{i}→σ}, …, E^{τ_{n_{i}}^{i} →σ}), α_{j}^{i} non empty, τ_{j}^{i} empty. Induction on x^{branch(σ)}. If x ≡ Nil, the assertion is trivial. If x ≡ Cons(i, b), then if i ≡ ι_{j}^{i}(s) with s : τ_{j}^{i}, then by τ_{j}^{i} empty we get the assertion. Otherwise ϵ[x] ≅ ϵ[b] and the assertion follows by IH.

(b) E^{σ→τ} ∼ E^{σ→τ} follows from the emptiness of σ. Proof of ϵ_{σ} ∼ ϵ_{σ} by Meta-induction on the definition of types: If σ has decidable equality, the assertion follows by reflexivity of =_{σ}. If σ is a free algebra, the assertion follows by the symmetry and transitivity of loceq_{σ}^{∼} and (a). If σ = ρ → τ, ρ is empty, ϵ^{σ} ≡ E^{ρ→τ} ∼ E^{ρ→τ} ≡ ϵ^{σ}, and if ρ is non empty, τ is non empty, follows for all x, y : ρ, ϵ^{σ}(x) ≅ ϵ^{τ} ∼ ϵ^{τ} ≅ ϵ^{σ}(y).

(c) “→” follows by the reflexivity of ∼_{branch(σ)}≡=_{branch(σ)}. “←”: Assume x ∼ y, i.e. x = y, ∀x^{branch(σ)}.loceq_{σ}^{∼}(r[x], r′[x]). Then

∀x^{branch(σ)}.label_{i,j}(r[x]) ∼ label_{i,j}(r′[x]) ,

by Lemma 14

label_{i,j}(r[x]) ∼ label_{i,j}(r′[y]) .

Similarly constr_{i}(r[x]) ∼ constr_{i}(r′[y]), loceq_{σ}^{∼}(r[x], r′[y]).

(d) and (e) follow using (b) and (c), since the types branch(index(σ)) and branch(branch(σ)) have decidable equality.

Now we are ready, to characterize ∼_{σ} similarly to the characterization of =_{σ} before:

Lemma 16. Assume σ is a free algebra defined by constructors C_{i} with usual typing.

(a) If i ≠ j, then C_{i}(r⃗) ≁_{σ} C_{j}(r′).

(b) Let r := C_{i}(l⃗, s⃗, t⃗), r′ := C_{i}(l⃗′, s′, t⃗′). Then

r ∼_{σ} r′ ↔ ⋀_{j=1}^{m_{i}} l_{j} ∼ l′_{j} ∧ ⋀_{j=1}^{n_{i}} s_{j} ∼ s′_{j} ∧ ⋀_{j=1}^{p_{i}} t_{j} ∼ t′_{j} .

Proof. If σ has decidable equality the assertions are easy. (a): easy. (b): “→”: Nil ∼ Nil, loceq^{∼}(r[Nil], r′[Nil]), l_{i} ∼ l_{i}. Further, if b ∼_{branch(σ)} b′, y ∼_{τ_{j}^{i}} y′, then Cons(ι_{i,j}(y), b) ∼ Cons(ι_{i,j}(y′), b′), r[Cons(ι_{i,j}(y), b)] ≅ (s_{j}(y))[b], loceq^{∼}(r[Cons(ι_{i,j}(y), b)], r′[Cons(ι_{i,j}(y′), b′)]), loceq^{∼}(s_{j}(y)[b], s′_{j}(y′)[b′]), s_{j}(y) ∼ s′_{j}(y′), s_{j} ∼ s′_{j}, similarly follows t_{j} ∼ t′_{j}.

“←”: By induction on branch(σ) we show x ∼ y → loceq^{∼}(r[x], r′[y]).

Lemma 17. If level(σ) ≤ 1, then ∀x^{σ}.x ∼ x.

Proof by Meta-induction on the types. If σ has decidable equality, this is trivial. If σ is a free algebra defined by constructors C_{i} with usual typing, we use induction on x : σ, and have in case x ≡ C_{i}(l_{1}, …, l_{m_{i}}, s_{1}, …, s_{n_{i}}, t_{1}, …, t_{p_{i}}), l_{i} ∼ l_{i} by Meta-IH, by IH ∀x^{τ_{j}^{i}}.s_{j}(x) ∼ s_{j}(x), therefore by Lemma 14 s_{j} ∼ s_{j}, by IH t_{j} ∼ t_{j}, by Lemma 16 (b) x ∼ x. If σ = ρ → τ follows for x : σ, by IH ∀y^{ρ}.x(y) ∼ x(y) and by Lemma 14 x ∼ x.

Lemma 18. If r(x⃗) := r[z⃗ := x⃗], FV(r) ⊂ {z_{1}, …, z_{n}}. Then ∀x⃗, y⃗.x⃗ ∼ y⃗ → r(x⃗) ∼ r(y⃗).

Proof by Meta-induction on the definition of the terms. Case r = C_{i} constructor: by Lemma 16 (b). Case r = f^{σ→τ} function defined from step terms r_{i}. Assume x⃗, y⃗, x⃗ ∼ y⃗ and let g := f[z⃗ := x⃗], g′ := f[z⃗ := y⃗], t̃_{i} := r_{i}[z⃗ := x⃗], t̃′_{i} := r_{i}[z⃗ := y⃗]. We show ∀x^{σ}, y^{σ}.x ∼ y → g(x) ∼ g′(y) by induction on x, y : σ. Case x ≡ C_{i}(l⃗, s⃗, t⃗), y ≡ C_{i}(l⃗′, s′, t⃗′).

g(x) ≅ t̃_{i}(l⃗, s⃗, t⃗, (λx.g(s_{1}(x))), …, (λx.g(s_{n_{i}}(x))), g(t_{1}), …, g(t_{p_{i}})) .

l_{i} ∼ l′_{i}, s_{i} ∼ s′_{i}, t_{i} ∼ t′_{i}, and if u ∼_{τ_{j}^{i}} u′, then s_{j}(u) ∼ s′_{j}(u′), by IH g(s_{j}(u)) ∼ g′(s′_{j}(u′)), therefore λx.g(s_{j}(x)) ∼ λx.g′(s′_{j}(x)), further by IH g(t_{j}) ∼ g′(t′_{j}), by Meta-IH t̃_{i} ∼ t̃′_{i}, g(x) ∼ g′(y). Case r an application or λ-abstraction: easy.

Definition 19 of ϕ^{∼} and ∼′_{σ}. (a) Let for ϕ a formula, \underline{ϕ^{∼}} be the result of binding all quantifiers ∀, ∃^{∗} by ∼: (∀x.ϕ)^{∼} := ∀x.x ∼ x → ϕ^{∼}, (∃^{∗}x.ϕ)^{∼} := ∃^{∗}x.x ∼ x ∧ ϕ^{∼}, and for other formula constructions ϕ^{∼} is the result of applying this operation to its components.

(b) \underline{r ∼′_{σ} s} := (r =_{σ} s)^{∼}.

Lemma 20. (a) Lemmata 15 and 16 follow with ∼ replaced by ∼′, loceq_{σ}^{∼}(r, s)

replaced by (loceq_{σ}(r, s))^{∼}.

(b) ∀x^{σ}, y^{σ}.x ∼_{σ} x → y ∼_{σ} y → (x ∼_{σ} y ↔ (x =_{σ} y)^{∼}).

(c) (∀x, y, z.x =_{σ} y → (z(x) =_{τ} z(y)))^{∼}.

Proof. (a) easy.

(b) Meta-induction on the definition of the types. If σ has decidable equality, the assertion is trivial. If σ is a free algebra defined by constructors C_{i}, show the assertion by induction on x, y : σ. If x ≡ C_{i}(r_{1}, …, r_{n}), y ≡ C_{i}(r′_{1}, …, r′_{n}), x ∼ x, y ∼ y, then r_{i} ∼ r_{i}, r′_{i} ∼ r′_{i},

x ∼_{ρ} y ↔ ⋀_{i} r_{i} ∼ r′_{i} ↔ ⋀_{i} r_{i} ∼′ r′_{i} ↔ x ∼′ y

using Meta-IH and IH. If σ = ρ → τ the assertion is easy. (c): by (b).

Theorem 21. If FA_{1} − Eq ⊢ ϕ, FV(ϕ) ⊂ x⃗, then FA_{1} ⊢ ∀x⃗.x⃗ ∼ x⃗ → ϕ^{∼}.

Proof by Meta-induction on the derivation. The logical rules are easy (for the rules ∀-elimination and ∃^{∗}-introduction note that by lemma 18 for the term r used we have ∀x⃗.x⃗ ∼ x⃗ → r ∼ r). The extensionality axiom was just treated. For every induction axiom ψ of a formula ϕ(x) we have ψ^{∼}, since using Lemma 16 (b), from the premise of ψ^{∼} we can derive the step terms for the induction axiom for ϕ′(x) := x ∼ x → ϕ^{∼}(x).

Theorem 22. (a) FA_{1} −Eq is a conservative extension for FA_{1} for P-formulas:

If ϕ is a closed P-formula, FA_{1} − Eq ⊢ ϕ, then FA_{1} ⊢ ϕ.

(b) Adding to FA_{1} an extensional equality yields a conservative extension of FA_{1} for P-formulas

(c) Especially this holds for formulas containing only types of level ≤ 1.

Proof. From FA_{1} − Eq ⊢ ϕ follows FA_{1} ⊢ ϕ^{∼}. Now using Lemma 17 follows, if ψ is an N-formula, FV(ψ) ⊂ {x⃗}, FA_{1} ⊢ ∀x⃗.x⃗ ∼ x⃗ → ψ → ψ^{∼} and if ψ is a P-formula, then FA_{1} ⊢ ∀x⃗.x⃗ ∼ x⃗ → ψ^{∼} → ψ. Therefore we get FA_{1} ⊢ ϕ. (b): by (a), since we can interpret FA_{1} extended by axioms for an extensional equality in FA_{1} + Eq.

References

[Be93] Berger, U.: Program extraction from normalization proofs. In: M. Bezem, J.F. Groote (Eds.): Typed Lambda Calculi and Applications. Springer Lecture Notes in Computer Science 664, 1993, pp. 91 – 106.

[Be94] Berger, U.: A constructive interpretation of inductive definitions. Draft, Dept. of Mathematics, University of Munich, 1994.

[Be95] Berger, U.: Programs from classical proofs. In: Behara, M., Fritsch, R.,Lintz, R. G. (Eds.): Symposia Gaussiana. Proceedings of the 2nd Gauss Symposium. Conference A: Mathematics and Theoretical Physics, Walter de Gruyter, Berlin, 1995, pp. 187 – 200.

[BS95a] Berger, U., Schwichtenberg, H.: Program extraction from classical proofs. In: Leivant, D. (Ed.): Logic and Computational Complexity, Springer Lecture Notes in Computer Science 960, 1995, pp. 77 – 97.

[BS95b] Berger, U., Schwichtenberg, H.: Program development by proof transformation, In: Schwichtenberg, H. (Ed.): Proof and Computation. NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20 – August 1, 1993. Springer, Heidelberg, 1995, pp. 1 – 45.

[BS96] Berger, U., Schwichtenberg, H.: The greatest common divisor: a case study for program extraction from classical proofs. To appear in: Proceedings of Proofs and Types, Turin 1995, 1996.

[Ga56] Gandy, R.: On the axiom of extensionality – part I, Journal of Symbolic Logic, 21, 1956, pp. 36 – 48.

[Ga59] Gandy, R.: On the axiom of extensionality – part II, Journal of Symbolic Logic, 24, 1959, pp. 287 – 300.

[Lu73] Luckhardt, H.: Extensional Gödel Functional Interpretation. A Consistency Proof of Classical Analysis. Springer Lecture Notes in Mathematics 306, 1973.

[ML84] Martin-Löf, P.: Intuitionistic type theory, Bibliopolis, Naples, 1984.

[Mu90] Murthy, C.: Extracting constructive content from classical proofs. PhD thesis. Technical Report 90-1151, Dept. of Computer Science, Cornell University, Ithaca, New York, 1990.

[NPS90] Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s type theory. An Introduction, Oxford University Press, Oxford, 1990.

[PM93] Paulin-Mohring, C.: Inductive definitions in the system Coq. Rules and Properties. In: Bezem, M., Groote, J.F. (Eds.): Typed lambda calculi and applications, Springer Lecture Notes in Computer Science 664, 1993, pp. 328 – 345.

[Sch91] Schwichtenberg, H.: Normalization. In: Bauer, F. L. (Ed.): Logic, Algebra and Computation. Springer, Heidelberg, 1991, pp. 201 – 237.

[Sch92] Schwichtenberg, H.: Minimal from classical proofs. In: Börger, E. , Jäger, G., Kleine–Büning, H. , Richter, M. M.: Computer Science Logic, Springer Lecture Notes in Computer Science 626, 1992, pp. 326 – 328.

[Sch93a] Schwichtenberg, H.: Minimal Logic for computable functions. In: Bauer, F. L., Brauer, W., Schwichtenberg, H.: Logic and Algebra of Specification, NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 23–August 4, 1991, Springer, Heidelberg, 1993, pp. 289 – 320.

[Sch93b] Schwichtenberg, H.: Proofs as Programs. In: Aczel, P.,Simmons, H., Wainer, S. S.: Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990. Cambridge University Press, 1993, pp. 81 – 113.

[Sch94] Schwichtenberg, H.: Proof Theory. Manuskript, Dept. of Mathematics, University of Munich, 1994. Available via http://www.mathematik.uni-muenchen.de/∼schwicht/lectures/proofth/ss94/ pt.dvi.Z.

[Sch95] Schwichtenberg, H.: Computational Content of Proofs. To appear in Proceedings of the Summerschool in Marktoberdorf, 1995.

[Se93] Setzer, A.: Proof Theoretical Strength of Martin–Löf Type Theory with W – Type and One Universe, PhD thesis, University of Munich, Dep. of Mathematics, 1993.

[Se94] Setzer, A.: A type theory for iterated inductive definitions, Draft, Munich, 1994. Available via http://www.mathematik.uni-muenchen.de/∼setzer/articles.

[Se95] Setzer, A.: Well-ordering proofs for Martin-Löf Type Theory with W-type and one universe. Submitted. A preliminary version is available via http://www.mathematik.uni-muenchen.de/∼setzer/articles.

[TD88] Troelstra, A. S., Dalen, D. v.: Constructivism in Mathematics. An introduction, volume 121, 123 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1988

[Tr73] Troelstra, A. S. (Ed.): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer Lecture Notes in Mathematics 344, 1973.

This article was processed using the L^{A}TEX macro package with LLNCS style