Weak reduction in sequent calculus — Draft version

Hugo Herbelin^{∗} INRIA, LIP-IMAG URA 1398, ENS Lyon

January 21, 1996

Abstract

Interpreting classical proofs as winning strategies for a certain game, Coquand [5] has defined a new kind of cut-elimination by letting winning strategies interact one against the other. This interaction can be proved to correspond to a cut-elimination procedure explicitly reduced according to a weak strategy. In this paper, we place ourselves in a quite general framework of sequents and give a cut-elimination procedure for it. We consider then a weak strategy of reduction (a call by name strategy of reduction) for this procedure. A special interest in weak reduction is that it enjoys a kind of optimality result: it computes only what is needed. Apart from this, an overview of the non-determinism of cut-elimination is done in the very last section.

Contents

1 Introduction 3

2 Infinitary propositional calculus 5 2.1 Formulas and sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Cut-elimination 6 3.1 The Hauptsatz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 The atomic steps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.3 The proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.4 Computational contents of the cut-elimination proof . . . . . . . . . . . . . . . 10

4 An innermost strategy of cut-elimination 12 4.1 Term notation for proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.2 Atomic steps in term notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.3 The innermost strategy of reduction . . . . . . . . . . . . . . . . . . . . . . . . 14 4.4 The termination of the innermost strategy of reduction . . . . . . . . . . . . . . 15 5 Strategy of outermost cut-elimination 15

∗Author’s address: INRIA, BP 105, Domaine de Voluceau F-78153 Rocquencourt Cedex, France. Internet:

Hugo.Herbelin@inria.fr.

This research was partly supported by ESPRIT Basic Research Action “Types for Proofs and Programs” and by Programme de Recherche Coordonnées “Programmation avancée et Outils pour l’Intelligence Artificielle”.

5.1 An outermost strategy of reduction . . . . . . . . . . . . . . . . . . . . . . . . . 15 5.2 The termination of the outermost strategy of reduction . . . . . . . . . . . . . 17 5.3 Correctness of the outermost cut-elimination w.r.t. the innermost cut-elimination 18 5.4 Finiteness of weak reduction for atomic sequents . . . . . . . . . . . . . . . . . 19

6 Arbitrariness in cut-elimination procedures 20 6.1 Main atomic step . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.2 The ambiguous permutation atomic step . . . . . . . . . . . . . . . . . . . . . . 21 6.3 Permutation of the order of cuts . . . . . . . . . . . . . . . . . . . . . . . . . . 22 6.4 On the duplication of ∧-formulas . . . . . . . . . . . . . . . . . . . . . . . . . . 22

1 Introduction

Classical logic and sequent calculus Our work takes origin from the symmetric sequent calculus of Gentzen. In 1935, Gentzen described a new kind of calculus in a deduction-like style (in contrast with the axiomatic-style of Hilbert’s definition of logical calculus) that he called sequent calculus. He presented several versions of this kind of calculus, first for intuitionistic predicate logic and for classical predicate logic called LK [6], then for arithmetic [9]. The classical version of sequent calculus is specially striking. Effectively, classical reasoning is gained with a duality of the negation (e.g. ¬(A ∨ B) is identified with ¬A ∧ ¬B and ¬¬A is identified with A) while usual formulations of classical logic consist in the addition of a classical axiom (typically the elimination of the double negation: ¬¬A ⇒ A) upon an intuitionistic structure. Gentzen [10] compares such an intuitionistic structure (the natural deduction) extended by a classical axiom with classical sequent calculus for arithmetic: “The special position of negation [...] which constituted a troublesome exception in the natural [deduction] calculus has been completely removed in a seemingly magical way”.

Sequent calculus and cut-elimination The cut rule (“if A ∨ B and ¬A ∨ C then B ∨ C”) takes the place, in sequent calculus, of the modus ponens (“if A ⇒ B and A then B”) of intuitionistic logic. Gentzen’s Hauptsatz [6, 9] states that any proof with cuts can be reduced by cut-elimination into a cut-free proof. Seeing the things from another point a view, the Hauptsatz amounts to say that there is a constructive notion of proof of which the cut rule is excluded, and that the cut rule is an admissible rule of reasoning which brings nothing more to the provability (this approach is explicit in Martin-Löf [20] or Schütte [25]). Numerous cutelimination or cut-admissibility proofs have been described in the literature. A problem with all these proofs is that they are intrinsically non-deterministic (i.e. arbitrary choices have to be made to extract a deterministic procedure from them). We will analyse this non-determinism in the last section.

Computational contents of classical logic There is a computational interpretation of intuitionistic provability. Is it possible to give a computational interpretation to classical provability ? Until a couple of years ago, it was not clear. According to Gödel-like translations into intuitionistic logic, it should be, but what computationally happens in these translations was not clear. Another suggestive result was Kreisel’s result about the equivalence between intuitionistic and classical provability of purely existential statements (Σ_{1}^{0} statements). This expresses that, at least for a simple class of statements, there is a constructive meaning in classical logic. However, it was not understood how to assign an explicit computational contents to the elimination of the double negation and therefore no extension of Curry-Howard isomorphism was known for classical logic. On the sequent calculus side, it was possible to see a constructive meaning in cut-free proofs, but there were no real understanding of cut-elimination. In a sequential approach of the cut-elimination process, it was not possible to understand what could be the significance of the apparently arbitrary choices performed during the computation. In a non-deterministic approach (suggested by the apparent arbitrary of certain performed choices) of the cut-elimination process, it was also not clear how to interpret this non-determism.

Infinitary logic In 1935, in his first paper about the consistency of arithmetic [7], Gentzen defines, for arithmetic, a notion of “statability of a reduction rule” which amounts to the cut-free provability in a logic with the rule “if P (n) is provable for each n then ∀n.P (n) is provable” (ω-logic). He proves that for any provable statement of arithmetic, such a reduction rule is statable. It amounts to say, in a modern formulation, that there is a translation of arithmetic into ω-logic and that there is a cut-admissibility theorem for ω-logic. In 1941, Novikoff [22] defines an infinitary propositional calculus. He defines also a notion of regularity of the same kind as Gentzen’s statability of a reduction rule and proves that any rule (including modus ponens) of the infinitary propositional calculus preserves the regularity and all axioms are regular. As a special consequence of this, he intuitionistically infers the consistency of arithmetic. Both proofs of Gentzen and Novikoff entails that classically provable Σ_{1}^{0} formulas are also intuitionistically provable. This is implicit in Gentzen and explicit in Novikoff. Each of these proofs also, Novikoff’s proof of regularity and Gentzen’s first [7] (and galley [8]) proof of consistency for arithmetic are in fact cut-admissibility proofs for ω-logic. An explicit definition of a calculus with a rule having infinitely many premises appears in 1951, in Lorenzen [18]. For Lorenzen, the purpose is to use the Hauptsatz to obtain an intuitionistic proof of the consistency of a part of Russell’s type theory.

Recent constructive interpretations for classical logic In the past few years, important advances have been made in the subject. In 1990, Griffin [16] pointed out that a certain control operator (Felleisen’s operator C [17]) was typable by means of the classical axiom about the elimination of the double negation. (Such a control operator is an operator added to functional languages to simulate imperative features.) This was precised by Murthy in his thesis [21]. Shortly after, Girard [12, 13], Parigot [23, 24] and Coquand [3, 5] brought new approaches of classical logic. Girard introduced a new sequent calculus for classical logic for which a denotational semantic is available. Parigot enlarged natural deduction into a framework which he called free deduction, embedding both natural deduction and the cut-free part of sequent calculus. He defined also an extension of λ-calculus, the λμ-calculus which extends the Curry-Howard isomorphism to classical natural deduction.

Recent game-theoretic interpretations for classical logic Reconsidering the first consistency proof of Gentzen [1, 7, 8], Coquand gave a game-theoretic approach of provability. Cut-free proofs are winning strategies for a certain game. Cuts are seen as a play between proofs and the elimination of cuts as the result of letting proofs play one against the other (an interaction). Such a game-theoretic approach was proposed in 1958 by Lorenzen [19], but only for cut-free intuitionistic proofs and not for cut-elimination. This approach appears to be closely related to call-by-name operational semantics of reduction in sequent calculus (what is called weak reduction in the sequel).

Weak strategy of reduction for cut-elimination According to the Curry-Howard isomorphism, a constructive proof of cut-elimination (or cut-admissibility) means that there is a terminating procedure mapping two cut-free proofs, one of B ∨ ¬A, the other of C ∨ A to a cut-free proof of B ∨ C. What we do here is to consider such a cut-elimination procedure and focus on a special evaluation order for cut-elimination: a weak strategy of cut-elimination. Weak reduction in λ-calculus stands for a reduction which never reduces under abstraction. Here, in sequent calculus, we talk about weak reduction in the sense of a reduction which eliminates the outermost cut if any and never reduces under a rule of connective introduction. This is of special interest for two reasons. First, in an infinitary sequent calculus, such as the one we consider in this paper, where proofs are transfinite objects and cut-elimination is a transfinite procedure, the weak strategy of reduction yields cut-free proofs of Σ_{1}^{0} formulas in a finite number of steps. Roughly speaking, this is because the weak reduction computes only what is needed. Secondly, but it is not shown here (and nowhere else yet), this weak reduction corresponds to Coquand’s interaction. Thus the termination of weak reduction for proofs of Σ_{1}^{0} formulas should give an alternative proof of termination of the interaction.

Proofs of termination of particular strategies of cut-elimination Applying recursively weak cut-elimination under the rules of introduction of connectives gives a complete procedure of cut-elimination, that we call outermost strategy of cut-elimination. We compare this procedure for which a strategy of reduction is associated to the same procedure for which an innermost strategy of reduction is associated. It is surprising because the proof of cut-elimination in our (infinitary) sequent calculus directly applies to show the (transfinite) termination of the innermost strategy of reduction while a strengthening of the argument is needed to show the (transfinite) termination of the outermost strategy of cut-elimination.

2 Infinitary propositional calculus

We first describe in this section a logical calculus as in Martin-Löf [20]. One interest in this calculus, besides its power, is the simplicity of its syntax. It can be understood as an infinitary propositional calculus as described in Tait [27]. There is no variable, atoms are reduced to boolean values and connectives are confined to disjunction and conjunction, but both are possibly infinite. The cut rule is an explicit rule of the calculus and Gentzen’s Hauptsatz states that this cut rule is redundant. We give at the end of the section such a proof of the Hauptsatz and then a term notation for proofs.

2.1 Formulas and sequents

The two connectives are written ∨ and ∧ and consist in possibly infinite disjunctions and conjunctions respectively. Atoms, reduced to boolean values, are themselves encoded with the connectives ∨ and ∧. A conjunction with no conjuncts stands for the true proposition. A disjunction with no disjuncts stands for the false proposition.

Formulas are well-founded trees with ∧- and ∨-nodes.

Definition 1 Formulas are defined inductively by the following rule:

• If (A_{i})_{i∈I} is a family of formulas then ∨_{i∈I}A_{i} and ∧_{i∈I}A_{i} are formulas.

Formulas ∨_{i∈I}A_{i} are called ∨-formulas or disjunctive formulas and formulas ∧_{i∈I}A_{i} are called ∧-formulas or conjunctive formulas. The formula ∨_{i∈∅}, also written 0 is called the false atomic formula and the formula ∧_{i∈∅}, also written 1 is called the true atomic formula.

We define also subformulas of a formula as usual.

Remark: We put no condition on the sets I ranged by the indices. All works well by considering them in a abstract manner. See Tait [27] for a discussion about this.

Definition 2 The negation of F, written F^{⊥} is inductively defined as:

• (∨_{i∈I}A_{i})^{⊥} = ∧_{i∈I}A_{i}^{⊥}

• (∧_{i∈I}A_{i})^{⊥} = ∨_{i∈I}A_{i}^{⊥}

Note that we have 1^{⊥} = 0 and 0^{⊥} = 1. 0 and 1 are the only atoms.

Formulas are ranged over by uppercase latin letters A, B, ...

Definition 3 A sequent is a sequence of formulas

Δ, A, Γ, B,... stand for sequents where Δ, Γ are themselves sequences of formulas. (Δ_{i})_{i∈I} is a notation for a family of sequents indexed by i ∈ I. To consider sequents consisting of an infinite sequence of formulas poses no problem.

2.2 Proofs

Definition 4 A proof is a well-founded tree defined inductively by means of the three following inferences:

{Γ, ∨_{i∈I}A_{i}, A_{i_{0}} \atop Γ, ∨_{i∈I}A_{i}} ∨-intro

\begin{matrix}(Γ, ∧_{i∈I}A_{i}, A_{i}) & i∈I \\ Γ, ∧_{i∈I}A_{i} \end{matrix} ∧-intro

(Observe that I may be infinite.)

{Γ, Γ_{1}, A  Γ, Γ_{2}, A^{⊥} \atop Γ, Γ_{1}, Γ_{2}} cut

In all these rules, Γ, Γ_{1}, Γ_{2} are called contexts. In the cut rule, A and A^{⊥} are called cut formulas.

Definition 5 A cut-free proof (cf-proof) is a proof which does not use the cut rule.

Remarks

• There is no explicit axiom rule, but as a special case of the ∧-introduction, when I = ∅, we get an axiom rule

Γ, 1 axiom

• There is no contraction rule. Each rule of our calculus performs contraction at the same time. By means of the presence of ∨_{i∈I}A_{i} (resp ∧_{j∈J}A_{j}) in the upper sequent, ∨-intro rule (resp ∧-intro rule) performs contraction in the same time as the introduction. As for the cut rule, a common Γ and specific Γ_{1} and Γ_{2} make contraction available in the same time as the cut. When no contraction is intended in introduction rules, a superfluous occurrence remains in the sequent and appears in the axiom as a side (and irrelevant) formula.

• There is no weakening rule, but an arbitrary number of formulas may occur in the axioms.

• We need an exchange rule but we do not write it explicitly.

• Any formula appearing in an axiom rule can be traced along the proof, having in mind the exchange rule. Either it disappears at the time of an introduction rule or of a cut rule, or it goes through the end sequent of the proof.

• We do not want to consider sequents as multisets, because in such a case, the two following proofs would have been identified.

(\begin{matrix}\binom{⋮ . π_{ii′}}{A_{j_{0}i},  A_{j_{0}i′}} & i′∈I \\ A_{j_{0}i},  ∧_{i∈I}A_{j_{0}i} \end{matrix} ∧-intro)_{i∈I} ∧_{i∈I}A_{j_{0}i},  ∧_{i∈I}A_{j_{0}i} ∧-intro

∧_{i∈I}A_{j_{0}i}, ∨_{j∈J} ∧_{i∈I} A_{ji} ∨-intro

∨_{j∈J} ∧_{i∈I} A_{ji} ∨-intro

(\begin{matrix}\binom{⋮ . π_{ii′}}{A_{j_{0}i}, A_{j_{0}i′}} & i′∈I \\ A_{j_{0}i}, ∧_{i∈I}A_{j_{0}i} \end{matrix} ∧-intro)_{i∈I} ∧_{i∈I}A_{j_{0}i}, ∧_{i∈I}A_{j_{0}i} ∧-intro

∨_{j∈J} ∧_{i∈I} A_{ji}, ∧_{i∈I}A_{j_{0}i} ∨-intro

∨_{j∈J} ∧_{i∈I} A_{ji} ∨-intro

3 Cut-elimination

3.1 The Hauptsatz

The fundamental theorem of Gentzen states that the cut rule is redundant:

Theorem of cut-elimination (Hauptsatz)

For any sequent Γ, if there is a proof of Γ using the cut rule, then there is a cut-free proof of Γ.

Remark: The Hauptsatz amounts to say that the primitive notion of proof is the one with the cut rule excepted, and that the cut rule is an admissible rule of reasoning (in the sense where it brings nothing more to the provability). This approach is explicit in Martin-Löf [20] or Schütte [25]. This approach is implicit in Gentzen [7] and in Novikoff [22] where the notions respectively of statability of a reduction rule for a sequent and of regularity for a formula amount to a notion of cut-free proof. (About statability of a reduction rule, Gentzen says that it “will serve as a formal replacement of the informal notion of truth” and that “it provides with a special finitist interpretation of propositions and takes the place of their actualist interpretation”). Their definitions mainly differ from our definition of cut-free proof by the allowance of contraction for ∧-formulas. The reason why we allow ∧-contraction is that it simplifies the definition of the cut-elimination: effectively when performing the cut-elimination process, ∧-contractions may appear, even when eliminating a cut between two cut-free proofs without ∧-contraction (see an example in last section). In Gentzen or Novikoff, extra lemmas to transform proofs with ∧-contractions into proofs without ∧-contractions are needed. So we get a more uniform approach by allowing ∧-contraction from the very beginning.

A constructive proof of the Hauptsatz provides an effective procedure which eliminates cuts. There are several such constructive proofs of the Hauptsatz in the literature (see the last section). The proof we give in the next section is built on cross-cut and can be found in Martin-Löf [20]. This proof, in fact like most of the informal proofs, leaves undetermined some points of the proof, typically to keep a symmetry which otherwise would be broken. For our purpose, we break — thus arbitrarily — such a non-determinism.

3.2 The atomic steps

We describe the cut-elimination proof by means of a set of rewriting rules, called atomic steps concerning proofs of our calculus. These atomic steps form the basic constituents of the proof. It can be checked that the rules exhaust all possible proof patterns having cut as main symbol. This entails that at least one rule is applicable to a non cf-proof.

There is no critical pairs in the set of rewriting rules and it is shown in the next section that the question of confluence for terminating strategies is answered in the affirmative.

According to the λ-calculus terminology, we call redexes the left members of the rewriting rules and contractum the right members.

Let Λ, Λ_{1} and Λ_{2} be sequents and ∧_{i∈I}A_{i} a formula. Let ρ be a proof of Λ, Λ_{1}, ∧_{i∈I}A_{i} and σ a proof of Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}.

An atomic step is one of the hereafter listed reduction rules applicable to the proof

π = \begin{matrix}{⋮ . ρ \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ, Λ_{1}, Λ_{2} \end{matrix} cut

• main atomic step

Both sides of the cut come from an introduction of the cut formula.

ρ = \begin{matrix}\binom{⋮ . ρ_{i}}{Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i}} & i∈I \\ Λ, Λ_{1}, ∧_{i∈I}A_{i} \end{matrix} ∧-intro  σ = {⋮ . σ_{i_{0}} \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}, A_{i_{0}}^{⊥}} ; Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥} ∨-intro

Then the cut pattern reduces to

\begin{matrix}{⋮ . ρ_{i_{0}} \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i_{0}}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i_{0}} \end{matrix} cut \begin{matrix}{⋮ . ρ \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}} & {⋮ . σ_{i_{0}} \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}, A_{i_{0}}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i_{0}}^{⊥} \end{matrix} cut

Λ, Λ_{1}, Λ_{2} cut

It is the way of solving this case which gives the name “cross-cut” to the procedure. Between ρ and σ a cross is drawn, leading to the cuts between ρ and σ_{i_{0}} and between ρ_{i_{0}} and σ.

• permutation atomic steps It corresponds to cases when the last rule of at least one side of the cut pattern consists in an introduction of a formula in the context. There are three cases.

– first case The ∧-side of the cut consists of the ∧-introduction of the cut formula, but the ∨-side of the cut consists of the introduction of a formula in Ω_{2} = Λ, Λ_{2}:

ρ = \begin{matrix}⋮ . ρ_{i} \\ (Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i}) & i∈I \end{matrix} ; Λ, Λ_{1}, ∧_{i∈I}A_{i} ∧-intro  σ = {⋮ . σ′ \atop Ω′_{2}, ∨_{i∈I}A_{i}^{⊥}} ; Ω_{2}, ∨_{i∈I}A_{i}^{⊥} intro in Ω_{2}

reduces to

\begin{matrix}{⋮ . ρ \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}} & {⋮ . σ′ \atop Ω′_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ_{1}, Ω′_{2} \end{matrix} cut
Λ, Λ_{1}, Λ_{2}

intro in Ω_{2}

where the rule “intro in Ω_{2}” stands for the introduction of a formula either in Λ or in Λ_{2}. To simplify, we write only one premise for this rule, but in case of the introduction of a ∧-formula, rigorously writing, there should be several premises.

– the second case is the symmetric of the first case by inverting the symbols ∧ and ∨.

– the third case is more problematic, it is when the last rule of both sides of the cut consists in the introduction of a formula of the context.

ρ = {⋮ . ρ′ \atop Ω′_{1}, ∧_{i∈I}A_{i}} ; Ω_{1}, ∧_{i∈I}A_{i} intro in Ω_{1}  σ = {⋮ . σ′ \atop Ω′_{2}, ∨_{i∈I}A_{i}^{⊥}} ; Ω_{2}, ∨_{i∈I}A_{i}^{⊥} intro in Ω_{2}

where Ω_{1} = Λ, Λ_{1} and Ω_{2} = Λ, Λ_{2}. To be deterministic, we have to make a choice. Our choice — arbitrarily — is to privilege the side with the ∧-formula. This gives the following rewriting:

\begin{matrix}{⋮ . ρ′ \atop Ω′_{1}, ∧_{i∈I}A_{i}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Ω′_{1}, Λ_{2} \end{matrix} cut
Ω_{1}, Λ_{2}

intro in Ω_{1} Having made this choice, we can remark that it corresponds to the same rewriting than the above second case. Thus we can put together this two rewritings rules by saying that

{⋮ . ρ′ \atop Ω′_{1}, ∧_{i∈I}A_{i}} ; Ω_{1}, ∧_{i∈I}A_{i} intro in Ω_{1} {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}}

Λ, Λ_{1}, Λ_{2} cut

reduces to

\begin{matrix}{⋮ . ρ′ \atop Ω′_{1}, ∧_{i∈I}A_{i}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Ω′_{1}, Λ_{2} \end{matrix} cut
Λ, Λ_{1}, Λ_{2}

intro in Ω_{1}

independently of which proof occurs on the ∨-side of the cut.

Remark: The cases which involve at least an axiom inference rule on one side are special cases of permutation step. Though not explicitly written, they are fundamental since they are the only cases which decrease the number of cut in the proof.

3.3 The proof

We state first the Hauptsatz about a cut between cut-free proofs. This amounts to a cutadmissibility theorem as discussed above.

Theorem of cut-admissibility

Let ρ be a cut-free proof of Γ, Γ_{1}, A and σ a cut-free proof of Γ, Γ_{2}, A^{⊥}. Then there exists a cut-free proof π of Γ, Γ_{1}, Γ_{2}.

Proof:

By induction first on A then on the pair of ρ and σ.

We do a unambiguous pattern-matching on

\begin{matrix}{⋮ . ρ \atop Γ, Γ_{1}, A} & {⋮ . σ \atop Γ, Γ_{2}, A^{⊥}} \\ Γ, Γ_{1}, Γ_{2} \end{matrix} cut

according to the system of rewriting rules and consider the right side of the rewriting rule. In case of main step, three new cuts are generated. The two upper ones verifies that the pair of proofs on the left-hand and right-hand side is lesser. We apply the induction hypothesis to get the existence of cut-free proofs od same conclusion. The size of the cut formula in the third and lower new generated cut is lesser. Again by induction hypothesis, we get the existence of a cut-free proof of Γ, Γ_{1}, Γ_{2}. In case of permutation steps, the pair of proof on the left-hand and right-hand side of the new cut is lesser. This is sufficient also to apply the induction hypothesis.

We now state the Hauptsatz in a general form.

Theorem of cut-elimination (Hauptsatz)

Let π be a proof of Γ. Then there exists a cut-free proof π′ of Γ.

Proof: By induction on π, using the admissibility of cut in case of a cut rule.

3.4 Computational contents of the cut-elimination proof

If we formalize this cut-elimination proof in a formal system such as the Calculus of Constructions (CC) or Martin-Löf’s type theory (ITT), systems built on the Curry-Howard isomorphism, which can be seen also as a programming language, it yields a program (a term) which takes as argument a proof containing cuts and outputs a cut-free proof. For both these languages a normalisation procedure for the terms of the language exists. A strong normalisation procedure for the Calculus of Constructions [2], a call by name procedure to put in “canonical” form for Martin-Löf’s type theory.

Up to some particularities of these formal systems, the obtained program is the following one that we have written in ML style. This is a simplified version, a complete and correct formulation can be found in appendix.

type proof =
   E_intro of name * name * I * proof
 | A_intro of name * name * (I -> proof)
 | Cut of name * proof * name * proof;;
let rec adm np p nq q =
   match p with
   E_intro(np',np'',i,p')
     -> let p'' = adm np p' nq q in
        E_intro(np',np'',i,p'')
 | A_intro(np',np'',pi)
     -> if np'<>np then
           let pi' = fun i -> adm np (pi i) nq q in
           A_intro(np',np'',pi')
        else (match q with
             A_intro(nq',nq'',qi)
               -> let qi' = fun i -> adm np p nq (qi i) in
                  A_intro(nq',nq'',qi')
           | E_intro(nq',nq'',i,q')
             -> if nq'<>nq then
                   let q'' = adm np p nq q' in
                   E_intro(nq',nq'',i,q'')
                else
                   let p0 = adm np (pi i) nq q in
                   let q0 = adm np p nq q' in
                   adm nq'' q0 np'' p0
           | _-> failwith "not a cut-free proof")
 | _-> failwith "not a cut-free proof";;
let rec elim p =
   match p with
   A_intro(np',np'',pi) -> A_intro(np',np'',fun i -> elim (pi i))
 | E_intro(np',np'',i,p') -> E_intro(np',np'',i,elim p')
 | Cut(np,p,nq,q) -> adm np (elim p) nq (elim q);;

Let us assume that, though the choice of a ML syntax, these programs are terms of CC (the let rec has to be replaced by an iterator). Let us assume that we restrict our attention to the class of proofs expressible in CC (i.e. as a term of type proof in the calculus: the class of proofs for which the functional argument in A_intro is expressible by a term of type I -> proof in Coc, i.e. the class of proofs for which the transfinite aspect can be captured by finistic means in CC (this is the case, in particular, of the proofs of arithmetic)). The strong normalisation theorem for CC implies the strong termination of the function elim when applied to a closed term of type proof. Moreover, we can remark that for any such term p of type proof, for any Cut in it, there exists an evaluation order which reduces first this Cut. This is a remarkable property of this program and this allows to derive the strong termination of the elimination of cut for this subset of proofs expressible in CC, from the strong termination of reduction in the Calculus of Constructions.

In the following sections, we consider reduction of infinitary proofs from an abstract point of view. That is, we do not assume that the functional argument of A_intro is expressible as a closed term of a known normalisable language, but rather consider it as an abstract function of which no special property is known. It can be any — actualist — family of proofs indexed on I.

We define two strategies of cut-elimination and prove their — transfinite — termination (it amounts to consider two strategies of reduction for the transfinite extension of the function elim). The first strategy is an innermost strategy of reduction. The second strategy is an outermost strategy of reduction. What is strange is that the termination of this innermost strategy of reduction derives directly from the argument of the Hauptsatz proof while the termination of this outermost strategy of reduction needs an extension of this argument.

In both cases, the termination needs an induction on the normal form of the proofs of the calculus. But for the induction step of the innermost reduction termination proof, we deal with proofs already in normal form. This is in contrast with the outermost reduction termination proof where we consider cuts between proofs not in normal form. In such a way to carry the induction, we need to take into account both the proofs and the normal form of these proofs.

Both proofs, but in fact also the Hauptsatz proof have the same following form. We prove by induction on the cut formula A, then on (p, q) (seen as a pair of cut-free proofs cut on A) that:

∀A, ∀(p, q), P (A, p, q)

The only difference between the three proofs is the choice of the predicate P. Informally, for the termination of the innermost reduction, P is “there exists r cut-free such that CUT (A, p, q) reduces to r following the innermost reduction”. For the termination of the outermost reduction, P is “for all (p′, q′) reducing respectively to (p, q) following the outermost reduction, there exists r cut-free such that CUT (A, p′, q; ) reduces to r following the outermost reduction”. For the Hauptsatz, P is “there exists r cut-free such that r proves the same sequent as CUT (A, p, q)”.

All three proofs use the same induction steps allowing to propagate the cut-admissibility to more and more complex proofs (see next sections).

All these proofs induces the same underlying program. Just the output of the program is different. Especially, we get the paradox that, if we are interested in the computation of the witness in the proof of the termination of the innermost reduction, then this witness may be computed by means of a radically different strategy of reduction than the innermost one.

It seems that there is a strong link with what happens in reducibility proofs à la Tait, where the reducibility lemma is a general result allowing to show several properties on λ-terms, assuming that these properties are saturated, closed (by application of terms to variables) and including the variables.

What remains strange is the fact that the termination of the outermost reduction can be deduce (in case of proofs expressible, say, in CC) from the proof of the Hauptsatz from the strong normalisation of the meta-system. Why a quantification upon all proofs having a given normal form is needed in one case but not in the other case. An intuitive idea is that the quantification is implicitly lifted at the meta-level : when we say that “there exists r cut-free such that ...”, it amounts to say “for all syntactic term of the meta-system justifying that “there exists r cut-free such that ...””.

It looks like if semantics at a level were family of convertible syntactic terms at the metalevel. Here again, it seems that there is a strong link with what happens in reducibility proofs.

The translation of a term into its semantics allows to recover the normal form by means of an implicit reduction hidden on the meta-level.

4 An innermost strategy of cut-elimination

We consider in this section the explicit reduction of the underlying procedure of the previous cut-elimination proof, according to an innermost strategy of reduction. A proof of termination is given. It directly follows the previous cut-elimination proof. In a first step, a term notation for proofs is described to avoid excessive amount of large proof trees and to handle more precisely with the proofs.

4.1 Term notation for proofs

This subsection describes a term notation for proofs. Though not indispensable, we adopt another approach of sequents. Here sequents are not sequences of formulas but rather sets of formulas with “names” associated to formulas in order to distinguish between distinct occurrences of similar formulas.

We admit the existence of a set N of which the elements are called names. We assume that the equality is decidable for names and that N is equipped with a map New which associates to any proper subset of it, a new name not belonging to the subset (a kind of “gensym”): for any X ⊂ N , X ≠ N implies New(X) ∉ X. In fact, such a set exists, typically the set of natural numbers or the set of string on a given alphabet.

Definition 6 Let X be a subset of N. A renaming map σ for X is a bijection from X to a certain subset Y of N disjoint from X. If x ∉ X and y ∉ Y, then σ ∪ {x → y} is the extension of σ from X ∪ {x} to Y ∪ {y}. The empty renaming map (from ∅ to ∅) is written ∅ and Rσ denotes the range of σ.

Definition 7 A sequent with names is the pair of a subset X ⊂ N and of a function which maps names of X to formulas. We usually write the function Γ and the sequent Γ^{X}. The formula of name x in Γ^{X} is written Γ^{x}. If X = X_{1} ∪ X_{2} with X_{1} and X_{2} disjoint, the sequent Γ^{X} is sometimes written Γ^{X_{1}}, Γ^{X_{2}}. Furthermore, if X is reduced to a singleton {x} then the sequent Γ^{X} is sometimes written Γ^{x} or even A^{x} if A is precisely the formula of name x by Γ.

To emphasis on whether a formula is conjunctive or disjunctive, names are written underlined for ∧-formulas and overlined for ∨-formulas.

Definition 8 proofs in term notation (or shortly proofs again) are inductively defined as follows:

• if p is a proof of a sequent with names Γ^{X}, (∨_{i∈I}A_{i})\overline{x}, (A_{i_{0}})^{x′}, then

\overline{x}!i_{0} ∈ I ↦^{x′} p

is a proof of Γ, (∨_{i∈I}A_{i})\overline{x}

• if (p_{i})_{i∈I} is a family of proofs such that for each i ∈ I, p_{i} is a proof of Γ^{X}, (∧_{i∈I}A_{i})\underline{x}, (A_{i_{0}})^{x′}, then

\underline{x}?i ∈ I ↦^{x′} p_{i}

is a proof of Γ^{X}, (∧_{i∈I}A_{i})\underline{x} where the same name \underline{x} is associated to ∧_{i∈I}A_{i} in each conjunct.

• if p is a proof of Γ^{X}, Γ_{1}^{X_{1}}, (∧_{i∈I}A_{i})\underline{x}, q a proof of Γ^{X}, Γ_{2}^{X_{2}}, (∨_{i∈I}A_{i}^{⊥})\overline{x}, σ_{1} a renaming map from X_{1} to Y_{1} and σ_{2} a renaming map from X_{2} to Y_{2} such that X, Y_{1} and Y_{2} are disjoint, then

CUT_{(σ_{1},σ_{2},X,\underline{x},\overline{x})}[p|q]

is a proof of Γ^{X}, Γ^{Y_{1}}, Γ^{Y_{2}}.

where for each y_{1} ∈ Y_{1}, Γ^{y_{1}} = Γ_{1}^{σ_{1}^{−1}(y_{1})} and for each y_{2} ∈ Y_{2}, Γ^{y_{2}} = Γ_{2}^{σ_{2}^{−1}(y_{2})}.

Remarks: 1) Except in the use of names in sequent instead of considering them as sequences, this follows the previous definition of proofs as trees. Let us notice that the names make that the exchange rule is not necessary. As a counterpart, the use of names makes that clash of names could occur during the cut elimination. To remedy this, the cut rule performs a renaming of the names which are not shared by both sides of the cut.

2) The notations ? and ! can be understood having in mind the following analogy : formulas are channels, cut is communication, ∨-introduction is data sending ∧-introduction is data receiving.

3) In the following sections, to shorten the notation, we write \overline{x}!i_{0} ↦^{x′} p (resp \underline{x}?i ↦^{x′} p_{i}) for

\overline{x}!i_{0} ∈ I ↦^{x′} p (resp \underline{x}?i ∈ I ↦^{x′} p_{i}). When talking about a proof in term notation, it is implicit that it is a correct proof of a certain sequent.

4) By convention, the left side of a cut is always the side with the ∧-occurrence of the cut formula. And vice-versa.

4) As before a proof is said to be cut-free (cf-proof) if and only if it does not contain CUT.

4.2 Atomic steps in term notation

We consider a more precise formulation of the atomic steps in term notation. A predicate relation ⟹^{h} is introduced in such a way that q ⟹^{h} r expresses that q reduces to r according to one of the atomic steps. This is a one-step head reduction.

Definition 9 The relation ⟹^{h} is defined by the following rules:

• if p = \underline{x}?i ↦^{x′} p_{i} and q = \overline{y}!i_{0} ↦^{y′} q_{i_{0}} such that \underline{x} = \underline{z} and \overline{y} = \overline{z} then, letting X′ = Rσ_{1} ∪ Rσ_{2} ∪ X, z′ = New(X′) and

\begin{matrix}p′ = CUT_{(σ_{1}∪(y′→z′),σ_{2},X,\underline{z},\overline{z})}[p|q_{i_{0}}] \\ q′ = CUT_{(σ_{1},σ_{2}∪(x′→z′),X′,\underline{z},\overline{z})}[p_{i_{0}}|q] \end{matrix} ,

CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{h} CUT_{(∅,∅,X,z′,z′)}[p′|q′]

• if p = \underline{x}?i ↦^{x′} p_{i} and q = \underline{y}?j ↦^{y′} q_{j} such that \underline{x} = \underline{z} then, letting y′′ = New(Rσ_{1} ∪ Rσ_{2} ∪ X),

CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{h} σ_{2}(\underline{y})?j ↦^{y′′} CUT_{(σ_{1},σ_{2}∪(y′→y′′),X,\underline{z},\overline{z})}[p|q_{j}]

• if p = \underline{x}?i ↦^{x′} p_{i} and q = \overline{y}!j_{0} ↦^{y′} q_{j_{0}} such that \underline{x} = \underline{z} and \overline{y} ≠ \overline{z} then, letting y′′ = New(Rσ_{1} ∪ Rσ_{2} ∪ X),

CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{h} σ_{2}(\overline{y})!j_{0} ↦^{y′′} CUT_{(σ_{1},σ_{2}∪(y′→y′′),X,\underline{z},\overline{z})}[p|q_{j_{0}}]

• if p = \overline{x}!j_{0} ↦^{x′} p_{j_{0}} then,

letting x′′ = New(Rσ_{1} ∪ Rσ_{2} ∪ X),

CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{h} σ_{1}(\overline{x})!j_{0} ↦^{x′′} CUT_{(σ_{1}∪(x′→x′′),σ_{2},X,\underline{z},\overline{z})}[p_{j_{0}}|q]

• if p = \underline{x}?j ↦^{x′} p_{j} such that \underline{x} ≠ \underline{z} then, letting x′′ = New(Rσ_{1} ∪ Rσ_{2} ∪ X),

CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{h} σ_{1}(\underline{x})?j ↦^{x′′} CUT_{(σ_{1}∪(x′→x′′),σ_{2},X,\underline{z},\overline{z})}[p_{j}|q]

Remark: Strictly speaking, the first clause of the definition should be splitten into two subcases. Adopting the convention that the left side of CUT is the side of the ∧-occurrence of the cut formula, what is written upon is the case where x′ is the name \underline{x′} of a ∧-formula. In the other case (\overline{x′} is the name of a ∨-formula), it should be:

CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{h} CUT_{(∅,∅,X,\underline{z′},\overline{z′})}[q′|p′]

4.3 The innermost strategy of reduction

The innermost strategy of reduction is described in two steps. The first step applies to a single cut between two cf-proofs. Newly generated cuts are reduced from the inner side to the outer side. The second step applies to any proof and eliminates cuts from the inner side to the outer side. Consistently with the transfinite character of proofs, the procedure is transfinite as well.

Definition 10 The relation ⟹^{u}_{1} is inductively defined by the following rules:

\begin{matrix}CUT [p|q] ⟹^{h} \overline{x}!j_{0} ↦^{x′} r & r ⟹^{u}_{1} r′ \\ CUT [p|q] ⟹^{u}_{1} \overline{x}!j_{0} ↦^{x′} r′ \end{matrix}

\begin{matrix}CUT [p|q] ⟹^{h} \overline{x}?j ↦^{x′} r_{j} & ∀j ∈ J, r_{j} ⟹^{u}_{1} r′_{j} \\ CUT [p|q] ⟹^{u}_{1} \overline{x}?j ↦^{x′} r′_{j} \end{matrix}

\begin{matrix}CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{h} CUT_{(σ′_{1},σ′_{2},X′,\underline{z}′,\overline{z}′)}[p′|q′] & \{ \begin{matrix}p′ ⟹^{u}_{1} p′′ \\ q′ ⟹^{u}_{1} q′′ \end{matrix} & CUT_{(σ′_{1},σ′_{2},X′,\underline{z}′,\overline{z}′)}[p′′|q′′] ⟹^{u}_{1} r \\ CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{u}_{1} r \end{matrix}

Definition 11 Let p be a proof. The relation p ⟹^{u} q is inductively defined by the following rules:

{p ⟹^{u} p′ \atop \overline{x}!i_{0} ↦^{x′} p ⟹^{u} \overline{x}!i_{0} ↦^{x′} p′}

{∀i ∈ I, p_{i} ⟹^{u} p′_{i} \atop \underline{x}?i ↦^{x′} p_{i} ⟹^{u} \underline{x}?i ↦^{x′} p′_{i}}

\begin{aligned}p ⟹^{u} p′ & q ⟹^{u} q′ & CUT [p′|q′] ⟹^{u}_{1} r \\ & CUT [p|q] ⟹^{u} r \end{aligned}

4.4 The termination of the innermost strategy of reduction

The proof that the innermost strategy of reduction effectively eliminates cuts deterministically follows Martin-Löf’s argument in [20]:

Lemma 1 If CUT_{(σ_{1},σ_{2},X,\underline{x},\overline{x})}[p|q] is a proof such that p is a cf-proof of Γ^{X}, Γ_{1}^{X_{1}}, (∧_{i∈I}A_{i})\underline{x}, q a cf-proof of Γ^{X}, Γ_{2}^{X_{2}}, (∨_{i∈I}A_{i}^{⊥})\overline{x}, then there exists a unique proof r such that CUT_{(σ_{1},σ_{2},X,\underline{x},\overline{x})}[p|q] ⟹^{u}_{1} r. Moreover, r is cut-free.

Proof: The unicity follows from the determinism of the rules. The existence is by induction first on ∧_{i∈I}A_{i}, then on the pair of p and q.

In case of main step, three new cuts are generated. The two upper ones verifies that the pair of sizes of the left-hand and right-hand side is lesser. They reduce by ⟹^{u}_{1} to a cf-proof according to the induction hypothesis. The size of the cut formula in the third and lower new generated cut is lesser. By induction hypothesis, it reduced also to a cf-proof.

In case of permutation steps, the pair of sizes of the left-hand and right-hand side of the new cut is lesser than the one of the replaced cut. This is sufficient to apply the induction hypothesis.

Lemma 2 If p is cut-free, then p ⟹^{u} p.

Proof: Immediate.

Proposition 1 For all proof p, there exists a unique q such that p ⟹^{u} q. Moreover q is cut-free. We write q = nf(p).

Proof: The unicity comes from the determinism in the rule defining ⟹^{u} and ⟹^{u}_{1}. The existence of q such that p ⟹^{u} q and the fact that q follows the line of the proof of the Hauptsatz: by induction on p then by lemma 1 for the case of CUT.

5 Strategy of outermost cut-elimination

We call weak a strategy of reduction which reduces a proof until an introduction rule comes out on the top of the proof, but never reduces under an introduction rule.

We define a predicate which expresses the reduction of a proof according to a weak strategy of reduction associated to the previous procedure. A second predicate expresses the reduction of a proof according to an outermost strategy of reduction. This outermost strategy extends the weak strategy by a recursive application of it under introduction rules. This procedure is transfinite, consistently with the transfinite character of proofs.

An extension of the previous argument, reasoning by induction on the potential cut-free form of a proof, allows to show that this reduction leads to a cut-free proof. It is shown also that this cf-proof is effectively the same as the one obtained by the previous procedure.

5.1 An outermost strategy of reduction

We give in this section the operational definition of the outermost strategy. At first, the procedure scans the proof until finding a cut. A pattern analysis is performed. This needs that at least one argument of the cut begins with a ∨-introduction or a ∧-introduction. For such an aim, the procedure is applied recursively to its arguments until finding an introduction rule. At this point, a rewriting rule can be applied, and the procedure is recursively called. In fact, to stay consistent with the preference of the ∧-side in the rewriting rules, the procedure first scans the proof on the ∧-side of the cut, and scans only the second proof when the proof on the ∧-side consists of the introduction of the cut formula. This weak reduction stops to reduce a proof as soon as an introduction rule comes on top. The outermost reduction is defined recursively from the weak reduction.

Definition 12 The weak reduction is a relation between proofs written ⟹^{w} and defined by the following clauses:

\overline{x}!i_{0} ↦^{x′} p ⟹^{w} \overline{x}!i_{0} ↦^{\underline{x}} p

\underline{x}?i ↦^{x′} p_{i} ⟹^{w} \underline{x}?i ↦^{\overline{x}} p_{i}

\begin{matrix}p ⟹^{w} \overline{x}!j_{0} ↦^{x′} p′ & CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[\overline{x}!j_{0} ↦^{x′} p′|q] ⟹^{h} r \\ CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{w} r \end{matrix}

\begin{aligned}p ⟹^{w} \underline{x}?j ↦^{x′} p_{j} & CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[\underline{x}?j ↦^{x′} p_{j}|q] ⟹^{h} r & \underline{x} ≠ \underline{z} \\ & CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{w} r \end{aligned}

\begin{aligned}\{ \begin{matrix}p ⟹^{w} \underline{x}?i ↦^{x′} p_{i} \\ q ⟹^{w} \overline{y}!j_{0} ↦^{y′} q′ \end{matrix} & CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|\overline{y}!j_{0} ↦^{y′} q′] ⟹^{h} r & \{ \begin{matrix}\underline{x} = \underline{z} \\ \overline{y} ≠ \overline{z} \end{matrix} \\ & CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{w} r \end{aligned}

\begin{aligned}\{ \begin{matrix}p ⟹^{w} \underline{x}?i ↦^{x′} p_{i} \\ q ⟹^{w} \underline{y}?j ↦^{y′} q_{j} \end{matrix} & CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|\underline{y}?j ↦^{y′} q_{j}] ⟹^{h} r & \underline{x} = \underline{z} \\ & CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{w} r \end{aligned}

\begin{aligned}\{ & \begin{matrix}p ⟹^{w} \underline{x}?i ↦^{x′} p_{i}  \underline{x} = \underline{z} \\ q ⟹^{w} \overline{y}!i_{0} ↦^{y′} q′  \overline{y} = \overline{z} \\ CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|\overline{y}!i_{0} ↦^{y′} q′] ⟹^{h} r \\ r ⟹^{w} r′ \end{matrix} \\ & CUT_{(σ_{1},σ_{2},X,\underline{z},\overline{z})}[p|q] ⟹^{w} r′ \end{aligned}

Remark: In each case, the shape of the left argument of the ⟹^{h} step determined which one of the five clauses of the definition of ⟹^{h} is intended. It could be replace by the corresponding reduction. If we keep this notation, it is to insist on the fact that the weak reduction is purely built as a composition of one step head reduction.

The outermost reduction recursively applies the weak reduction under introduction rules.

Definition 13 The outermost reduction is a relation between proofs written ⟹^{o} and defined by the following clauses:

\begin{matrix}p ⟹^{w} \underline{x}?i ↦^{x′} p_{i} & ∀i ∈ I, p_{i} ⟹^{o} q_{i} \\ p ⟹^{o} \underline{x}?i ↦^{x′} q_{i} \end{matrix}

\begin{matrix}p ⟹^{w} \underline{x}!i_{0} ↦^{x′} p′ & p′ ⟹^{o} q \\ p ⟹^{o} \underline{x}!i_{0} ↦^{x′} q \end{matrix}

5.2 The termination of the outermost strategy of reduction

We give a proof of termination of the outermost reduction. The proof, due to Coquand, differs from the proof of the Hauptsatz by generalizing the induction to all proofs reducing to the same cut-free proof.

Lemma 3 For all formula ∧_{i∈I}A_{i}, for all cf-proofs p′ of Γ, Γ_{1}, \underline{z} : ∧_{i∈I}A_{i} and q′ of Γ, Γ_{2}, \overline{z} : ∨_{i∈I}A_{i}^{⊥}, for all proofs p and q such that p ⟹^{o} p′ and q ⟹^{o} q′, there exists a cf-proof r such

that CUT_{(σ,\underline{z},\overline{z})}[p|q] ⟹^{o} r.

Proof: (we do not care any longer with the σ’s)

By an induction first on the formula, then on the pair (p′, q′). We consider p such that p ⟹^{o} p′ and q such that q ⟹^{o} q′. The proof depends on the outer rule of p′ and q′.

• We suppose first that p′ = \overline{x}!j_{0} ↦^{x′} p′_{j_{0}}.

Coming back to the definition of ⟹^{o} implies that there exists a proof p_{j_{0}} such that

p ⟹^{w} \overline{x}!j_{0} ↦^{x′} p_{j_{0}} and p_{j_{0}} ⟹^{o} p′_{j_{0}}.

This entails that CUT_{(\underline{z},\overline{z})}[p|q] ⟹^{w} \overline{x}!j_{0} ↦^{x′} CUT_{(\underline{z},\overline{z})}[p_{j_{0}}|q] by the third clause of the

definition of ⟹^{w}, taking into account the effect of ⟹^{h}.

But the pair (p′_{j_{0}}, q′) is less than the pair (p′, q′). We can apply the induction hypothesis which assures the existence of r_{j_{0}} cut-free such that CUT_{(\underline{z},\overline{z})}[p_{j_{0}}|q] ⟹^{o} r_{j_{0}}

Thus the existence of r = \overline{x}!j_{0} ↦^{\underline{x}} r_{j_{0}} cut-free satisfying the lemma.

• The case where p′ is \underline{x}?j ↦^{x′} p′_{j} with \underline{x} ≠ \underline{z} works similarly.

• We suppose now that p′ = \underline{x}?i ↦^{x′} p′_{i} with \underline{x} = \underline{z}.

Coming back to the definition of ⟹^{o} implies that there exists a family of proofs (p_{i})_{i∈I}

such that p ⟹^{w} \underline{x}?i ↦^{x′} p_{i} and for each i ∈ I, p_{i} ⟹^{o} p′_{i}.

The inversion of the definition of ⟹^{o} depends now on the form of q′

– We suppose that q′ = \underline{y}?j ↦^{y′} q′_{j}.

Coming back to the definition of ⟹^{o} implies that there exists a family of proofs q_{j}

such that q ⟹^{w} \underline{y}?j ↦^{y′} q_{j} and for each j ∈ J, q_{j} ⟹^{o} q′_{j}.

This entails that for each j ∈ J, CUT_{(\underline{z},\overline{z})}[p|q] ⟹^{w} \underline{y}?j ↦^{\overline{y}} CUT_{(\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|q_{j}].

But for each j ∈ j, the pair (p′, q′_{j}) is less than the pair (p′, q′). We can apply the induction hypothesis which assures the existence of r_{j} cut-free such that

CUT_{(\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|q_{j}] ⟹^{o} r_{j}.

Thus the existence of r = \underline{y}?j ↦^{y′} r_{j} cut-free satisfying the lemma.

– The case where q′ is \overline{y}!j_{0} ↦^{y′} p′_{j_{0}} with \overline{y} ≠ \overline{z} works similarly.

– We suppose that q′ = \overline{y}!i_{0} ↦^{y′} q′_{i_{0}} with \overline{y} = \overline{z}.

Coming back to the definition of ⟹^{o} implies that there exists a proof q_{i_{0}} such that

q ⟹^{w} \overline{y}!i_{0} ↦^{y′} q_{i_{0}} and q_{i_{0}} ⟹^{o} q′_{i_{0}}.

The induction hypothesis stands for the pair (p′, q′_{i_{0}}), thus there exists r_{1} cut-free

such that CUT_{(\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|q_{i_{0}}] ⟹^{o} r_{1},

Similarly, the induction hypothesis stands for the pair (p′_{i_{0}}, q′), thus there exists r_{2}

cut-free such that CUT_{(\underline{z},\overline{z})}[p_{i_{0}}|\overline{y}!i_{0} ↦^{y′} q_{i_{0}}] ⟹^{o} r_{2},

But reusing the induction hypothesis for the formula A_{i_{0}} and the pair (r_{1}, r_{2}), we obtain the existence of r cut-free such that

CUT_{(\underline{y}′,\overline{x}′)}[CUT_{(\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|q_{i_{0}}]|CUT_{(\underline{z},\overline{z})}[p_{i_{0}}|\overline{y}!i_{0} ↦^{y′} q_{i_{0}}]] ⟹^{o} r

At the end, we obtain CUT_{(\underline{z},\overline{z})}[p|q] ⟹^{o} r by applying the last clause of the definition

of ⟹^{w}.

Proposition 2 For all proof p, there exists a unique q such that p ⟹^{o} q. Moreover q is cut-free. Then we write q = nf_{h}(p)

Proof: The existence is by induction on p, using the lemma 3 to carry the case of CUT. The uniqueness comes from the determinism of the definition of ⟹^{o} and ⟹^{w}.

Remark1: Two alternative proofs seem possible. First by considering a formalisation of the previous proof of cut-elimination in a logical system enjoying termination of the weak reduction. Secondly, by using Gonthier-Lévy-Mellies standardisation theorem [15]. Remark2: It seems that the previous proof can be extended into a proof of strong cutelimination. We do not know what could be the meaning of strong cut-elimination for transfinite proofs such as the one of the calculus we consider. But, if we would have considered a finitary calculus (the predicate calculus for instance, but then by adding non necessary decidable atoms in our formalism) for which strong cut-elimination makes sense, then, by replacing the lemma statement

∀p, q∀p′, q′p ⟹^{o} p′ ∧ q ⟹^{o} q′ ⇒ ∃r, CUT pq ⟹^{o} r

by

∀p, q∀p′, q′pstrongly reduces top′ ∧qstrongly reduces toq′ ⇒ ∃r, CUT pqstrongly reduces tor the strong cut-elimination could have beed deduced.

5.3 Correctness of the outermost cut-elimination w.r.t. the innermost cut-elimination

We prove in this section that the outermost reduction is correct w.r.t. the previous procedure.

Definition 14 We write p ∼ q to say that nf(p) = nf(q).

Lemma 4 We have:

1. p ⟹^{h} q implies p ∼ q

2. p ⟹^{w} q implies p ∼ q

3. p ⟹^{o} q implies p ∼ q

Proof:

1. By coming back to the definition of ⟹^{u}. We show for instance the first case of the definition of ⟹^{h}: Assume that

r = CUT_{(\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|\overline{y}!i_{0} ↦^{y′} q_{i_{0}}]

p = CUT_{(\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p_{i}|q_{i_{0}}]

q = CUT_{(\underline{z},\overline{z})}[p_{i_{0}}|\overline{y}!i_{0} ↦^{y′} q_{i_{0}}]

r′ = CUT_{(\underline{x},\overline{y})}[p|q]

r ⟹^{h} r′

Let R such that r ⟹^{u} R. By unambiguous pattern-matching, there exist cf-proofs (p′_{i})_{i∈I} and q′_{i_{0}} such that

∀i ∈ I, p_{i} ⟹^{u} p′_{i}

q_{i_{0}} ⟹^{u} q′_{i_{0}}

CUT_{(\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p′_{i}|\overline{y}!i_{0} ↦^{y′} q′_{i_{0}}] ⟹^{h} CUT_{(\underline{x},\overline{y})}[p′|q′]

where

\begin{matrix}p′ = CUT_{(\underline{z},\overline{z})}[\underline{x}?i ↦^{x′} p′_{i}|q′_{i_{0}}] \\ q′ = CUT_{(\underline{z},\overline{z})}[p′_{i_{0}}|\overline{y}!i_{0} ↦^{y′} q′_{i_{0}}] \end{matrix}

and there exist P and Q such that

p′ ⟹^{u}_{1} P

q′ ⟹^{u}_{1} Q

CUT_{(\underline{x},\overline{y})}[P |Q] ⟹^{u}_{1} R

But the fact that (p′_{i})_{i∈I} and q′_{i_{0}} are cut-free implies that

\begin{matrix}p ⟹^{u} P \\ q ⟹^{u} Q \end{matrix}

and with the same reasoning that CUT_{(\underline{x},\overline{y})}[p|q] ⟹^{u} R. Hence the result.

2. By direct induction on the proof of p ⟹^{w} q using 1.

3. By direct induction on the proof of p ⟹^{o} q using 2.

Proposition 3 For all p, we have nf_{h}(p) = nf(p).

Proof: nf_{h}(p) is cut-free, hence nf(nf_{h}(p)) = nf_{h}(p), by lemma 2. But p ⟹^{o} nf_{h}(p) implies p ∼ nf_{h}(p). Thus nf_{h}(p) = nf(p).

In fact, there is a generalisation: if a strategy built on ⟹^{h}, when applied to a proof q, ultimately yields a cf-proof q′, then q′ = nf(q)

5.4 Finiteness of weak reduction for atomic sequents

Proposition 4 Let Γ be a sequent consisting only of atomic formulas and F a formula. Let p be a proof of Γ, F^{x}, q a proof of Γ, (F^{⊥})^{x^{⊥}} and r = CUT_{(x,x^{⊥})}[p|q].

Then r reduces to nf(r) by a finite number of application of the one-step head reduction

⟹^{h}.

Proof: Since Γ consists only of atomic formulas, we have r ⟹^{w} nf(r) by proposition 3 and the definition of ⟹^{o}.

But, by induction on the proof of r ⟹^{w} nf(r), there is a finite number of application of ⟹^{h} such that

r ⟹^{h} r_{1} ... r_{n} ⟹^{h} nf(r)

Remark: What is noticeable is that this result is valid not only for effective proofs (the ones for which the function of the ∧-intro rule may be described by a finite number of symbols) but also for abstract proofs where the branches of the ∧-intro rule have a priori no link between them (especially it is possible that there is no uniform bound on the length of branches).

6 Arbitrariness in cut-elimination procedures

We have defined in this paper a deterministic procedure of cut-elimination. The procedure has been defined through a pattern-matching analysis of the different forms taken by a proof with cut as head symbol. The determinism has been expressed by the fact that the pattern-matching was unambiguous. But this determinism relies on arbitrary choices. We list here some of the possible choices that can be done in the definition of a deterministic cut-elimination procedure.

6.1 Main atomic step

Both sides of the cut come from an introduction of the cut formula.

ρ = \begin{matrix}\binom{⋮ . ρ_{i}}{Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i}} & i∈I \\ Λ, Λ_{1}, ∧_{i∈I}A_{i} \end{matrix} ∧-intro  σ = {⋮ . σ_{i_{0}} \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}, A_{i_{0}}^{⊥}} ; Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥} ∨-intro

Three ways to reduce such a pattern are possible.

• cross-cut

\begin{matrix}{⋮ . ρ_{i_{0}} \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i_{0}}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i_{0}} \end{matrix} cut \begin{matrix}{⋮ . ρ \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}} & {⋮ . σ_{i_{0}} \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}, A_{i_{0}}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i_{0}}^{⊥} \end{matrix} cut

Λ, Λ_{1}, Λ_{2} cut

• ∧-first

\begin{matrix}{⋮ . ρ_{i_{0}} \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i_{0}}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i_{0}} \end{matrix} cut (\begin{matrix}{⋮ . ρ_{i} \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i_{0}}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i} \end{matrix} cut)_{i∈I} Λ, Λ_{1}, Λ_{2}, ∧_{i∈I}A_{i} ∧-intro {⋮ . σ_{i_{0}} \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}, A_{i_{0}}^{⊥}} Λ, Λ_{1}, Λ_{2}, A_{i_{0}}^{⊥} cut

Λ, Λ_{1}, Λ_{2} cut

• ∨-first

{⋮ . ρ_{i_{0}} \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i_{0}}} \begin{matrix}{⋮ . ρ \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}} & {⋮ . σ_{i_{0}} \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}, A_{i_{0}}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i_{0}}^{⊥} \end{matrix} cut

Λ, Λ_{1}, Λ_{2}, ∨_{i∈I}A_{i}^{⊥} ∨-intro

Λ, Λ_{1}, Λ_{2}, A_{i_{0}} cut \begin{matrix}{⋮ . ρ \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}} & {⋮ . σ_{i_{0}} \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}, A_{i_{0}}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i_{0}}^{⊥} \end{matrix} cut

Λ, Λ_{1}, Λ_{2} cut

All these three kinds of main atomic step are valid. The first one, usually called cross-cut is the one used by the procedure previously studied. The second one, that we call ∧-first, is the atomic step used in the cut-elimination procedure of LC [12]. The proof of correctness for a procedure using this main step is a bit different. The induction on the pair of the proofs on the ∧ and ∨ sides of the cut has to be replaced by an induction carried first on the proof on the ∧-side, then on the proof on the ∨-side. We call ∧-first this atomic step because it can be splitten into two steps. In a first time, the ∧-side duplicates the ∨-side:

(\begin{matrix}{⋮ . ρ_{i} \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i} \end{matrix} cut)_{i∈I}

Λ, Λ_{1}, Λ_{2}, ∧_{i∈I}A_{i} ∧-intro

{⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}}

Λ, Λ_{1}, Λ_{2} cut

In a second time, it is the turn of the outer copy of the ∨-side to duplicates the other side:

(\begin{matrix}{⋮ . ρ_{i} \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i} \end{matrix} cut)_{i∈I}

Λ, Λ_{1}, Λ_{2}, ∧_{i∈I}A_{i} ∧-intro

(\begin{matrix}{⋮ . ρ_{i} \atop Λ, Λ_{1}, ∧_{i∈I}A_{i}, A_{i}} & {⋮ . σ \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}} \\ Λ, Λ_{1}, Λ_{2}, A_{i} \end{matrix} cut)_{i∈I}

Λ, Λ_{1}, Λ_{2}, ∧_{i∈I}A_{i} ∧-intro

{⋮ . σ_{i_{0}} \atop Λ, Λ_{2}, ∨_{i∈I}A_{i}^{⊥}, A_{i_{0}}^{⊥}}

Λ, Λ_{1}, Λ_{2}, A_{i_{0}}^{⊥} cut

Λ, Λ_{1}, Λ_{2}, ∨_{i∈I}A_{i}^{⊥} ∨-intro

Λ, Λ_{1}, Λ_{2} cut

It remains then to decrease the complexity of the cut formula in the outermost cut. We gather all these elementary steps into one because this simplifies the proof of termination and insists on the difference between ∧-first and cross-cut.

The ∨-first main atomic step is obtained from the ∧-first by exchanging the role of ∧ and ∨. In this case, the proof of correctness of the procedure is a bit different again. The induction has to be carried first on the proof on the ∨-side then on the proof on the ∧-side.

The ∧-first atomic step seems to have a special place among the different possible ways of performing the main atomic step. Besides being compatible with a denotational semantics of classical proofs (it is the case in the LC calculus), it corresponds also to the natural way of expressing Coquand’s interaction. More precisely, Coquand’s interaction in [4] can be shown to be the trace of the execution following a weak strategy of reduction of the procedure studied in the paper, but with the ∧-first atomic step instead of cross-cut.

Let us remark that all three become only one when there is no contraction of the ∧-formula (i.e. when the remaining occurrence of the ∧-formula is not further introduced in the remaining part of ρ_{i_{0}}). Similarly when there is no contraction of the ∨-formula. But ∧-contractions can be eliminated in a proof while ∨-contractions cannot. This is a mark of the deep difference between ∨ and ∧.

Cross-cut, ∧-first and ∨-first are the more canonical main atomic steps. But more complicated variants of them can be conceived. It is also possible to conceived a procedure which sometimes uses one of these main atomic steps, sometimes another of those. This is the case for instance of the first Gentzen’s proof for cut-elimination in [6] where an argument of laterality is used (the proof on the left side duplicates the other first).

Cross-cut is used in Gentzen’s second published proof for arithmetic consistency [9], in Martin-Löf’s proof in [20], in Girard’s proofs in [11, 14].

6.2 The ambiguous permutation atomic step

It is the case where both sides of the cut comes from an introduction of a formula of the context.

ρ = {⋮ . ρ′ \atop Ω′_{1}, ∧_{i∈I}A_{i}} ; Ω_{1}, ∧_{i∈I}A_{i} intro in Ω_{1}  σ = {⋮ . σ′ \atop Ω′_{2}, ∨_{i∈I}A_{i}^{⊥}} ; Ω_{2}, ∨_{i∈I}A_{i}^{⊥} intro in Ω_{2}

where Ω_{1} = Λ, Λ_{1} and Ω_{2} = Λ, Λ_{2}.

Besides the choice that have been made in the procedure we have studied, there is a second possibility obtained by exchanging the role of ∧ and ∨. The proof of termination keeps being valid when changing from one to the other of these possible atomic steps.

Typically, the ambiguousness of this atomic step is related to the Lafont’s example [14] concerning the cut of a formula which is weakened on both sides of the cut (translated in our calculus, this means that ∧_{i∈I}A_{i} and ∨_{i∈I}A_{i}^{⊥} are no further concerned with an introduction rule in the rest of the proofs ρ and σ).

Let’s remark that both the cut-elimination procedure for LC and Coquand’s interaction (translated into a cut-elimination procedure in the usual sense) choose to make the rule on the ∧-side crossing first the cut. This is consistent with the ∧-first main atomic step.

6.3 Permutation of the order of cuts

The proof we have described belongs to a kind of cut-elimination procedure which never permutes the order of cuts. But some proofs do, such as Girard’s ones in [11, 14] or Tait’s one for infinitary propositional logic in [27]. Girard’s proof works with formula of bounded depth. The procedure first consider cuts concerning formulas of higher depth in the proof. By a sequence of permutations, they are progressively moved until the axiom and ultimately disappear. This decreases by one the higher depth of cut formula in the proof. Repeating recursively this process leads to a cut-free proof. For such a procedure, it is easy to bound the length of the resulting cut-free proof: this length is an hyperexponential function of the original length. In contrast with this, the bound provided by the procedure we have described is, at first glance, an Ackerman function of the original length.

6.4 On the duplication of ∧-formulas

Consider the following cut between proofs without ∧-contraction:

((\begin{matrix}\binom{⋮ . ρ}{Γ, A_{i}, B_{jk}} & k∈K \\ Γ, A_{i}, ∧_{k∈K}B_{jk} \end{matrix} ∧-intro)_{i∈I} Γ, ∧_{i∈I}A_{i}, ∧_{k∈K}B_{jk} ∧-intro)_{j∈J}

Γ, ∧_{i∈I}A_{i}, ∧_{j∈J} ∧_{k∈K} B_{jk} ∧-intro

{⋮ . σ \atop Γ, ∨_{k∈K}B_{j_{0}k}^{⊥}, B_{j_{1}k_{10}}^{⊥}} ; Γ, ∨_{k∈K}B_{j_{0}k}^{⊥}, ∨_{k∈K}B_{j_{1}k}^{⊥} ∨-intro

Γ, ∨_{j∈J} ∨_{k∈K} B_{jk}^{⊥}, ∨_{k∈K}B_{j_{0}k}^{⊥} ∨-intro

Γ, ∨_{j∈J} ∨_{k∈K} B_{jk}^{⊥} ∨-intro

Γ, ∧_{i∈I}A_{i} cut

The beginning of its reduced form looks like this:

(\begin{matrix}\binom{⋮ .}{Γ, A_{i}, A_{i′}} & i′∈I \\ Γ, ∧_{i∈I}A_{i}, A_{i} \end{matrix} ∧-intro)_{i∈I}

Γ, ∧_{i∈I}A_{i} ∧-intro

A ∧-contraction has appeared. Remarks:

For information, we give Gentzen’s definition [7] of the statability of a reduction rule. This was originally stated for an intuitionistic sequent calculus together with elimination of the double negation.

Definition 15 The statability of a reduction rule or provability for a sequent is inductively defined as follows:

• if for some i_{0} ∈ I, the sequent Δ, ∨_{i∈I}A_{i}, A_{i_{0}} is provable then the sequent Δ, ∨_{i∈I}A_{i} is provable

• if for all i′ ∈ I, the sequent Δ, A_{i′} is provable then the sequent Δ, ∧_{i∈I}A_{i} is provable

For information again, we give Novikoff’s definition [22] of regularity. An analysis of [22] can be found in Coquand [5].

Definition 16 The regularity or provability of a sequent is inductively defined as follows:

• if for some i_{0} ∈ I, the sequent Δ, ∨_{i∈I,i≠i_{0}}A_{i}, A_{i_{0}} is provable then the sequent Δ, ∨_{i∈I} is provable

• if for all i ∈ I, the sequent Δ, A_{i} is provable then the sequent Δ, ∧_{i∈I}A_{i} is provable

Conclusion

We have studied the cut-elimination according to a weak strategy of reduction. The origin of this study is a re-injection into the framework of the classical sequent calculus of the game-theoretic approach of cut-elimination as Coquand’s interaction sequences. We conjecture that interaction corresponds to the trace of cut-elimination according to a strategy of weak reduction. Up to this, what we have shown in this paper would provide for an alternative, short and constructive proof of termination for interaction. This is in contrast with the classical (but working with non well-founded formulas) proof in [4] and with the constructive proof in [5] which needs that the formulas are depth-bounded.

Thanks The proof of termination of the outermost strategy of cut-elimination is due to Thierry Coquand. We are indebted to Christine Paulin for several remarks and improvements in the presentation. Also to Luc Bouge for his encouragements. Chet Murthy helped us with the English.

Appendix : the underlying procedure of the cut-elimination proof

We give here the underlying procedure, i.e. the computational part of the cut-elimination proof. Proofs are defined as proofs in term notation and the program is written in ML’s style.

The routine to manage with renaming maps:

type name == int;;
type finmap == (name * name) list;; (* finite map *)
type renaming == finmap * finmap * (name list);;
let add1 (sigma1,sigma2,X) (n',n) =
  ((n',n)::sigma1,sigma2,X);;

let add2 (sigma_1,sigma2,X) (n',n) =
  (sigma_1,(n',n)::sigma2,X);;
let assoc1 n (sigma1,sigma2,X) = assoc n sigma1;;
let assoc2 n (sigma1,sigma2,X) = assoc n sigma2;;
let range (sigma1,sigma2,X) =
   union X (union (map snd sigma1) (map snd sigma2));;
let lower_sigma sigma = ([],[],range sigma);;
let rec max_list l =
   match l with
   [a] -> a
 | a::l -> max a (max_list l)
 | [] -> failwith "empty list";;
let newn sigma = (max_list (range sigma)) + 1;;

The cut-elimination procedure is decomposed into two phases: the elimination of a cut between cut-free proofs, then the complete elimination procedure. To simplify, and because ML can not handle with explicit polymorphism, we admit that all the indices range the same domain I, here the integers.

type I == int;;
type proof =
   E_intro of name * name * I * proof
 | A_intro of name * name * (I -> proof)
 | Cut of name * proof * name * proof * renaming;;
let rec adm np p nq q sigma =
   match p with
   E_intro(np',np'',i,p')
     -> let n = newn sigma in
        let p'' = adm np p' nq q (add1 sigma (np'',n)) in
        E_intro(assoc1 np' sigma,n,i,p'')
 | A_intro(np',np'',pi)
     -> if np'<>np then
           let n = newn sigma in
           let pi' = fun i -> adm np (pi i) nq q (add1 sigma (np'',n)) in
           A_intro(assoc1 np' sigma,n,pi')
        else (match q with
             A_intro(nq',nq'',qi)
               -> let n = newn sigma in
                  let qi' =
                     fun i -> adm np p nq (qi i) (add2 sigma (nq'',n)) in
                  A_intro(assoc2 nq' sigma,n,qi')
           | E_intro(nq',nq'',i,q')
             -> if nq'<>nq then
                   let n = newn sigma in

                  let q'' = adm np p nq q' (add2 sigma (nq'',n)) in
                  E_intro(assoc2 nq' sigma,n,i,q'')
               else
                  let n = newn sigma in
                  let p0 = adm np (pi i) nq q (add1 sigma (np'',n)) in
                  let q0 = adm np p nq q' (add2 sigma (nq'',n)) in
                  adm n p0 n q0 (lower_sigma sigma)
          | _-> failwith "not a cut-free proof")
| _-> failwith "not a cut-free proof";;
let rec elim p =
  match p with
  A_intro(np',np'',pi)   -> A_intro(np',np'',fun i -> elim (pi i))
| E_intro(np',np'',i,p') -> E_intro(np',np'',i,elim p')
| Cut(np,p,nq,q,sigma)   -> adm np (elim p) nq (elim q) sigma;;

References

[1] P. Bernays, On the original Gentzen consistency proof for number theory, in Intuitionism and Proof Theory, Kino, Myhill, Vesley eds, 1968, pp 409-417.

[2] T. Coquand, Une théorie des constructions Thèse de doctorat, université Paris 7, 1985.

[3] T. Coquand, A semantics of evidence for classical arithmetic, Proceedings of BRA Logical Frameworks 1991.

[4] T. Coquand, Interaction sequences, private paper, 1992.

[5] T. Coquand, A semantics of evidence for classical arithmetic, revised version, to appear in Journal of Symbolig Logic.

[6] G. Gentzen, Investigations into logical deduction, for instance in [26], pp 68ff.

[7] G. Gentzen, The consistency of elementary number theory, for instance in [26], pp 132ff.

[8] G. Gentzen, Galley proof of “the consistency of elementary number theory”, in [26], pp 201ff. Also reported in [1].

[9] G. Gentzen, New version of the consistency proof for elementary number theory, for instance in [26], pp 252ff.

[10] G. Gentzen, New version of the consistency proof for elementary number theory, in [26], page 259.

[11] J-Y. Girard, Proof theory and logical complexity, Bibliopolis, Napoli, 1987, to be published also by North Holland.

[12] J-Y. Girard, A new constructive logic: classical logic, rapport de recherche INRIA, number 1443, 1991.

[13] J-Y. Girard, On the unity of logic, rapport de recherche INRIA, number 1467, 1991.

[14] J-Y. Girard, Y. Lafont, P. Taylor, Proofs and types, Cambridge University Press, 1989.

[15] G. Gonthier, J-J. Levy, P-A. Mellies A standardisation theorem, Proceedings of LICS, 199?.

[16] T. Griffin, A Formulae-as-Types Notion of Control, proceedings of POPL, 1990.

[17] M. Felleisen, Reasoning About Continuations, proceedings of LICS, 1986.

[18] K. Lorenzen, Algebraische und logistische Untersuchung über freie Verbände, The Journal of Symbolic Logic, V 16, N 2, 1951, pp 81-106, review (in english) in V 16, N 4, 1951, pp 269-272.

[19] K. Lorenzen, Ein dialogisches Konskruktivitätskriterium, in Infinistic Methods, Proceed. Symp. Found. of Math., PWN, Warszawa, 1958, pp. 193-200.

[20] P. Martin-Löf, Notes on Constructive Mathematics, §30, Almqvist & Wiksell ed, Stockholm, 1968.

[21] C. Murthy, Extracting constructive content from classical proofs Ph. D., Cornell University, 1990.

[22] P.S. Novikoff, On the consistency of certain logical calculus in Matematiceskij sbornik (Recueil Mathématique), T 12 (54), N 2, 1941, pp 230-260.

[23] M. Parigot, Free Deduction: an analysis of “computation” in classical logic, Proceedings of RCLP’91, St Petersburg, Springer Lecture Notes in Computer Sciences 592, pp 361-380.

[24] M. Parigot, λ-μ-calculus: an Algorithmic Interpretation of Classical Natural Deduction, Springer Lecture Notes in Computer Sciences 624, pp 190-201.

[25] K. Schütte, Proof Theory, Springer, 1977.

[26] M. E. Szabo, Gentzen collected work, North Holland, 1969.

[27] W. W. Tait, Normal Derivability in Classical Logic, Springer Lecture Notes in Mathematics 72, J. Barwise ed, pp. 204-236.