Cut-Elimination for a Logic with Definitions and Induction

Raymond McDowell Department of Computer Science Widener University Chester, PA 19013 USA

Dale Miller Department of Computer Science and Engineering 200 Pond Laboratory The Pennsylvania State University University Park, PA 16802 USA

May 15, 1998

Abstract

In order to reason about specifications of computations that are given via the proof search or logic programming paradigm one needs to have at least some forms of induction and some principle for reasoning about the ways in which terms are built and the ways in which computations can progress. The literature contains many approaches to formally adding these reasoning principles with logic specifications. We choose an approach based on the sequent calculus and design an intuitionistic logic F Oλ^{ΔIN} that includes natural number induction and a notion of definition. We have detailed elsewhere that this logic has a number of applications. In this paper we prove the cut-elimination theorem for F Oλ^{ΔIN}, adapting a technique due to Tait and Martin-Löf. This cut-elimination proof is technically interesting and significantly extends previous results of this kind.

1 Introduction

As one attempts to prove a given sequent by placing above it an inference rule, zero or more unproven sequents will arise for the premise of the inference rule and these sequents will, in general, involve some different formulas than the conclusion sequent. Such changes in sequents during the search for a proof have been used to provide a rich and flexible framework for the specification of a wide range of computations. Of course, to make proof search resemble a computational process, the cut rule needs to be avoided; that is, when attempting to model a computation by constructing a proof, it seems sensible not to oblige the search to also search for lemmas to establish. The search for lemmas is part of the creative activity of mathematicians when they look for proofs and does not seem part of the notion of mechanical computation. The cut-elimination theorem, when available, could be used to argue that the search for cut-free proofs is a complete proof procedure. The logic programming paradigm can be defined, at least abstractly, using this notion of proof search, although a further restriction on the search of proofs is often made. In particular, the notion of “goal-directed search” that seems to be a natural aspect of the logic programming paradigm has been formulated using the technical notion of uniform proof [18, 17]. To retain completeness of uniform proofs, restrictions on logical formulas need to maintained. For example, completeness of uniform proofs can be achieved in classical logic by restricting to Horn clauses [19]; in intuitionistic logic by restricting to hereditary Harrop formulas [18]; and in linear logic by choosing the proper logical connectives [1, 17].

There are numerous examples of specifying computations within these logics and with using meta-theoretic properties of those logics to infer properties of computations. We only mention a few of these examples here. Intuitionistic logic has been used to specify both the dynamic and static semantics of functional programming languages [10], and theorems that relate these two semantics (such as subject reduction or type preservation) are rendered as simple consequences of the proof theory of intuitionistic logic [14]. In [17], various linear logic encodings of simple objects with state are given and proved equivalent within linear logic. Also in that paper, a small programming language with references is specified, and techniques for proving the equivalence of two programs are given based on resolution within linear logic. In [2], Chirimar provides two specifications of the operational semantics of the DLX RISC processor [20], one capturing its sequential, machine code semantics and the other capturing its concurrent, pipe-lined semantics. Using simple properties of proofs in linear logic, he is able to formally show the equivalence of those two specifications.

Moving from the classical theory of Horn clauses (the logical foundations of Prolog) to all of linear logic (as in the Forum specification language [17]) greatly increases the expressive power of the logic programming paradigm. While Horn clauses are, of course, powerful enough to specify all computations, such specifications need to represent most of the dynamics of a computation within atomic formulas, that is, within the non-logical layer of the language. As a result, deep properties of the ambient logic, such as cut-elimination, are of only limited use when reasoning about Horn clause specifications since such properties only supply meaning for the logical constants. As more expressive logics are used, more dynamics of a computation can be captured by various aspects of the logic, and this increases the likelihood that properties of the logic can be used to derive properties of the specified computations.

There is a difference, however, between specifying a computation and reasoning about a computation, and, in particular, reasoning about computation often requires induction and some way to considering all possible paths that a given computation could proceed or a given object could have been constructed. In the literature, there have been various approaches to providing for these missing features. Within type theory, for example, induction over data structures and over proofs can be used for reasoning about computations [21]. Within logic programming, there are various ways to turn the closed world assumption into a proof principle, such as SLDNF [4]. In this paper, we consider another approach that introduces new inference rules into the sequent calculus of intuitionistic logic. In particular, we add to the sequent calculus a rule for induction on natural numbers and inference rules for treating logic specifications as definitions instead of as theories. Our approach to definitions follows lines developed by Schroeder-Heister [25], Eriksson [5], Girard [9], and Stärk [28].

Our needs for reasoning about specifications, however, forced us to develop a single extension to intuitionistic logic, called F Oλ^{ΔIN} (pronounced “fold-n”), that goes beyond the logics studied in previous works. In particular, we needed one logic that allowed for not only induction and definitions but also for higher-order quantification (but not predicate quantification) since we wished to treat higher-order abstract syntax [23]. When designing a new sequent calculus to be used for reasoning, it is important to establish a cut-elimination theorem since this one result can be used to show the consistency of the logic as well as that the consequence relation is closed under modus ponens. The key features of F Oλ^{ΔIN} (induction, definitions, and higher-order quantification) interact in complicated ways, so previous cut-elimination proofs for logics with these features in isolation do not carry over to this new system. The bulk of this paper is a presentation of a proof of cutelimination for F Oλ^{ΔIN}.

The paper is organized as follows. In the next section, we briefly describe some uses that have been made of F Oλ^{ΔIN}. In section 3 we introduce the logic and some of its basic properties. We proceed in Section 4 to give an overview of the cut-elimination proof. Section 5 specifies the reduction rules that will be used to eliminate applications of the cut rule. This is followed by a section which provides some auxiliary definitions and their properties. Section 7 contains the proof of cut-elimination. We conclude with a brief comparison of our work with related work of Martin-Löf and Schroeder-Heister.

2 Applications of F Oλ^{ΔIN}

One use of F Oλ^{ΔIN} has been to reason about Horn clause programs. For example, Horn clauses can be used to specify a predicate that relates a list to its length and another predicate that relates two lists if they are permutations of each other. It is an easy matter to give a proof in F Oλ^{ΔIN} that if two lists are permutations of each other, then those two lists have the same length [13, Chapter 2]. Many similar theorems can be found throughout McDowell’s dissertation [13].

As we shall see, the integration of definitions into sequent calculus makes it possible to perform a case analysis on possible ways that a specified computation can progress. If exploited properly, it is possible to capture notions such as simulation and bisimulation between two processes. The paper [16] shows how this can be accomplished in abstract transition systems and CCS.

A final area where F Oλ^{ΔIN} has been used to reason about specifications is in the area of logical frameworks and higher-order abstract syntax. Logical frameworks have been successfully used to give high-level, modular, and formal specifications of many important judgments in the area of programming languages and inference systems. These judgments, such as “the term M denotes a program”, “the program M evaluates to the value V ”, and “the program M has type T ”, are represented by predicates in the specification logic or by types in a dependent type calculus. One of the advantages of such formal specifications is that they allow logical and mathematical analyses to be used to prove properties about the specified systems. Given the specification of evaluation for a functional programming language, for example, we may wish to prove that the language is deterministic or that evaluation preserves types.

One challenge in reasoning about such specifications centers on the use of higher-order abstract syntax, an elegant and declarative encoding of abstraction and substitution [23]. With most approaches to syntactic representation, the details of variable binding and substitution must be carefully addressed throughout a specification, and theorems about substitution and bound variables can dominate the system analyses. With higher-order abstract syntax, on the other hand, these features are specified concisely and their basic properties follow immediately from the specification logic. However, reasoning within a logical framework about systems represented in higher-order abstract syntax has been difficult since the logics that support this notion of syntax do not provide facilities for the fundamental operations of case analysis and induction. Moreover, higher-order abstract syntax leads to types and recursive definitions that do not give rise to monotone inductive operators, making inductive principles difficult to find. In [14] the authors have shown that these difficulties can be overcome within F Oλ^{ΔIN}. See [13, 14] for more on how F Oλ^{ΔIN} can be used as a meta-logic for an intuitionistic and linear logical framework.

The Pi derivation editor of Eriksson [6] was designed for the finitary calculus of partial inductive definitions [5]. Because of F Oλ^{ΔIN}’s close relationship with the finitary calculus of partial inductive definitions, the Pi editor can be used to construct F Oλ^{ΔIN} derivations. The many examples of specifications and proofs in F Oλ^{ΔIN} reported in [13, 14] were constructed using this editor.

Dependent typed λ-calculi have been used to specify computations in ways analogous to the logic programming setting presented here [22]. Schürmann and Pfenning [26] presented a meta-logic for such a dependent typed λ-terms that can be used to reason about higher-order deductions in ways similar to uses of F Oλ^{ΔIN} [14].

3 The Logic F Oλ^{ΔIN}

The basic logic is an intuitionistic version of a subset of Church’s Simple Theory of Types [3] in which meta-level formulas will be given the type o. The logical connectives are ⊥, ⊤, ∧, ∨, ⊃, ∀_{τ}, and ∃_{τ}. The quantification types τ (and thus the types of variables) are restricted to not contain o. Thus F Oλ^{ΔIN} supports quantification over higher-order (non-predicate) types, a crucial feature for higher-order abstract syntax, but has a first-order proof theory since there is no quantification over predicate types. We will use sequents of the form Γ ⟶ B, where Γ is a finite multiset of formulas and B is a single formula. The basic inference rules for the logic are shown in Table 1. In the ∀R and ∃L rules, y is an eigenvariable that is not free in the lower sequent of the rule. The multicut (mc) rule is a generalization of cut due to Slaney [27], and is used to simplify the presentation of the cut-elimination proof.

We introduce the natural numbers via the constants z : nt for zero and s : nt → nt for successor and the predicate nat : nt → o. The right and left rules for this new predicate are

Γ ⟶ nat z natR  Γ ⟶ nat I Γ ⟶ nat (s I) natR

\begin{aligned}⟶ B z & B j ⟶ B (s j) & B I, Γ ⟶ C \\ & nat I, Γ ⟶ C \end{aligned} natL .

In the left rule, the predicate B : nt → o represents the property that is proved by induction, and j is an eigenvariable that is not free in B. The third premise of that inference rule witnesses the fact that, in general, B will express a property stronger than (⋀ Γ) ⊃ C.

Because the induction predicate B in the natL rule is not necessarily a subformula of the formula C or any formula in Γ, the subformula property does not hold for F Oλ^{ΔIN}. In fact, we can derive the following inference rule from the induction rule:

\begin{matrix}⟶ B & B, Γ ⟶ C \\ nat I, Γ ⟶ C \end{matrix} .

This derived rule resembles the cut rule but requires a nat assumption. Although F Oλ^{ΔIN} does not have the subformula property, the cut-elimination theorem still provides a strong basis for reasoning about proofs in F Oλ^{ΔIN} [13, 14, 16]. In fact, the formulation of the natL rule and the failure of the subformula property reflect the fact that in actual mathematical practice, finding the Table 1: Inference rules for the core of F Oλ^{ΔIN}

⊥, Γ ⟶ B ⊥L  Γ ⟶ ⊤ ⊤R

{B, Γ ⟶ D \atop B ∧ C, Γ ⟶ D} ∧L  {C, Γ ⟶ D \atop B ∧ C, Γ ⟶ D} ∧L  {B[t/x], Γ ⟶ C \atop ∀x.B, Γ ⟶ C} ∀L

\begin{matrix}Γ ⟶ B & Γ ⟶ C \\ Γ ⟶ B ∧ C \end{matrix} ∧R  {Γ ⟶ B[y/x] \atop Γ ⟶ ∀x.B} ∀R

\begin{matrix}B, Γ ⟶ D & C, Γ ⟶ D \\ B ∨ C, Γ ⟶ D \end{matrix} ∨L  {B[y/x], Γ ⟶ C \atop ∃x.B, Γ ⟶ C} ∃L

{Γ ⟶ B \atop Γ ⟶ B ∨ C} ∨R  {Γ ⟶ C \atop Γ ⟶ B ∨ C} ∨R  {Γ ⟶ B[t/x] \atop Γ ⟶ ∃x.B} ∃R

\begin{matrix}Γ ⟶ B & C, Γ ⟶ D \\ B ⊃ C, Γ ⟶ D \end{matrix} ⊃ L  {B, Γ ⟶ C \atop Γ ⟶ B ⊃ C} ⊃ R

A, Γ ⟶ A init, where A is atomic  {B, B, Γ ⟶ C \atop B, Γ ⟶ C} cL

\begin{aligned}Δ_{1} ⟶ B_{1} & ⋯ & Δ_{n} ⟶ B_{n} & B_{1}, …, B_{n}, Γ ⟶ C \\ & Δ_{1}, …, Δ_{n}, Γ ⟶ C \end{aligned} mc, where n ≥ 0

proper induction hypothesis requires insight and creativity; they are not simply rearrangements of the subformulas of the conclusion. As a result, any implementation of F Oλ^{ΔIN} will necessarily be interactive, at least for the invention of many induction hypotheses.

A definitional clause is written ∀x̄[p t̄=^{△} B], where p is a predicate constant, every free variable of the formula B is also free in at least one term in the list t̄ of terms, and all variables free in t̄ are contained in the list x̄ of variables. Since all free variables in p t̄ and B are universally quantified, we often leave these quantifiers implicit when displaying definitional clauses. The atomic formula p t̄ is called the head of the clause, and the formula B is called the body. The symbol =^{△} is used simply to indicate a definitional clause: it is not a logical connective. A definition is a (perhaps infinite) set of definitional clauses. The same predicate may occur in the head of multiple clauses of a definition: it is best to think of a definition as a mutually recursive definition of the predicates in the heads of the clauses.

Definitions are employed in F Oλ^{ΔIN} via left and right introduction rules for atomic formulas. If we impose no restrictions on definitions, the cut-elimination theorem does not hold [24]. Two different approaches have been taken to retain the admissibility of cut. First, if the structural rule of contraction is removed or restricted (as it is in linear logic, for example), cut-elimination can be established [9, 25]. Another approach, more appropriate for use here since we wish to work within an intuitionistic setting, is to restrict the occurrences of implications within the body of definitions. In [25], Schroeder-Heister proved the cut-elimination theorem for an intuitionistic logic in which no implications are allowed within definitions. Here we shall allow implications in the body of definitions if they are suitably stratified. Toward that end we assume that each predicate symbol p in the language has associated with it a natural number lvl(p), the level of the predicate. The following definition extends the notion of level to formulas and derivations.

Definition 1 Given a formula B, its level lvl(B) is defined as follows:

1. lvl(p t̄) = lvl(p)

2. lvl(⊥) = lvl(⊤) = 0

3. lvl(B ∧ C) = lvl(B ∨ C) = max(lvl(B), lvl(C))

4. lvl(B ⊃ C) = max(lvl(B) + 1, lvl(C))

5. lvl(∀x.B) = lvl(∃x.B) = lvl(B).

Given a derivation Π of Γ ⟶ B, lvl(Π) = lvl(B).

We shall now require that for every definitional clause ∀x̄[p t̄=^{△} B], lvl(B) ≤ lvl(p).

The logic F Oλ^{ΔIN} has uses definitions in left and right-introduction rules for atoms; the following relation will be useful for describing those inference rules.

Definition 2 Let the four-place relation dfn(ρ, A, σ, B) be defined to hold for the formulas A and B and the substitutions ρ and σ if there is a clause ∀x̄[A′ =^{△} B] in the given definition such that Aρ = A′σ.

The right and left rules for atoms are

{Γ ⟶ Bθ \atop Γ ⟶ A} def R, where dfn(ϵ, A, θ, B)

{\{Bσ, Γρ ⟶ Cρ | dfn(ρ, A, σ, B)\} \atop A, Γ ⟶ C} def L ,

where ϵ is the empty substitution and the bound variables x̄ in the definitional clauses are chosen to be distinct from the variables free in the lower sequent of the rule. Specifying a set of sequents as the premise should be understood to mean that each sequent in the set is a premise of the rule. The right rule corresponds to the logic programming notion of backchaining if we think of =^{△} in definitional clauses as reverse implication. The left rule is similar to definitional reflection [25] (not to be confused with another notion of reflection often considered between a meta-logic and object-logic) and to an inference rule used by Girard in his note on fixed points [9]. Notice that in the def L rule, the free variables of the conclusion can be instantiated in the premises.

The number of premises of the def L rule may be zero or may be infinite. If the formula A does not unify with the head of any definitional clause, then the number of premises will be zero. In this case, A is an unprovable formula logically equivalent to ⊥, and def L corresponds to the ⊥L rule. If the formula A does unify with the head of a definitional clause, the number of premises could be infinite, since the domains of the substitutions ρ and σ may include variables that are not free in A and B. In general we wish to work with inference rules with a finite number of premises. This can be achieved by restricting definitions to have only a finite number of clauses and to restrict the use of def L rule to those formulas A such that for every definitional clause there is a finite, complete set of unifiers (CSU) [11] of A and the head of the clause. Consider the following inference rule due to Eriksson [5]

{Bθ, Γθ ⟶ Cθ | θ ∈ CSU(A, A′) for some clause ∀x̄[A′ =^{△} B]} A, Γ ⟶ C def L_{CSU} ,

where the variables x̄ are chosen to be distinct from the variables free in the lower sequent of the rule. When the CSUs and definition are finite, this rule will have a finite number of premises. Notice that in first-order logics, a CSU will have at most one member, namely the most general unifier (MGU).

Proposition 3 The rules def L and def L_{CSU} are interadmissible, that is, if F Oλ^{ΔIN} is formulated with either def L or def L_{CSU}, the other rule is admissible in that formulation.

Proof Given the set of derivations

\left\{{Π^{θ,B} \atop Bθ, Γθ ⟶ Cθ}\right\}_{θ∈CSU(A,A′) for some clause ∀x̄[A′=^{△}B]} ,

we can construct a derivation of A, Γ ⟶ C using def L as follows. For any definitional clause ∀x̄[A′ =^{△} B] and substitutions ρ and σ such that Aρ = A′σ, the substitution

ρ_{σ}(y) = \begin{cases}σ(y) & if y ∈ F V (A′) \\ ρ(y) & otherwise \end{cases}

will be a unifier of A and A′. Thus for some θ ∈ CSU(A, A′) there is a substitution θ′ such that ρ_{σ} is θ ∘ θ′. (Notice that composition of substitution is defined so that A(θ ∘ θ′) = (Aθ)θ′.) We can thus use Π^{θ,B}θ′ as the premise derivation of Bσ, Γρ ⟶ Cρ for def L. (We will formally define what it means to apply a substitution to a derivation in Definition 5. For now it is enough to know that it yields a derivation whose endsequent is obtained by applying the substitution to the endsequent of the original derivation.)

Given the set of derivations

\left\{{Π^{ρ,σ,B} \atop Bσ, Γρ ⟶ Cρ}\right\}_{dfn(ρ,A,σ,B)} ,

we can construct a derivation of A, Γ ⟶ C using def L_{CSU} as follows. For any definitional clause ∀x̄[A′ =^{△} B] and substitution θ ∈ CSU(A, A′), dfn(θ, A, θ, B) holds. We can thus use Π^{θ,θ,B} as the premise derivation of Bθ, Γθ ⟶ Cθ for def L.

Observe that several of the rules of F Oλ^{ΔIN} may have variables that are free in the premise but not in the conclusion: this results from the eigenvariable y of ∀R and ∃L, the term t of ∀L and ∃R, the cut formulas B_{1}, …, B_{n} of mc, the induction predicate B of natL, and the substitutions ρ and σ of def L. We view the choice of such variables as arbitrary and identify all derivations that differ only in the choice of variables that are not free in end-sequent.

We define an ordinal measure which corresponds to the height of a derivation:

Definition 4 Given a derivation Π with premise derivations {Π_{i}}_{i}, the measure ht(Π) is the least upper bound of {ht(Π_{i}) + 1}_{i}.

Substitutions are finite maps from variables to terms. It is common to view substitutions as maps from terms to terms by applying the substitution to all free variables of a term. We can then extend the mapping in turn to formulas and multisets by applying it to every term in a formula and every formula in a multiset. The following definition extends substitutions yet again to apply to derivations. Since we identify derivations that differ only in the choice of variables that are not free in the end-sequent, we will assume that such variables are chosen to be distinct from the variables in the domain of the substitution and from the free variables of the range of the substitution. Thus applying a substitution to a derivation will only affect the variables free in the end-sequent.

Definition 5 If Π is a derivation of Γ ⟶ C and θ is a substitution, then we define the derivation Πθ of Γθ ⟶ Cθ as follows:

1. Suppose Π ends with the def L rule

\begin{matrix}\left\{{Π^{ρ,σ,B} \atop Bσ, Γ′ρ ⟶ Cρ}\right\} & dfn(ρ,A,σ,B) \\ A, Γ′ ⟶ C \end{matrix} def L .

Observe that if dfn(ρ′, Aθ, σ′, B) then dfn(θ ∘ ρ′, A, σ′, B). Thus Πθ is

\begin{matrix}\left\{{Π^{θ∘ρ′,σ′,B} \atop Bσ′, Γ′θρ′ ⟶ Cθρ′}\right\} & dfn(ρ′,Aθ,σ′,B) \\ Aθ, Γ′θ ⟶ Cθ \end{matrix} def L .

2. If Π ends with any other rule and has premise derivations Π_{1}, …, Π_{n}, then Πθ also ends with the same rule and has premise derivations Π_{1}θ, …, Π_{n}θ.

Lemma 6 For any substitution θ and derivation Π of Γ ⟶ C, Πθ is a derivation of Γθ ⟶ Cθ.

Proof This lemma states that Definition 5 is well-constructed, and follows by induction on μ(Π). Observe that if Π ends with the def R rule

{Π′ \atop Γ ⟶ Bσ} ; Γ ⟶ A def R ,

then dfn(ϵ, A, σ, B), and so it is also true that dfn(ϵ, Aθ, σ ∘ θ, B). Therefore

{Π′θ \atop Γθ ⟶ Bσθ} ; Γθ ⟶ Aθ def R

is a valid derivation.

Lemma 7 For any derivation Π and substitution θ, ht(Π) ≥ ht(Πθ).

Proof The proof of this lemma is a simple induction on ht(Π). The measures may not be equal because when the derivations end with the def L rule, some of the premise derivations of Π may not be needed to construct the premise derivations of Πθ.

Our logic does not contain a weakening rule; instead we allow extra assumptions in the axioms. The following definition provides meta-level weakening on derivations. Since we identify derivations that differ only in the choice of variables that are not free in the end-sequent, we will assume that such variables are chosen to be distinct from the free variables of the weakening formulas.

Definition 8 If Π is a derivation of Γ ⟶ C and Δ is a multiset of formulas, then we define the derivation w(Δ, Π) of Γ, Δ ⟶ C as follows:

1. If Π ends with the def L rule

\begin{matrix}\{ & {Π^{ρ,σ,B} \atop Bσ, Γ′ρ ⟶ Cρ} & \} \\ A, Γ′ ⟶ C \end{matrix} def L ,

then w(Δ, Π) is

\begin{matrix}\{ & {w(Δρ, Π^{ρ,σ,B}) \atop Bσ, Γ′ρ, Δρ ⟶ Cρ} & \} \\ A, Γ′, Δ ⟶ C \end{matrix} def L .

2. If Π ends with the natL rule

{Π_{1} \atop ⟶ B z} {Π_{2} \atop B j ⟶ B (s j)} {Π_{3} \atop B I, Γ ⟶ C} nat I, Γ ⟶ C natL ,

then w(Δ, Π) is

{Π_{1} \atop ⟶ B z} {Π_{2} \atop B j ⟶ B (s j)} {w(Δ, Π_{3}) \atop B I, Γ, Δ ⟶ C} nat I, Γ, Δ ⟶ C natL .

3. If Π ends with the mc rule

{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π′ \atop B_{1}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc ,

then w(Δ, Π) is

{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {w(Δ, Π′) \atop B_{1}, …, B_{n}, Γ, Δ ⟶ C} Δ_{1}, …, Δ_{n}, Γ, Δ ⟶ C mc .

4. If Π ends with any other rule and has premise derivations Π_{1}, …, Π_{n}, then w(Δ, Π) also ends with the same rule and has premise derivations w(Δ, Π_{1}), …, w(Δ, Π_{n}).

The following lemmas can be proved by induction on the measure of the given derivation.

Lemma 9 For any multiset Δ of formulas and derivation Π of Γ ⟶ C, w(Δ, Π) is a derivation of Γ, Δ ⟶ C.

Lemma 10 For any derivation Π and multiset Δ of formulas, ht(Π) = ht(w(Δ, Π)).

Lemma 11 For any derivation Π, multiset Δ of formulas, and substitution θ,

w(Δ, Π)θ and w(Δθ, Πθ)

are the same derivation.

Lemma 12 For any derivation Π and multisets Δ and Δ′ of formulas,

w(Δ, w(Δ′, Π)) and w(Δ ∪ Δ′, Π)

are the same derivation.

4 Overview of the Cut-Elimination Proof

Gentzen’s classic proof of cut-elimination for first-order logic [7] uses an induction involving the number of logical connectives in the cut formula. A cut on a compound formula is replaced by cuts on its subformulas, which necessarily contain a lower number of connectives. For example, the derivation

\begin{matrix}{Π_{1} \atop Δ ⟶ B_{1}} & {Π_{2} \atop Δ ⟶ B_{2}} \\ Δ ⟶ B_{1} ∧ B_{2} \end{matrix} ∧R {Π_{3} \atop B_{1}, Γ ⟶ C} ; B_{1} ∧ B_{2}, Γ ⟶ C ∧L

Δ, Γ ⟶ C mc

is reduced to

\begin{matrix}{Π_{1} \atop Δ ⟶ B_{1}} & {Π_{3} \atop B_{1}, Γ ⟶ C} \\ Δ, Γ ⟶ C \end{matrix} mc .

By the induction hypothesis, this cut on B_{1} is eliminable, hence the original cut on B_{1} ∧ B_{2} is also eliminable. In first-order logic, when the cut formula is atomic, the cut can easily be removed by permuting the cut up toward the leaves of the proof; eventually an initial rule is reached, at which point the removal of the cut is trivial.

In F Oλ^{ΔIN}, however, the rules for natural numbers and definitions act on atoms, so the atomic case is not simple. Consider, for example, the derivation

{Π_{1} \atop Δ ⟶ Bθ} ; Δ ⟶ A def R \begin{matrix}\{ & {Π^{ρ,σ,D} \atop Dσ, Γρ ⟶ Cρ} & \} \\ A, Γ ⟶ C \end{matrix} def L Δ, Γ ⟶ C mc .

The obvious reduction for this is a cut between Π_{1} and the appropriate premise of the def L rule; however, Bθ is a formula of arbitrary complexity, and so will in general have a greater number of connectives than the atom A, which has zero. Thus a different induction measure is needed.

Schroeder-Heister proves cut-elimination for several logics with definitions [24, 25] by including the number of uses of the def L rule in the derivation as part of the induction measure. However, the logics he considers do not contain induction; the inclusion of the natR and natL rules in F Oλ^{ΔIN} complicates things further. The derivation

{Π_{1} \atop Δ ⟶ nat I} Δ ⟶ nat (s I) natR {Π_{2} \atop ⟶ B z} {Π_{3} \atop B j ⟶ B (s j)} {Π_{4} \atop B (s I), Γ ⟶ C} nat (s I), Γ ⟶ C natL

Δ, Γ ⟶ C mc

can be reduced in a number of ways, but the reductions are all variations of the derivation

{Π_{1} \atop Δ ⟶ nat I} {Π_{2} \atop ⟶ B z} {Π_{3} \atop B j ⟶ B (s j)} {Π_{3}[I/j] \atop B I ⟶ B (s I)} nat I ⟶ B (s I) natL Δ ⟶ B (s I) mc {Π_{4} \atop B (s I), Γ ⟶ C} Δ, Γ ⟶ C mc .

Here, the cut on the atomic formula nat (s I) is replaced by two cuts, one on the atom nat I and the other on the formula B (s I). It is not clear what induction measure can be used here. For the first cut, the atom nat I contains no logical connectives, but this is true of the original cut formula nat (s I) as well. The number of natR rules in the right subderivation of the cut has gone down by one, but the duplication of Π_{3} might offset this. For the second cut, the cut formula B (s I) is not related at all to the original cut formula; it certainly can have no fewer connectives than the atom nat (s I). And though its left premise is shorter than the left premise of the original cut, it is unclear how the heights of the right premises compare.

It should be noted, however, that the complicating factor here is not the presence of an induction rule, but our use of the nat predicate in the induction rule. If we remove the natR rules from the logic and reformulate the induction rule to be

\begin{aligned}⟶ B z & B j ⟶ B (s j) & B I, Γ ⟶ C \\ & Γ ⟶ C \end{aligned} ind ,

then Schroeder-Heister’s proofs can be extended to that logic. Despite this, we prefer to include the nat predicate in our formulation of the logic. At an aesthetic level, our formulation maintains the symmetry between right and left rules of the logic. Including the nat predicate also keeps the form of the induction rule for natural numbers consistent with the form of the induction rules we can derive from it for defined predicates [13]. Finally, the nat predicate plays a key role in the adequacy proofs for encodings of intuitionistic and linear logic frameworks in F Oλ^{ΔIN} [14].

Our proof of the cut-elimination theorem for F Oλ^{ΔIN} uses a technique introduced by Tait [29] to prove normal form theorems. Martin-Löf extended the method to apply beyond terms to natural deduction proofs [12], and we use it here in a sequent calculus setting. Rather than associate an induction measure with derivations, we use the derivations themselves as a measure by defining well-founded orderings on derivations, and performing the induction relative to those orderings. The basis for the orderings is a set of reduction rules, such as those suggested above, that will be used to eliminate applications of the cut rule. We give these reduction rules in Section 5. This is followed by a section which discusses two orderings on derivations, a normalizability ordering and a reducibility ordering. The well-foundedness of the normalizability ordering for a derivation implies that the reduction rules can be used to reduce the derivation to a cut-free derivation of the same end-sequent. The reducibility ordering is a superset of the normalizability ordering; thus its well-foundedness implies the well-foundedness of the normalizability ordering. (This notion of reducibility was called convertibility by Tait and computability by Martin-Löf. We prefer to avoid these terms since they carry other meanings in theoretical computer science and, instead, use reducibility after Girard [8].) In Section 7 we prove the key lemma: for every derivation, the tree of its successive predecessors in the reducibility relation is well-founded. From this we conclude that the corresponding tree in the normalizability relation is also well-founded, and hence the cut rule can be eliminated from that derivation. Since this holds for every derivation, the consistency of F Oλ^{ΔIN} follows.

5 Reduction Rules for Derivations

Here we define a reduction relation between derivations, which is an adaptation of the reduction rules used in Gentzen’s original Hauptsatz [7].

Definition 13 We define a reduction relation between derivations. The redex is always a derivation Ξ ending with the multicut rule

{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π \atop B_{1}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

If n = 0, Ξ reduces to the premise derivation Π.

For n > 0 we specify the reduction relation based on the last rule of the premise derivations. If the rightmost premise derivation Π ends with a left rule acting on a cut formula B_{i}, then the last rule of Π_{i} and the last rule of Π together determine the reduction rules that apply. We classify these rules according to the following criteria: we call the rule an essential case when Π_{i} ends with a right rule; if it ends with a left rule, it is a right-commutative case; if Π_{i} ends with the init rule, then we have an axiom case; a multicut case arises when it ends with the mc rule. When Π does not end with a left rule acting on a cut formula, then its last rule is alone sufficient to determine the reduction rules that apply. If Π ends in a rule acting on a formula other than a cut formula, then we call this a left-commutative case. A structural case results when Π ends with a contraction on a cut formula. If Π ends with the init rule, this is also an axiom case; similarly a multicut case arises if Π ends in the mc rule. For simplicity of presentation, we always show i = 1.

Essential cases:

∧R/ ∧ L: If Π_{1} and Π are

\begin{matrix}{Π′_{1} \atop Δ_{1} ⟶ B′_{1}} & {Π′′_{1} \atop Δ_{1} ⟶ B′′_{1}} \\ Δ_{1} ⟶ B′_{1} ∧ B′′_{1} \end{matrix} ∧R  {Π′ \atop B′_{1}, B_{2}, …, B_{n}, Γ ⟶ C} ; B′_{1} ∧ B′′_{1}, B_{2}, …, B_{n}, Γ ⟶ C ∧L ,

then Ξ reduces to

{Π′_{1} \atop Δ_{1} ⟶ B′_{1}} {Π_{2} \atop Δ_{2} ⟶ B_{2}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π′ \atop B′_{1}, B_{2}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

The case for the other ∧L rule is symmetric.

∨R/ ∨ L: If Π_{1} and Π are

{Π′_{1} \atop Δ_{1} ⟶ B′_{1}} ; Δ_{1} ⟶ B′_{1} ∨ B′′_{1} ∨R \begin{matrix}{Π′ \atop B′_{1}, B_{2}, …, B_{n}, Γ ⟶ C} & {Π′′ \atop B′′_{1}, B_{2}, …, B_{n}, Γ ⟶ C} \\ B′_{1} ∨ B′′_{1}, B_{2}, …, B_{n}, Γ ⟶ C \end{matrix} ∨L ,

then Ξ reduces to

{Π′_{1} \atop Δ_{1} ⟶ B′_{1}} {Π_{2} \atop Δ_{2} ⟶ B_{2}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π′ \atop B′_{1}, B_{2}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

The case for the other ∨R rule is symmetric.

⊃ R/ ⊃ L: Suppose Π_{1} and Π are

{Π′_{1} \atop B′_{1}, Δ_{1} ⟶ B′′_{1}} ; Δ_{1} ⟶ B′_{1} ⊃ B′′_{1} ⊃ R \begin{matrix}{Π′ \atop B_{2}, …, B_{n}, Γ ⟶ B′_{1}} & {Π′′ \atop B′′_{1}, B_{2}, …, B_{n}, Γ ⟶ C} \\ B′_{1} ⊃ B′′_{1}, B_{2}, …, B_{n}, Γ ⟶ C \end{matrix} ⊃ L .

Let Ξ_{1} be

\begin{matrix}\left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{2..n\}} & {Π′ \atop B_{2}, …, B_{n}, Γ ⟶ B′_{1}} \\ Δ_{2}, …, Δ_{n}, Γ ⟶ B′_{1} \end{matrix} mc {Π′_{1} \atop B′_{1}, Δ_{1} ⟶ B′′_{1}} Δ_{1}, …, Δ_{n}, Γ ⟶ B′′_{1} mc .

Then Ξ reduces to

{Ξ_{1} \atop … ⟶ B′′_{1}} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{2..n\}} {Π′′ \atop B′′_{1}, \{B_{i}\}_{i∈\{2..n\}}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ, Δ_{2}, …, Δ_{n}, Γ ⟶ C mc cL Δ_{1}, …, Δ_{n}, Γ ⟶ C .

We use the double horizontal lines to indicate that the relevant inference rule (in this case, cL) may need to be applied zero or more times.

∀R/∀L: If Π_{1} and Π are

{Π′_{1} \atop Δ_{1} ⟶ B′_{1}[y/x]} ; Δ_{1} ⟶ ∀x.B′_{1} ∀R  {Π′ \atop B′_{1}[t/x], B_{2}, …, B_{n}, Γ ⟶ C} ; ∀x.B′_{1}, B_{2}, …, B_{n}, Γ ⟶ C ∀L ,

then Ξ reduces to

{Π′_{1}[t/y] \atop Δ_{1} ⟶ B′_{1}[t/x]} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{2..n\}} {Π′ \atop … ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

∃R/∃L: If Π_{1} and Π are

{Π′_{1} \atop Δ_{1} ⟶ B′_{1}[t/x]} ; Δ_{1} ⟶ ∃x.B′_{1} ∃R  {Π′ \atop B′_{1}[y/x], B_{2}, …, B_{n}, Γ ⟶ C} ; ∃x.B′_{1}, B_{2}, …, B_{n}, Γ ⟶ C ∃L ,

then Ξ reduces to

{Π′_{1} \atop Δ_{1} ⟶ B′_{1}[t/x]} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{2..n\}} {Π′[t/y] \atop … ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

natR/natL: Suppose Π_{1} is Δ_{1} ⟶ nat z natR and Π is

{Π′ \atop ⟶ D z} {Π′′ \atop D j ⟶ D (s j)} {Π′′′ \atop D z, B_{2}, …, B_{n}, Γ ⟶ C} nat z, B_{2}, …, B_{n}, Γ ⟶ C natL .

Then Ξ reduces to

{w(Δ_{1}, Π′) \atop Δ_{1} ⟶ D z} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{2..n\}} {Π′′′ \atop D z, B_{2}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

natR/natL: Suppose Π_{1} is

{Π′_{1} \atop Δ_{1} ⟶ nat I}

Δ_{1} ⟶ nat (s I)

natR

and Π is

{Π′ \atop ⟶ D z} {Π′′ \atop D j ⟶ D (s j)} {Π′′′ \atop D (s I), B_{2}, …, B_{n}, Γ ⟶ C} nat (s I), B_{2}, …, B_{n}, Γ ⟶ C natL .

Let Ξ_{1} be

{Π′_{1} \atop Δ_{1} ⟶ nat I} {Π′ \atop ⟶ D z} {Π′′ \atop D j ⟶ D (s j)} D I ⟶ D I init nat I ⟶ D I natL Δ_{1} ⟶ D I mc ,

and Ξ_{2} be

\begin{matrix}{Ξ_{1} \atop Δ_{1} ⟶ D I} & {Π′′[I/j] \atop D I ⟶ D (s I)} \\ Δ_{1} ⟶ D (s I) \end{matrix} mc .

Then Ξ reduces to

{Ξ_{2} \atop Δ_{1} ⟶ D (s I)} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{2..n\}} {Π′′′ \atop D (s I), B_{2}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

def R/def L: Suppose Π_{1} and Π are

{Π′_{1} \atop Δ_{1} ⟶ B′_{1}θ} ; Δ_{1} ⟶ B_{1} def R \begin{matrix}\{ & {Π^{ρ,σ,D} \atop Dσ, B_{2}ρ, …, B_{n}ρ, Γρ ⟶ Cρ} & \} \\ B_{1}, B_{2}, …, B_{n}, Γ ⟶ C \end{matrix} def L .

Then by the def R rule in Π_{1} dfn(ϵ, B_{1}, θ, B′_{1}) holds. Let θ′ be the restriction of θ to the variables x̄ of the relevant definitional clause. Since B′_{1} is the body of this clause, its free variables are included in x̄, and so B′_{1}θ′ = B′_{1}θ. Then Ξ reduces to

{Π′_{1} \atop Δ_{1} ⟶ B′_{1}θ} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{2..n\}} {Π^{ϵ,θ′,B′_{1}} \atop B′_{1}θ, B_{2}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

Left-commutative cases:

•L/ ∘ L: Suppose Π ends with a left rule other than cL acting on B_{1}, and Π_{1} is

\begin{matrix}\{ & {Π_{1}^{i} \atop Δ_{1}^{i} ⟶ B_{1}} & \} \\ Δ_{1} ⟶ B_{1} \end{matrix} •L ,

where •L is any left rule except ⊃ L, def L, or natL (but including cL). Then Ξ reduces to

\{{Π_{1}^{i} \atop Δ_{1}^{i} ⟶ B_{1}} \left\{{Π_{j} \atop Δ_{j} ⟶ B_{j}}\right\}_{j∈\{2..n\}} {Π \atop B_{1}, …, B_{n}, Γ ⟶ C} Δ_{1}^{i}, Δ_{2}, …, Δ_{n}, Γ ⟶ C mc\} Δ_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C •L .

⊃ L/ ∘ L: Suppose Π ends with a left rule other than cL acting on B_{1} and Π_{1} is

\begin{matrix}{Π′_{1} \atop Δ′_{1} ⟶ D′_{1}} & {Π′′_{1} \atop D′′_{1}, Δ′_{1} ⟶ B_{1}} \\ D′_{1} ⊃ D′′_{1}, Δ′_{1} ⟶ B_{1} \end{matrix} ⊃ L .

Let Ξ_{1} be

{Π′′_{1} \atop D′′_{1}, Δ′_{1} ⟶ B_{1}} {Π_{2} \atop Δ_{2} ⟶ B_{2}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π \atop B_{1}, …, B_{n}, Γ ⟶ C} D′′_{1}, Δ′_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C mc .

Then Ξ reduces to

w(Δ_{2} ∪ … ∪ Δ_{n} ∪ Γ, Π′_{1}) Δ′_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ D′_{1} {Ξ_{1} \atop D′′_{1}, Δ′_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C} D′_{1} ⊃ D′′_{1}, Δ′_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C ⊃ L .

natL/ ∘ L: Suppose Π ends with a left rule other than cL acting on B_{1}, and Π_{1} is

{Π_{1}^{1} \atop ⟶ D_{1} z} {Π_{1}^{2} \atop D_{1} j ⟶ D_{1} (s j)} {Π_{1}^{3} \atop D_{1} I, Δ′_{1} ⟶ B_{1}} nat I, Δ′_{1} ⟶ B_{1} natL .

Let Ξ_{1} be

{Π_{1}^{3} \atop D_{1} I, Δ′_{1} ⟶ B_{1}} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{2..n\}} {Π \atop B_{1}, …, B_{n}, Γ ⟶ C} D_{1} I, Δ′_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C mc .

Then Ξ reduces to

{Π_{1}^{1} \atop ⟶ D_{1} z} {Π_{1}^{2} \atop D_{1} j ⟶ D_{1} (s j)} {Ξ_{1} \atop D_{1} I, Δ′_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C} nat I, Δ′_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C natL .

def L/ ∘ L: If Π ends with a left rule other than cL acting on B_{1} and Π_{1} is

\begin{matrix}\{ & {Π_{1}^{ρ,σ,D} \atop Dσ, Δ′_{1}ρ ⟶ B_{1}ρ} & \} \\ A, Δ′_{1} ⟶ B_{1} \end{matrix} def L ,

\{{Π_{1}^{ρ,σ,D} \atop Dσ, Δ′_{1}ρ ⟶ B_{1}ρ} \left\{{Π_{i}ρ \atop Δ_{i}ρ ⟶ B_{i}ρ}\right\}_{i∈\{2..n\}} {Πρ \atop … ⟶ Cρ} Dσ, Δ′_{1}ρ, Δ_{2}ρ, …, Δ_{n}ρ, Γρ ⟶ Cρ mc\} A, Δ′_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C def L .

Right-commutative cases: −/ ∘ L: Suppose Π is

\begin{matrix}\{ & {Π^{i} \atop B_{1}, …, B_{n}, Γ^{i} ⟶ C} & \} \\ B_{1}, …, B_{n}, Γ ⟶ C \end{matrix} ∘L ,

where ∘L is any left rule other than ⊃ L, def L, or natL (but including cL) acting on a formula other than B_{1}, …, B_{n}. Then Ξ reduces to

\{{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π^{i} \atop B_{1}, …, B_{n}, Γ^{i} ⟶ C} Δ_{1}, …, Δ_{n}, Γ^{i} ⟶ C mc\} Δ_{1}, …, Δ_{n}, Γ ⟶ C ∘L .

−/ ⊃ L: Suppose Π is

\begin{matrix}{Π′ \atop B_{1}, …, B_{n}, Γ′ ⟶ D′} & {Π′′ \atop B_{1}, …, B_{n}, D′′, Γ′ ⟶ C} \\ B_{1}, …, B_{n}, D′ ⊃ D′′, Γ′ ⟶ C \end{matrix} ⊃ L .

Let Ξ_{1} be

{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π′ \atop B_{1}, …, B_{n}, Γ′ ⟶ D′}

Δ_{1}, …, Δ_{n}, Γ′ ⟶ D′ mc

and Ξ_{2} be

{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π′′ \atop B_{1}, …, B_{n}, D′′, Γ′ ⟶ C} Δ_{1}, …, Δ_{n}, D′′, Γ′ ⟶ C mc .

Then Ξ reduces to

{Ξ_{1} \atop Δ_{1}, …, Δ_{n}, Γ′ ⟶ D′} {Ξ_{2} \atop Δ_{1}, …, Δ_{n}, D′′, Γ′ ⟶ C} Δ_{1}, …, Δ_{n}, D′ ⊃ D′′, Γ′ ⟶ C ⊃ L .

−/natL: Suppose Π is

{Π′ \atop ⟶ D z} {Π′′ \atop D j ⟶ D (s j)} {Π′′′ \atop B_{1}, …, B_{n}, D I, Γ′ ⟶ C} B_{1}, …, B_{n}, nat I, Γ′ ⟶ C natL .

Let Ξ_{1} be

{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π′′′ \atop B_{1}, …, B_{n}, D I, Γ′ ⟶ C} Δ_{1}, …, Δ_{n}, D I, Γ′ ⟶ C mc .

then Ξ reduces to

{Π′ \atop ⟶ D z} {Π′′ \atop D j ⟶ D (s j)} {Ξ_{1} \atop Δ_{1}, …, Δ_{n}, D I, Γ′ ⟶ C} Δ_{1}, …, Δ_{n}, nat I, Γ′ ⟶ C natL .

−/def L: If Π is

\begin{matrix}\{ & {Π^{ρ,σ,D} \atop B_{1}ρ, …, B_{n}ρ, Dσ, Γ′ρ ⟶ Cρ} & \} \\ B_{1}, …, B_{n}, A, Γ′ ⟶ C \end{matrix} def L ,

then Ξ reduces to

\{\begin{matrix}\left\{{Π_{i}ρ \atop Δ_{i}ρ ⟶ B_{i}ρ}\right\}_{i∈\{1..n\}} & {Π^{ρ,σ,D} \atop \{B_{i}ρ\}_{i∈\{1..n\}}, Dσ, Γ′ρ ⟶ Cρ} \\ Δ_{1}ρ, …, Δ_{n}ρ, Dσ, Γ′ρ ⟶ Cρ \end{matrix} mc\} Δ_{1}, …, Δ_{n}, A, Γ′ ⟶ C def L .

−/ ∘ R: If Π is

\begin{matrix}\{ & {Π^{i} \atop B_{1}, …, B_{n}, Γ^{i} ⟶ C^{i}} & \} \\ B_{1}, …, B_{n}, Γ ⟶ C \end{matrix} ∘R ,

where ∘R is any right rule, then Ξ reduces to

\{{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π^{i} \atop B_{1}, …, B_{n}, Γ^{i} ⟶ C^{i}} Δ_{1}, …, Δ_{n}, Γ^{i} ⟶ C^{i} mc\} Δ_{1}, …, Δ_{n}, Γ ⟶ C ∘R .

Multicut cases: mc/ ∘ L: If Π ends with a left rule other than cL acting on B_{1} and Π_{1} ends with a multicut and

reduces to Π′_{1}, then Ξ reduces to

{Π′_{1} \atop Δ_{1} ⟶ B_{1}} {Π_{2} \atop Δ_{2} ⟶ B_{2}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π \atop B_{1}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

−/mc: Suppose Π is

\begin{matrix}\left\{{Π^{j} \atop \{B_{i}\}_{i∈I^{j}}, Γ^{j} ⟶ D^{j}}\right\}_{j∈\{1..m\}} & {Π′ \atop \{D^{j}\}_{j∈\{1..m\}}, \{B_{i}\}_{i∈I′}, Γ′ ⟶ C} \\ B_{1}, …, B_{n}, Γ^{1}, …, Γ^{m}, Γ′ ⟶ C \end{matrix} mc ,

where I^{1}, …, I^{m}, I′ partition the formulas {B_{i}}_{i∈{1..n}} among the premise derivations Π_{1},

…, Π_{m},Π′. For 1 ≤ j ≤ m let Ξ^{j} be

\begin{matrix}\left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈I^{j}} & {Π^{j} \atop \{B_{i}\}_{i∈I^{j}}, Γ^{j} ⟶ D^{j}} \\ \{Δ_{i}\}_{i∈I^{j}}, Γ^{j} ⟶ D^{j} \end{matrix} mc .

Then Ξ reduces to

\left\{{Ξ^{j} \atop … ⟶ D^{j}}\right\}_{j∈\{1..m\}} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈I′} {Π′ \atop … ⟶ C} Δ_{1}, …, Δ_{n}, Γ^{1}, … Γ^{m}, Γ′ ⟶ C mc .

Structural case:

−/cL: If Π is

{Π′ \atop B_{1}, B_{1}, B_{2}, …, B_{n}, Γ ⟶ C} ; B_{1}, …, B_{n}, Γ ⟶ C cL ,

then Ξ reduces to

{Π_{1} \atop Δ_{1} ⟶ B_{1}} \left\{{Π_{i} \atop Δ_{i} ⟶ B_{i}}\right\}_{i∈\{1..n\}} {Π′ \atop B_{1}, B_{1}, B_{2}, …, B_{n}, Γ ⟶ C} Δ_{1}, Δ_{1}, Δ_{2}, …, Δ_{n}, Γ ⟶ C mc cL Δ_{1}, …, Δ_{n}, Γ ⟶ C .

\underline{Axiom cases:}

init/ ∘ L: If Π ends with either natL or def L acting on B_{1} and Π_{1} ends with the init rule, then Ξ reduces to

{Π_{2} \atop Δ_{2} ⟶ B_{2}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {w(Δ_{1} \ B_{1}, Π) \atop Δ_{1}, B_{2}, …, B_{n}, Γ ⟶ C} Δ_{1}, …, Δ_{n}, Γ ⟶ C mc .

−/init: If Π ends with the init rule and C is a formula in Γ, then Ξ reduces to

Δ_{1}, …, Δ_{n}, Γ ⟶ C init .

If Π ends with the init rule, but C is not a formula in Γ, then C must be one of the cut formulas, say B_{1}. In this case Ξ reduces to w(Δ_{2} ∪ … ∪ Δ_{n} ∪ Γ, Π_{1}).

An inspection of the rules of the logic and this definition will reveal that every derivation ending with a multicut has a reduct. Because we use a multiset as the left side of the sequent, there may be ambiguity as to whether a formula occurring on the left side of the rightmost premise to a multicut rule is in fact a cut formula, and if so, which of the left premises corresponds to it. As a result, several of the reduction rules may apply, and so a derivation may have multiple reducts.

The following lemma states that the reduction relation is preserved by weakening.

Lemma 14 If Ξ reduces to Ξ′, then, for any multiset Δ of formulas, w(Δ, Ξ) reduces to w(Δ, Ξ′).

The proof of this lemma is a simple case analysis on the relevant clauses of Def. 13 and makes use of Def. 8 and Lemmas 11 and 12.

6 Normalizability and Reducibility

We now define two properties of derivations: normalizability and reducibility. Each of these properties implies that the derivation can be reduced to a cut-free derivation of the same end-sequent.

Definition 15 We define the set of normalizable derivations to be the smallest set that satisfies the following conditions:

1. If a derivation Π ends with a multicut, then it is normalizable if for every substitution θ there is a normalizable reduct of Πθ.

2. If a derivation ends with any rule other than a multicut, then it is normalizable if the premise derivations are normalizable.

These clauses assert that a given derivation is normalizable provided certain (perhaps infinitely many) other derivations are normalizable. If we call these other derivations the predecessors of the given derivation, then a derivation is normalizable if and only if the tree of the derivation and its successive predecessors is well-founded. In this case, the well-founded tree is call the normalization of the derivation.

Since a normalization is well-founded, it has an associated induction principle: for any property P of derivations, if for every derivation Π in the normalization, P holds for every predecessor of Π implies that P holds for Π, then P holds for every derivation in the normalization.

Lemma 16 If there is a normalizable derivation of a sequent, then there is a cut-free derivation of the sequent.

Proof Let Π be a normalizable derivation of the sequent Γ ⟶ B. We show by induction on the normalization of Π that there is a cut-free derivation of Γ ⟶ B.

1. If Π ends with a multicut, then one of its reducts is one of its predecessors (by way of the empty substitution) and so is normalizable. But the reduct is also a derivation of Γ ⟶ B, so by the induction hypothesis this sequent has a cut-free derivation.

2. Suppose Π ends with a rule other than multicut. Since we are given that Π is normalizable, by definition the premise derivations are normalizable. These premise derivations are the predecessors of Π, so by the induction hypothesis there are cut-free derivations of the premises. Thus there is a cut-free derivation of Γ ⟶ B.

The next two lemmas are also proved by induction on the normalization of the given derivation. The proof of the second lemma uses Lemmas 11 and 14 for the case when the derivation ends with a multicut.

Lemma 17 If Π is a normalizable derivation, then for any substitution θ, Πθ is normalizable.

Lemma 18 If Π is a normalizable derivation, then for any multiset Δ of formulas, w(Δ, Π) is normalizable.

We now define the property of reducibility for derivations. We do this by induction on the level of the derivation: in the definition of reducibility for derivations of level i we assume that reducibility is already defined for all levels j < i. (Recall from Definition 1 that the level of a derivation is defined to be the level of the consequent of its end-sequent.)

Definition 19 For any i, we define the set of reducible i-level derivations to be the smallest set of i-level derivations that satisfies the following conditions:

1. If a derivation Π ends with a multicut, then it is reducible if for every substitution θ there is a reducible reduct of Πθ.

2. Suppose the derivation ends with the implication right rule

{Π \atop B, Γ ⟶ C} ; Γ ⟶ B ⊃ C ⊃ R .

Then the derivation is reducible if the premise derivation Π is reducible and, for every substitution θ, multiset Δ of formulas, and reducible derivation Π′ of Δ ⟶ Bθ, the derivation

\begin{matrix}{Π′ \atop Δ ⟶ Bθ} & {Πθ \atop Bθ, Γθ ⟶ Cθ} \\ Δ, Γθ ⟶ Cθ \end{matrix} mc

is reducible.

3. If the derivation ends with the implication left rule or the nat left rule, then it is reducible if the right premise derivation is reducible and the other premise derivations are normalizable.

4. If the derivation ends with any other rule, then it is reducible if the premise derivations are reducible.

These clauses assert that a given derivation is reducible provided certain (perhaps infinitely many) other derivations are reducible. If we call these other derivations the predecessors of the given derivation, then a derivation is reducible only if the tree of the derivation and its successive predecessors is well-founded. In this case, the well-founded tree is call the reduction of the derivation.

In defining reducibility for a derivation of Γ ⟶ B ⊃ C ending with ⊃ R we quantify over reducible derivations of Δ ⟶ Bθ. This is legitimate since we are defining reducibility for a derivation having level max(lvl(B) + 1, lvl(C)), so the set of reducible derivations having level lvl(Bθ) = lvl(B) is already defined. For a derivation ending with ⊃ L or natL, some premise derivations may have consequents with a higher level than that of the consequent of the conclusion. As a result, we cannot use the reducibility of those premise derivations to define the reducibility of the derivation as a whole, since the reducibility of the premise derivations may not yet be defined. Thus we use the weaker notion of normalizability for those premise derivations. Also observe that the consequent of the premise to the rule def R cannot have a higher level than the consequent of the conclusion because of the level restriction on definitional clauses. Finally, as with normalizations, reductions have associated induction principles.

The following lemmas are proved by induction on the reduction of the given derivation. The proof of Lemma 20 is straightforward. The proofs of Lemmas 21 and 22 use Lemmas 17 and 18, respectively, for the case when the derivation ends with ⊃ L or natL. The proof of Lemma 22 also requires Lemmas 11 and 14.

Lemma 20 If a derivation is reducible, then it is normalizable.

Lemma 21 If Π is a reducible derivation, then for any substitution θ, Πθ is reducible.

Lemma 22 If Π is a reducible derivation, then for any multiset Δ of formulas, w(Δ, Π) is reducible.

7 Cut-Elimination

In the previous section we proved that every reducible derivation is normalizable and that every normalizable derivation can be reduced to a cut-free derivation of the same end-sequent. In this section we show that every F Oλ^{ΔIN} derivation is reducible, and thus every derivable sequent can be derived without the cut rule. The consistency of F Oλ^{ΔIN} is then a simple corollary of the cut-elimination theorem.

Lemma 23 For any derivation Π of B_{1}, …, B_{n}, Γ ⟶ C and reducible derivations Π_{1}, …, Π_{n} of Δ_{1} ⟶ B_{1}, …, Δ_{n} ⟶ B_{n} (n ≥ 0), the derivation Ξ

{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π \atop B_{1}, …, B_{n}, Γ ⟶ C}

Δ_{1}, …, Δ_{n}, Γ ⟶ C mc

is reducible.

Proof The proof is by induction on ht(Π), with subordinate inductions on n and on the reductions of Π_{1}, …, Π_{n}. The proof does not rely on the order of the inductions on reductions. Thus when we need to distinguish one of the Π_{i}, we shall refer to it as Π_{1} without loss of generality.

The derivation Ξ is reducible if for every substitution θ some reduct of Ξθ is reducible. If n = 0, then Ξθ reduces to Πθ. By Lemma 21 it suffices to show that Π is reducible. This is proved by a case analysis of the last rule in Π. For each case, the result follows easily from the outer induction hypothesis and Definition 19. The ⊃ R case requires that substitution for variables doesn’t increase the measure of a derivation (Lemma 7). In the cases for ⊃ L and natL we need the additional information that reducibility implies normalizability (Lemma 20).

For n > 0 we proceed with a case analysis of the reduction rules that apply to Ξ (and thus to Ξθ) to show that in fact every reduct of Ξθ is reducible. Most cases follow easily from the induction hypothesis, Definition 19, and Lemmas 7, 10, 17, 18, 20, 21, and 22. We show the interesting cases below.

⊃ R/ ⊃ L: Π_{1} and Π are

{Π′_{1} \atop B′_{1}, Δ_{1} ⟶ B′′_{1}} ; Δ_{1} ⟶ B′_{1} ⊃ B′′_{1} ⊃ R \begin{matrix}{Π′ \atop B_{2}, …, B_{n}, Γ ⟶ B′_{1}} & {Π′′ \atop B′′_{1}, B_{2}, …, B_{n}, Γ ⟶ C} \\ B′_{1} ⊃ B′′_{1}, B_{2}, …, B_{n}, Γ ⟶ C \end{matrix} ⊃ L .

Recall that substitution for variables preserves reducibility (Lemma 21) and does not increase the measure of a derivation (Lemma 7). Thus the derivation Ξ_{1}

{Π_{2}θ \atop Δ_{2}θ ⟶ B_{2}θ} ⋯ {Π_{n}θ \atop Δ_{n}θ ⟶ B_{n}θ} {Π′θ \atop B_{2}θ, …, B_{n}θ, Γθ ⟶ B′_{1}θ}

Δ_{2}θ, …, Δ_{n}θ, Γθ ⟶ B′_{1}θ mc

is reducible by the outer induction hypothesis. Since we are given that Π_{1} is reducible, by Definition 19 the derivation Ξ_{2}

{Ξ_{1} \atop Δ_{2}θ, …, Δ_{n}θ, Γθ ⟶ B′_{1}θ} {Π′_{1}θ \atop B′_{1}θ, Δ_{1}θ ⟶ B′′_{1}θ}

Δ_{1}θ, …, Δ_{n}θ, Γθ ⟶ B′′_{1}θ mc

is reducible. Therefore the derivation

{Ξ_{2} \atop … ⟶ B′′_{1}θ} \left\{{Π_{i}θ \atop Δ_{i}θ ⟶ B_{i}θ}\right\}_{i∈\{2..n\}} {Π′′θ \atop B′′_{1}θ, \{B_{i}θ\}_{i∈\{2..n\}}, Γθ ⟶ Cθ} Δ_{1}θ, …, Δ_{n}θ, Γθ, Δ_{2}θ, …, Δ_{n}θ, Γθ ⟶ Cθ mc cL Δ_{1}θ, …, Δ_{n}θ, Γθ ⟶ Cθ ,

which is the reduct of Ξθ, is reducible by the outer induction hypothesis and Definition 19.

natR/natL: Π_{1} is

{Π′_{1} \atop Δ_{1} ⟶ nat I}

Δ_{1} ⟶ nat (s I)

natR

and Π is

{Π′ \atop ⟶ D z} {Π′′ \atop D j ⟶ D (s j)} {Π′′′ \atop D (s I), B_{2}, …, B_{n}, Γ ⟶ C} nat (s I), B_{2}, …, B_{n}, Γ ⟶ C natL .

Consider the derivation Ξ_{1}

{Π′_{1} \atop Δ_{1} ⟶ nat I} {Π′ \atop ⟶ D z} {Π′′ \atop D j ⟶ D (s j)} D I ⟶ D I init nat I ⟶ D I natL Δ_{1} ⟶ D I mc .

Since the measure of the right premise derivation is no larger than ht(Π), Ξ_{1} is reducible by induction on the reduction of Π_{1} (Π′_{1} is a predecessor of Π_{1}). Again recall that substitution for variables preserves reducibility (Lemma 21) and does not increase the measure of a derivation (Lemma 7). The derivation Ξ_{2}

\begin{matrix}{Ξ_{1}θ \atop Δ_{1}θ ⟶ Dθ Iθ} & {Π′′θ[Iθ/j] \atop Dθ Iθ ⟶ Dθ (s Iθ)} \\ Δ_{1}θ ⟶ Dθ (s Iθ) \end{matrix} mc

is then reducible by the outer induction hypothesis. Therefore the derivation

{Ξ_{2} \atop Δ_{1}θ ⟶ Dθ (s Iθ)} \left\{{Π_{i}θ \atop Δ_{i}θ ⟶ B_{i}θ}\right\}_{i∈\{2..n\}} {Π′′′θ \atop … ⟶ Cθ} Δ_{1}θ, …, Δ_{n}θ, Γθ ⟶ Cθ mc ,

which is the reduct of Ξθ, is reducible by the outer induction hypothesis. def L/ ∘ L: Π_{1} and Π_{1}θ are

\begin{matrix}\{ & {Π_{1}^{ρ,σ,D} \atop Dσ, Δ′_{1}ρ ⟶ B_{1}ρ} & \} \\ A, Δ′_{1} ⟶ B_{1} \end{matrix} def L \begin{matrix}\{ & {Π_{1}^{θ∘ρ′,σ′,D} \atop Dσ′, Δ′_{1}θρ′ ⟶ B_{1}θρ′} & \} \\ Aθ, Δ′_{1}θ ⟶ B_{1}θ \end{matrix} def L .

The derivation Ξ^{ρ′,σ′,D}

{Π_{1}^{θ∘ρ′,σ′,D} \atop Dσ′, Δ′_{1}θρ′ ⟶ B_{1}θρ′} \left\{{Π_{i}θρ′ \atop Δ_{i}θρ′ ⟶ B_{i}θρ′}\right\}_{i∈\{2..n\}} {Πθρ′ \atop … ⟶ Cθρ′} Dσ′, Δ′_{1}θρ′, Δ_{2}θρ′, …, Δ_{n}θρ′, Γθρ′ ⟶ Cθρ′ mc .

is reducible by Lemmas 7 and 21 and induction on the reduction of Π_{1} (Π_{1}^{θ∘ρ′,σ′,D} is a predecessor of Π_{1}). Therefore the derivation

\left\{{Ξ^{ρ′,σ′,D} \atop Dσ′, Δ′_{1}θρ′, Δ_{2}θρ′, …, Δ_{n}θρ′, Γθρ′ ⟶ Cθρ′}\right\} Aθ, Δ′_{1}θ, Δ_{2}θ, …, Δ_{n}θ, Γθ ⟶ Cθ def L ,

which is the reduct of Ξθ, is reducible by Definition 19.

−/ ⊃ R: Ξ has the form

{Π_{1} \atop Δ_{1} ⟶ B_{1}} ⋯ {Π_{n} \atop Δ_{n} ⟶ B_{n}} {Π′ \atop C′, B_{1}, …, B_{n}, Γ ⟶ C′′} ; B_{1}, …, B_{n}, Γ ⟶ C′ ⊃ C′′ ⊃ R Δ_{1}, …, Δ_{n}, Γ ⟶ C′ ⊃ C′′ mc .

Once again recall that substitution for variables preserves reducibility (Lemma 21) and does not increase the measure of a derivation (Lemma 7). The derivation Ξ_{1}

{Π_{1}θ \atop Δ_{1}θ ⟶ B_{1}θ} ⋯ {Π_{n}θ \atop Δ_{n}θ ⟶ B_{n}θ} {Π′θ \atop C′θ, B_{1}θ, …, B_{n}θ, Γθ ⟶ C′′θ}

C′θ, Δ_{1}θ, …, Δ_{n}θ, Γθ ⟶ C′′θ mc

is reducible by the outer induction hypothesis. For any substitutions θ′ and θ′′ and reducible derivation Ξ′, the derivation

{Ξ′θ′′ \atop (Δ′ ⟶ C′θθ′)θ′′} \left\{{Π_{i}θθ′θ′′ \atop (Δ_{i} ⟶ B_{i})θθ′θ′′}\right\}_{i∈\{1..n\}} {Π′θθ′θ′′ \atop (… ⟶ C′′)θθ′θ′′}

Δ′θ′′, Δ_{1}θθ′θ′′, …, Δ_{n}θθ′θ′′, Γθθ′θ′′ ⟶ C′′θθ′θ′′ mc

is reducible by the outer induction hypothesis. This is a reduct of Ξ_{2}θ′′, where Ξ_{2} is

{Ξ′ \atop Δ′ ⟶ C′θθ′} {Ξ_{1}θ′ \atop C′θθ′, Δ_{1}θθ′, …, Δ_{n}θθ′, Γθθ′ ⟶ C′′θθ′} Δ′, Δ_{1}θθ′, …, Δ_{n}θθ′, Γθθ′ ⟶ C′′θθ′ mc .

Since a reduct of Ξ_{2}θ′′ is reducible for every θ′′, by Definition 19 Ξ_{2} is reducible. Since Ξ_{1} is reducible and Ξ_{2} is reducible for every substitution θ′ and reducible derivation Ξ′, by Definition 19

{Ξ_{1} \atop C′θ, Δ_{1}θ, …, Δ_{n}θ, Γθ ⟶ C′′θ} ; Δ_{1}θ, …, Δ_{n}θ, Γθ ⟶ C′θ ⊃ C′′θ ⊃ R

is reducible. This last derivation is the reduct of Ξθ by the current reduction rule.

Corollary 24 Every derivation is reducible.

Proof This result follows immediately from Lemma 23 with n = 0.

Theorem 25 If a sequent is derivable, then there is a cut-free derivation of the sequent.

Proof This result follows immediately from Corollary 24, Lemma 20, and Lemma 16.

Since there is no right rule for ⊥, there is no cut-free derivation of ⟶ ⊥. Thus consistency is a simple corollary of cut-elimination.

Corollary 26 There is no F Oλ^{ΔIN} derivation of the sequent ⟶ ⊥.

8 Related Work

The logic F Oλ^{ΔIN} is related to Schroeder-Heister’s “logics with definitional reflection” [24]. He proved cut-elimination for two logics: the first without contraction but allowing arbitrary implications in definitions, the second with contraction but only implication-free definitions. He also showed a counter-example to cut-elimination for the logic with both contraction and definitions with arbitrary implications, but conjectured that cut-elimination should hold if the definitions were stratified (as we accomplish in F Oλ^{ΔIN} through the level restriction). The proof presented in this paper clearly establishes that Schroeder-Heister’s conjecture is true.

However, there are significant differences between Schroeder-Heister’s logics and ours. The first is that F Oλ^{ΔIN} uses a stronger version of the left rule for definitions; Schroeder-Heister has extended his cut-elimination results to logics with this stronger rule [25]. More significantly, Schroeder-Heister has no induction rules in his logics. Because of the presence of the natL rule in F Oλ^{ΔIN}, Schroeder-Heister’s cut-elimination proofs do not extend to our setting.

The proof of cut-elimination presented in this paper is patterned after Martin-Löf’s normalization proof for a natural deduction system with iterated inductive definitions [12]. Our work can be viewed as an adaptation of his to the sequent calculus setting: our rules for definitions and natural numbers roughly correspond to his introduction and elimination rules for inductively defined predicates.

Acknowledgments

We gratefully acknowledge interaction with Catuscia Palamidessi which led to the introduction of levels to allow restricted use of implication in definitions. The authors have been funded in part by the grants ONR N00014-93-1-1324, NSF CCR-92-09224, NSF CCR-94-00907, ARO DAAH04-95-1-0092, and AFOSR F49620-96-1-0204.

References

[1] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.

[2] Jawahar Chirimar. Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania, February 1995.

[3] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[4] K. L. Clark. Negation as failure. In J. Gallaire and J. Minker, editors, Logic and Data Bases, pages 293–322. Plenum Press, New York, 1978.

[5] Lars-Henrik Eriksson. A finitary version of the calculus of partial inductive definitions. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions to Logic Programming, volume 596 of Lecture Notes in Artificial Intelligence, pages 89–134. Springer-Verlag, 1991.

[6] Lars-Henrik Eriksson. Pi: an interactive derivation editor for the calculus of partial inductive definitions. In A. Bundy, editor, Proceedings of the Twelfth International Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 821–825. Springer-Verlag, June 1994.

[7] Gerhard Gentzen. Investigations into logical deductions, 1935. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68–131. North-Holland Publishing Co., 1969.

[8] Jean-Yves Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’émination des coupures dans l’analyse et la théorie des types. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 63–92, Amsterdam, 1971. North-Holland.

[9] Jean-Yves Girard. A fixpoint theorem in linear logic. A message posted on the

linear@cs.stanford.edu mailing list, http://www.csl.sri.com/linear/mailing-list-
traffic/www/07/mail_3.html, February 1992.

[10] John Hannan. Extended natural semantics. Journal of Functional Programming, 3(2):123–152, April 1993.

[11] Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

[12] Per Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 179–216. North-Holland, 1971.

[13] Raymond McDowell. Reasoning in a Logic with Definitions and Induction. PhD thesis, University of Pennsylvania, December 1997.

[14] Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax. In G. Winskel, editor, Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1997.

[15] Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus: Preliminary report. In Proceedings of the 1996 Workshop on Linear Logic, volume 3 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996.

[16] Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus. Theoretical Computer Science, to appear. Preliminary version appeared as [15].

[17] Dale Miller. Forum: A multiple-conclusion specification language. Theoretical Computer Science, 165:201–232, 1996.

[18] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

[19] Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777– 814, October 1990.

[20] David Patterson and John Hennessy. Computer Architecture: A Quantitative Approach. Morgan Kaufman Publishers, Inc., 1990.

[21] Christine Paulin-Mohring. Inductive definitions in the system Coq: Rules and properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 328–345, 1993.

[22] Frank Pfenning. The practice of logical frameworks. In Hélène Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, volume 1059 of Springer-Verlag LNCS, pages 119–134, April 1996.

[23] Frank Pfenning and Conal Elliot. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, June 1988.

[24] Peter Schroeder-Heister. Cut-elimination in logics with definitional reflection. In D. Pearce and H. Wansing, editors, Nonclassical Logics and Information Processing, volume 619 of Lecture Notes in Computer Science, pages 146–171. Springer-Verlag, 1992.

[25] Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 222–232. IEEE Computer Society Press, June 1993.

[26] Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for lf. To appear at CADE-15, Lindau, Germany, July 1998.

[27] John Slaney. Solution to a problem of Ono and Komori. Journal of Philosophic Logic, 18:103– 111, 1989.

[28] R. F. Stärk. Cut-property and negation as failure. International Journal of Foundations of Computer Science, 5(2):129–164, 1994.

[29] W.W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198–212, 1967.

Papers by McDowell are available via anonymous ftp from ftp.cis.upenn.edu in pub/papers/mcdowell or via the WWW at http://www.cis.upenn.edu/~mcdowell. Papers by Miller are available via anonymous

ftp from ftp.cse.psu.edu in pub/dale or via the WWW at http://www.cse.psu.edu/~dale.