Stefan Hetzl
email: hetzl@logic.at

Lutz Straßburger

Herbrand-Confluence for Cut Elimination in Classical First Order Logic

Keywords: F.4.2. Grammars and Other Rewriting Systems, F.1.1. Models of Computation Keywords and phrases proof theory, first-order logic, tree languages, term rewriting, semantics of proofs

We consider cut-elimination in the sequent calculus for classical first-order logic. It is well known that this system, in its most general form, is neither confluent nor strongly normalizing. In this work we take a coarser (and mathematically more realistic) look at cut-free proofs. We analyze which witnesses they choose for which quantifiers, or in other words: we only consider the Herbrand-disjunction of a cut-free proof. Our main theorem is a confluence result for a natural class of proofs: all (possibly infinitely many) normal forms of the non-erasing reduction lead to the same Herbrand-disjunction.

Introduction

The constructive content of proofs has always been a central topic of proof theory and it is also one of the most important influences that logic has on computer science. Classical logic is widely used and presents interesting challenges when it comes to understanding the constructive content of its proofs. These challenges have therefore attracted considerable attention, see, for example, [START_REF] Parigot | λµ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction[END_REF][START_REF] Vincent Danos | A New Deconstructive Logic: Linear Logic[END_REF][START_REF] Curien | The Duality of Computation[END_REF], [START_REF] Barbanera | A Symmetric Lambda Calculus for Classical Program Extraction[END_REF], [START_REF] Urban | Classical Logic and Computation[END_REF][START_REF] Urban | Strong Normalization of Cut-Elimination in Classical Logic[END_REF], [8], [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and their Use in Mathematics[END_REF], or [START_REF] Baaz | Cut-elimination and Redundancy-elimination by Resolution[END_REF], for different investigations in this direction. A well-known, but not yet well-understood, phenomenon is that a single classical proof usually allows several different constructive readings. From the point of view of applications this means that we have a choice among different programs that can be extracted. In [START_REF] Ratiu | Exploring the Computational Content of the Infinite Pigeonhole Principle[END_REF] the authors show that two different extraction methods applied to the same proof produce two programs, one of polynomial and one of exponential average-case complexity. This phenomenon is further exemplified by case studies in [START_REF] Urban | Classical Logic and Computation[END_REF][START_REF] Baaz | Cut-Elimination: Experiments with CERES[END_REF][START_REF] Baaz | CERES: An Analysis of Fürstenberg's Proof of the Infinity of Primes[END_REF] as well as the asymptotic results [START_REF] Baaz | On the non-confluence of cut-elimination[END_REF][START_REF] Hetzl | The Computational Content of Arithmetical Proofs[END_REF]. The reason for this behavior is that classical "proofs often leave algorithmic detail underspecified" [START_REF] Avigad | The computational content of classical arithmetic[END_REF].

On the level of cut-elimination in the sequent calculus this phenomenon is reflected by the fact that the standard proof reduction without imposing any strategy is not confluent. In this paper we consider cut-elimination in classical first-order logic and treat the question which cut-free proofs one can obtain (by the strategy-free rewriting system) from a single proof with cuts. As our aim is to compare cut-free proofs we need a notion of equivalence of proofs: clearly the syntactic equality makes more differences than those which are mathematically interesting. Being in a system with quantifiers, a natural and more realistic choice is to consider two cut-free proofs equivalent if they choose the same terms for the same quantifiers, in other words: if they have the same Herbrand-disjunction.

A cut-reduction relation will then be called Herbrand-confluent if all its normal forms have the same Herbrand-disjunction. The main result of this paper is that, for a natural class of proofs, the standard reduction without erasing of subproofs is Herbrand-confluent. This result is surprising as this reduction is neither confluent nor strongly normalizing and may produce normal forms of arbitrary size (which-as our result shows-arise only from repetitions of the same instances).

As a central proof technique we use rigid tree languages which have been introduced in [START_REF] Jacquemard | Rigid tree automata[END_REF] with applications in verification (e.g. of cryptographic protocols as in [START_REF] Jacquemard | Rigid tree automata and applications[END_REF]) as their primary purpose. To a proof we will associate a rigid tree grammar whose language is invariant under non-erasing cut-elimination and hence equal to the only obtainable Herbranddisjunction. This property suggests the new notion of Herbrand-content of a proof, which is defined as the language of the grammar of the proof, and which is a strong invariant. A side effect of this proof technique is a combinatorial description of how the structure of a cut-free proof is related to that of a proof with cut. Such descriptions are important theoretical results which underlie applications such as algorithmic cut-introduction as in [START_REF] Hetzl | Towards Algorithmic Cut-Introduction[END_REF].

In Section 2 we briefly review the sequent calculus and cut-elimination for classical firstorder logic. In Section 3 we describe regular and rigid tree grammars which we relate to proofs in Section 4. Section 5 is devoted to proving the invariance of the Herbrand-content under duplication of subproofs, and finally, in Section 6, we collect all results together.

Sequent Calculus and Cut-Elimination

For the sake of simplicity, we consider only a one-sided sequent calculus and formulas in negation normal form, but the results can be proved for a two-sided sequent calculus in the same way.

Definition 1.

A proof is a tree of multisets of formulas. Axioms are of the form A, A for A atomic (where A denotes the De Morgan-dual of A). The inference rules are:

Γ, A[x\α] -----------∀ Γ, ∀x A Γ, A[x\t] ----------∃ Γ, ∃x A Γ, A, A --------c Γ, A Γ -----w Γ, A Γ, A ∆, B -----------------∧ Γ, ∆, A ∧ B Γ, A, B ----------∨ Γ, A ∨ B Γ, A A, ∆ ---------------cut Γ, ∆
where α is called eigenvariable and does not appear in Γ, ∀x A and t does not contain a bound variable. We use the notation [x\α] for the substitution that replaces x by the eigenvariable α. Similarly, [x\t] is the substitution that replaces x with t.

The explicitly mentioned formula in a conclusion of an inference rule, like A ∨ B for ∨ is called main formula. Analogously, the explicitly mentioned formulas in the premises of an inference rule, like A and B for ∨, are called auxiliary formulas. In the context of a concrete derivation we speak about main and auxiliary occurrences of inferences.

Definition 2. A proof is called regular if different ∀-inferences have different eigenvariables.
We use the following convention: We use lowercase Greek letters α, β, γ, δ, . . . for eigenvariables in proofs, and π, ψ, . . . for proofs. For a proof π we write EV(π) for the set of

C S L ' 1 2

Axiom reduction:

ψ Γ, A A, A ----------------cut Γ, A ; ψ Γ, A Quantifier reduction: ψ1 ∆, A[x\t] -----------∃ ∆, ∃x A ψ2 A[x\α], Γ -----------∀ ∀x A, Γ -------------------------cut Γ, ∆ ; ψ1 ∆, A[x\t] ψ2[α\t] A[x\t], Γ ----------------------------cut Γ, ∆ Propositional reduction: ψ1 Γ, A ψ2 ∆, B -------------------∧ Γ, ∆, A ∧ B ψ3 A, B, Π ----------∨ A ∨ B, Π --------------------------------cut Γ, ∆, Π ; ψ2 ∆, B ψ1 Γ, A ψ3 A, B, Π --------------------cut B, Γ, Π ----------------------------cut Γ, ∆, Π Contraction reduction: ψ1 Γ, A, A --------c Γ, A ψ2 A, ∆ -------------------cut Γ, ∆ ; ψ1 Γ, A, A ψ2ρ A, ∆ --------------------cut Γ, ∆, A ψ2ρ A, ∆ ------------------------------cut Γ, ∆, ∆ = = = = = = = = = c * Γ, ∆
Weakening reduction:

ψ1 Γ ----w Γ, A ψ2 A, ∆ -------------------cut Γ, ∆ ; ψ1 Γ = = = = = w * Γ, ∆ Unary inference permutation: ψ1 Γ , A -----r Γ, A ψ2 A, ∆ -------------------cut Γ, ∆ ; ψ1 Γ , A ψ2 A, ∆ -------------------cut Γ , ∆ ------r Γ, ∆
Binary inference permutation:

ψ1 Γ ψ2 Γ , A ------------------r Γ, A ψ3 A, ∆ -------------------------cut Γ, ∆ ; ψ1 Γ ψ2 Γ , A ψ3 A, ∆ -------------------cut Γ , ∆ -------------------------r Γ, ∆ Figure 1 Cut-reduction steps.
eigenvariables of ∀-inferences of π. Furthermore, we write |π| for the number of inferences in π. Our results do not depend on technical differences in the definition of the calculus (which in classical logic are inessential) such as the choice between multiplicative and additive rules and the differences in the cut-reduction induced by these choices. However, for the sake of precision, let us formally define the cut-reduction we use in this paper.

Definition 3. Cut-reduction is defined on regular proofs and consists of the proof rewrite steps shown in Figure 1 (as well as all their symmetric variants), where in the contraction reduction step ρ = [α\α ] α∈EV(ψ2) and ρ = [α\α ] α∈EV(ψ2) are substitutions replacing each eigenvariable occurrence α in ψ 2 by fresh copies, i.e., α and α are fresh for the whole proof. We write for the compatible (w.r.t. the inference rules), reflexive and transitive closure of ;.

The above system for cut-reduction consists of purely local, minimal steps and therefore allows the simulation of many other reduction relations. We chose to work in this system in order to obtain invariance results of maximal strength. Among the systems that can be simulated literally are for example all color annotations of [START_REF] Vincent Danos | A New Deconstructive Logic: Linear Logic[END_REF] in the multiplicative version of LK defined there. The real strength of the results in this paper lies however in the general applicability of the used proof techniques: the extraction of a grammar from a proof (that is described in the next sections) is possible in all versions of sequent calculus for classical logic and in principle also in other systems like natural deduction.

Regular and Rigid Tree Grammars

Formal language theory constitutes one of the main areas of theoretical computer science. Traditionally, a formal language is defined to be a set of strings but this notion can be generalized in a straightforward way to considering a language to be a set of first-order terms. Such tree languages possess a rich theory and many applications, see e.g. [START_REF] Gécseg | Tree Languages[END_REF], [START_REF] Comon | Tree Automata: Techniques and Applications[END_REF].

In this section we introduce notions and results from the theory of tree languages that we will use for our proof-theoretic purposes.

A ranked alphabet Σ is a finite set of symbols which have an associated arity (their rank). We write T Σ to denote the set of all finite trees (or terms) over Σ, and we write T Σ (X) to denote the set of all trees over Σ and a set X of variables (seen as symbols of arity 0). We also use the notion of position in a tree, which is a list of natural numbers. We write ε for the empty list (the root position), and we write p.q for the concatenation of lists p and q. we write p ≤ q if p is a prefix of q and p < q if p is a proper prefix of q. Clearly, ≤ is a partial order and < is its strict part. We write Pos(t) to denote the set of all position in a term t ∈ T Σ (X). Definition 4. A regular tree grammar is a tuple G = N, Σ, θ, P , where N is a finite set of non-terminal symbols, and Σ is a ranked alphabet, such that N ∩ Σ = ∅, θ is the start symbol with θ ∈ N , and P is a finite set of production rules of the form β → t with β ∈ N and t ∈ T Σ (N ).

The derivation relation → G of a regular tree grammar G = N, Σ, θ, P is defined as follows. We have s → G r if there is a production rule β → t in P and a position p ∈ Pos(s), such that s| p = β and r is obtained from s by replacing β at p by t. The language of G is then defined as

L(G) = {t ∈ T Σ | θ → * G t}, where → * G is the transitive, reflexive closure of → G . A derivation D of a term t ∈ L(G) is a sequence t 0 → G t 1 → G . . . → G t n with t 0 = θ and t n = t. Note that a term t might have different derivations in G.
In [START_REF] Jacquemard | Rigid tree automata[END_REF] the class of rigid tree languages has been introduced with applications in verification (e.g. of cryptographic protocols as in [START_REF] Jacquemard | Rigid tree automata and applications[END_REF]) as primary motivation. It will turn out that this class is appropriate for describing cut-elimination in classical first-order logic. In contrast to [START_REF] Jacquemard | Rigid tree automata[END_REF] we do not use automata but grammars-their equivalence is shown in [START_REF] Hetzl | Applying Tree Languages in Proof Theory[END_REF].

Definition 5.

A rigid tree grammar is a tuple N, N R , Σ, θ, P , where N, Σ, θ, P , is a C S L ' 1 2 regular tree grammar and N R ⊆ N is the set of rigid non-terminals. We speak of a totally rigid tree grammar if N R = N . In this case we will just write N R , Σ, θ, P .

A derivation θ = t 0 → G t 1 → G . . . → G t n = t of a rigid tree grammar G = N, N R , Σ,
θ, P is a derivation in the underlying regular tree grammar satisfying the additional rigidity condition: If there are i, j < n, a non-terminal β ∈ N R , and positions p and q such that t i | p = β and t j | q = β then t| p = t| q . The language L(G) of the rigid tree grammar G is the set of all terms t ∈ T Σ which can be derived under the rigidity condition. For a given derivation D :

θ = t 0 → G t 1 → G . . . → G t n = t and a non-terminal β we say that p ∈ Pos(t) is a β-position in D if there is an i ≤ n with t i | p = β, i.e.
, either a production rule β → s has been applied at p in D, or β occurs at position p in t. In the context of a given grammar G, we sometimes write D : α → * G t to specify that D is a derivation starting with α and ending with the term t. Lemma 6. Let G = N, N R , Σ, θ, P be a rigid tree grammar and let t ∈ L(G). Then there is a derivation θ → G . . . → G t which uses at most one β-production for each β ∈ N R .

Proof. Given any derivation of t, suppose both β → s 1 and β → s 2 are used at positions p 1 and p 2 respectively. Then by the rigidity condition t| p1 = t| p2 and we can replace the derivation at p 2 by that at p 1 (or the other way round). This transformation does not violate the rigidity condition because it only copies existing parts of the derivation.

Lemma 7.

Let G = N R , Σ, θ, P be a totally rigid tree grammar and θ = β ∈ N R , such that there is exactly one

t with β → t in P . If G = N R \ {β}, Σ, θ, (P \ {β → t})[β\t] then L(G) = L(G ).
Proof. If a G-derivation of a term s uses β, it must replace β by t hence s is derivable using the productions of G as well. The rigidity condition is preserved as the equality constraints of the G -derivation are a subset of those of the G-derivation. Conversely, given a G -derivation of a term s we obtain a derivation of s from the productions of G by replacing applications of δ → r[β\t] by δ → r followed by a copy of β → t for each occurrence of β in r. Let γ 1 , . . . , γ n be the non-terminals that appear in t. By the rigidity condition for i ∈ {1, . . . , n} there is a unique term at all γ i -positions in the derivation. Hence β fulfills the rigidity condition as well, and we have obtained a G-derivation of s.

Lemma 8. If a rigid tree grammar G is obtained from another rigid tree grammar G by deletion of production rules, then L(G ) ⊆ L(G).

Proof. Every G -derivation is a G-derivation. Notation 9. For a given non-terminal β and a term t, we will write β ∈ t or t β for denoting that β occurs in t.

Definition 10.

Let G be a tree grammar. A path of G is a list P of productions α 1 → t 1 , . . . , α n → t n with n ≥ 1 and α i+1 ∈ t i for all i ∈ {1, . . . , n -1}. The length of a path is |P| = n. We will also write P :

α 1 → t 1 α 2 → . . . α n → t n to denote a path.
For a given path P : α 1 → t 1 α 2 → . . . α n → t n we say that α 1 , . . . , α n are on the path P and write α i ∈ P for that. We also write P : α 1 t n and P : α 1 α n , if we do not want to explicitly mention the intermediate steps. For a fixed grammar G, we write α β to denote that there is a path P in G with P : α β. For a set P of production rules, we write α ≺ P β (or simply α ≺ β, when P is clear from context) if there is a production α → t in P with β ∈ t. We write ≺ + for the transitive closure of ≺, and ≺ * for its reflexive, transitive closure. Note that α β implies α ≺ + β, but not the other way around, since β could be a non-terminal with no production β → s in P . Definition 11. A tree grammar N, Σ, θ, P is called cyclic if α ≺ + P α for some α ∈ N , and acyclic otherwise.

Lemma 12. If G is totally rigid and acyclic, then up to renaming of the non-terminals

G = {α 1 , . . . , α n }, Σ, α 1 , P with L(G) = {α 1 [α 1 \t 1 ] • • • [α n \t n ] | α i → t i ∈ P }.
Proof. Acyclicity permits a renaming of non-terminals, such that

α i ≺ + P α j implies i < j. Then L(G) ⊇ {α 1 [α 1 \t 1 ] • • • [α n \t n ] | α i → t i ∈ P } is obvious. For the left-to-right inclusion, let D : α 0 = s 0 → G . . . → G s n = s ∈ T Σ be a derivation in G.
By Lemma 6 we can assume that for each j at most one production whose left-hand side is α j is applied, say α j → t j . By acyclicity we can rearrange the derivation so that α j → t j is only applied after α i → t i for all i < j. For those α j which do not appear in the derivation we can insert any substitution without changing the final term so we obtain

s = α 0 [α 0 \t 0 ] • • • [α n \t n ]. This lemma entails that |L(G)| ≤ n i=1 |{t | α i → t ∈ P }|,
in particular we are dealing with a finite language. The central questions in this context are (in contrast to the standard setting in formal language theory) not concerned with representability but with the size of a representation.

Proofs as Grammars

We will now restrict our attention to a certain class of proofs, called simple proofs below.

Definition 13.

A proof π is called simple if it is regular, the end-sequent is of the form ∃x 1 • • • ∃x n A with A quantifier-free, and every cut in π whose cut-formula contains a quantifier is of the following form, where B is quantifier-free:

Γ, ∃x B B[x\α], ∆ ∀x B, ∆ ∀ Γ, ∆ cut (1)
The above definition requires regularity which is a necessary assumption in the context of cut-elimination. The restriction of the end-sequent is done for expository purposes only, and can be extended to arbitrary sequents. The requirement of the ∀-rule being applied directly above the cut is natural as the rule is invertible. Moreover, any proof which does not fulfill this requirement can be pruned to obtain one that does, by simply permuting ∀-inferences down and identifying their eigenvariables when needed. The only significant restriction is that of disallowing quantifier alternations in the cut formulas. We conjecture that the central results extend to the general case. However, this will require the development of an adequate class of grammars. Observation 14. Simple proofs have the technically convenient property of exhibiting a 1-1 relationship between eigenvariables and cuts. For an eigenvariable α we will therefore write ∀ α for the inference introducing α and cut α for the corresponding cut.

C S L ' 1 2

Definition 15. Let π be a proof of ∃x 1 • • • ∃x n A and let ψ be a subproof of π. The Herbrand-set H(ψ, π) of ψ with respect to π is defined as follows. If ψ is an axiom, then

H(ψ, π) = ∅. If ψ is of the form ψ Γ, A[xn\t] ------------∃ Γ, ∃xn A then H(ψ, π) = H(ψ , π) ∪ {A[x\t]}.
If ψ ends with any other unary inference and ψ is its immediate subproof then H(ψ, π) = H(ψ , π). If ψ ends with a binary rule and ψ and ψ are its immediate subproofs, then H(ψ, π) = H(ψ , π) ∪ H(ψ , π). We write H(π) for H(π, π). Definition 16. Let Q be an occurrence of a formula ∃x A in a proof. We define the set tm(Q) of terms associated with Q as follows: if Q is introduced as the main formula of a weakening, then tm(Q) = ∅. If Q is introduced by a quantifier rule

Γ, A[x\t] ----------∃ Γ, ∃x A then tm(Q) = {t}.
If Q is the main formula in the conclusion of a contraction, and Q 1 and Q 2 are the two occurrences of the same formula in the premise that are contracted, then tm(Q) = tm(Q 1 ) ∪ tm(Q 2 ). In all other cases, an inference with the occurrence Q in the conclusion has a corresponding occurrence Q of the same formula in one of its premises, and we let tm(Q) = tm(Q ).

Definition 17.

Let π be a simple proof, let α ∈ EV(π), and let Q be the occurrence of the existentially quantified cut-formula in the premise of cut α . Then we write B(α) for the set { [α\t] | t ∈ tm(Q) } of substitutions and we define B(π) = α∈EV(π) B(α).

Structures similar to the above B(π) have been investigated also in [START_REF] Heijltjes | Classical proof forestry[END_REF] and [START_REF] Mckinley | Herbrand expansion proofs and proof identity[END_REF] where they form the basis of proof net like formalisms using local reductions for quantifiers in classical first-order logic. Our aim in this work is however quite different: we use these structures for a global analysis of the sequent calculus.

Definition 18.

The grammar of a simple proof π is defined to be the totally rigid grammar G(π) = N R , Σ, θ, P with

N R = EV(π) ∪ {θ} Σ = Σ(π) ∪ {∧, ∨} P = {θ → A | A ∈ H(π)} ∪ {α → t | [α\t] ∈ B(π)}
where Σ(π) is the signature of π, the rank of ∧ and ∨ is 2, and θ does not occur in π.

Lemma 19. If π is a simple proof, then G(π) is acyclic.
Proof. By induction on the number of cuts in π. The grammar of a cut-free proof is trivially acyclic. For the induction step, let r be the lowest binary inference with subproofs π 1 and π 2 s.t. either (i) r is a cut or (ii) r is not a cut but both π 1 and π 2 contain at least one cut. Let P , P 1 , and P 2 be the set of productions induced by the cuts in π, π 1 , π 2 , respectively. In case (ii), ≺ P = ≺ P1 ∪ ≺ P2 , which is acyclic by induction hypothesis (since EV(π 1 ) ∩ EV(π 2 ) = ∅). In case (i), let P r be the productions induced by the cut r, then ≺ P = ≺ P1 ∪ ≺ P2 ∪ ≺ Pr . By induction hypothesis, ≺ P1 and ≺ P2 are acyclic and as the cut-formula in r contains at most one quantifier, also ≺ Pr is acyclic. Therefore, a cycle in ≺ + P must be of the form

α 1 ≺ * P1 β 1 ≺ Pr α 2 ≺ + P2 β 2 ≺ Pr α 1 where α 1 , β 1 ∈ EV(π 1
) and α 2 , β 2 ∈ EV(π 2 ). However, r contains only one quantifier and depending on its polarity all productions in P r lead from π 1 to π 2 or from π 2 to π 1 but not both, so ≺ P is acyclic.

We now come to a central definition of this paper.

Definition 20. For a simple proof π, we define its Herbrand-content as [[π]] = L(G(π)).

Lemma 19 together with Lemma 12 implies that the Herbrand-content of a simple proof π with n cuts can be written as

[[π]] = {A[α 1 \t 1 ] • • • [α n \t n ] | A ∈ H(π), [α i \t i ] ∈ B(α i )}.
Note that for cut-free π we have [[π]] = H(π), i.e. the Herbrand-content is nothing else but the Herbrand-disjunction induced by the proof. Furthermore, the Herbrand-content is a strong invariant: it is not changed by axiom reduction, propositional reduction and inference permutations as those transformations do not change the grammar. Furthermore, Lemma 7 shows that [[π]] is not changed by quantifier reduction and Lemma 8 shows that if π π is a step of weakening reduction then

[[π ]] ⊆ [[π]].
A more difficult result is that the Herbrand-content is even invariant under the reduction of a contraction; the following section is devoted to proving this.

Invariance under Duplication

For simplifying the presentation, we assume in the following (without loss of generality) that the ∀-side is on the right of a cut and the ∃-side on the left. Then, a production β → t in G(π) corresponds to three inferences in π: a cut, an instance of the ∀-rule, and an instance of the ∃-rule, that we denote by cut β , ∀ β , and ∃ t , respectively, and that are, in general, arranged in π as shown below.

Γ , A[x\t]

-----------∃t Γ , ∃x A . . . ---------------------------------

Γ, ∃x A A[x\β], ∆ ------------∀ β ∀x A, ∆ . . . ∀x A, ∆ -
-cut β Γ, ∆ (2)
The additional condition that ∀ β is directly above cut β , as indicated in ( 1) is only needed because in the following we make extensive use of Observation 14: there is a one-to-one correspondence between the cuts and the eigenvariables in π, and thus, the notation cut β makes sense. Furthermore, we say that the instances cut β , ∀ β , and ∃ t are on a path P in G(π) if the production β → t is in P.

Definition 21.

Let π be a proof containing the configuration . . . ------r1 . . . . . .

-----r2 . . . ------------------r3 . . .

, where r 1 , r 2 , and r 3 are arbitrary rule instances, and r 3 is a branching rule, and r 1 and r 2 might or might not be branching. Then we say that r 1 is on the left above r 3 , denoted by r 1 r 3 , and r 2 is on the right above r 3 , denoted by r 3 r 2 , and r 1 and r 2 are in parallel, denoted by r 1 r 2 .

Lemma 22.

Let π be a simple proof and P : α 1 → t 1 α 2 . . . → t n be a path in G(π). Then there is a k ∈ {1, . . . , n} s.t. cut α k is lowermost among all inferences on P. Furthermore, ∀ α1 is on the right above cut α k and ∃ tn is on the left above cut α k .

Proof. We proceed by induction on n. If n = 1, then n = k = 1. For the induction step consider a path α 1 → t 1 . . . α n → t n α n+1 → t n+1 . As α n+1 ∈ t n we know that ∃ tn C S L ' 1 2 must be on the right above cut αn+1 . By induction hypothesis there is a k ∈ {1, . . . , n} such that we are in one of the following two situations . . . -------------------cutα k . . . ----------------------------cutα n+1 . . . ---------------------cutα n+1 . . . . . .

-----∀α 1 . . . --------------------------------cutα k . . .

In the first case we let l = n + 1 and in the second we let l = k. In both cases cut α l has the desired properties.

Lemma 23. Let π be a simple proof, G(π) = N R , Σ, θ, P , and β, α ∈ EV(π). If β α then either cut α cut β or cut α cut β or cut α cut β .

Proof. Since β α, we have a path β → . . . α → t for some t. By Lemma 22 there is a γ, such that ∃ t cut γ and cut γ ∀ β , and such that cut α and cut β are not below cut γ . Furthermore, cut α must be below ∃ t , and

cut β below ∀ β . If γ = β, then cut α cut β . If γ = α, then cut α cut β . And if γ = β and γ = α, then cut α cut β .
Lemma 24. Let G(π) = N R , Σ, θ, P be the grammar of a simple proof π, such that there are two paths

β → t γ 0 → s 0 γ 1 → s 1 . . . → s n-1 γ n = α → s n β → t δ 0 → r 0 δ 1 → r 1 . . . → r m-1 δ m = α → r m
such that γ 0 and δ 0 occur at two different positions in t. Then we have one of the following two cases: 1. we have γ i = δ j for some 0 ≤ i < n and 0 ≤ j < m, or 2. for all 0 ≤ i < n and 0 ≤ j < m we have cut α cut γi and cut α cut δj .

Proof. Note that because of acyclicity of G(π), we have that β = γ i for all i ≤ n and β = δ j for all j ≤ m, in particular β = α. Assume, for the moment, that m, n > 0; the case of one of them being zero will be treated at the very end of the proof. Then γ 0 = α and δ 0 = α. If γ 0 = δ 0 , we have case 1. So, assume also γ 0 = δ 0 . As β → t is a production in G(π), the proof π contains a formula which contains both γ 0 and δ 0 hence ∀ γ0 and ∀ δ0 are not parallel. Since we have cut γ0 ∀ γ0 and cut δ0 ∀ δ0 , we also have that cut γ0 and cut δ0 are not parallel. Without loss of generality, assume that cut δ0 is below cut γ0 . Then cut δ0 cut γ0 (since cut γ0 cut δ0 would entail ∀ γ0 ∀ δ0 ). Since we have δ 0 α, we can apply Lemma 23, giving us three possibilities:

If cut α cut δ0 then we have the situation -------------------cutα . . . . . .

-----∃s 0 . . . . . .

-----∀γ 0 . . . -------------------cutγ 0 . . . ----------------------------------cut δ0 . . .

. By Lemma 22 applied to the path γ 0 s n we have that cut δ0 must coincide with cut γi for some 0 ≤ i < n (since π is a tree), so δ 0 = γ i (by Observation 14), and we are in case 1.

If cut α cut δ0 then we are in both of the following two situations:

. . . -----∀γ 0 . . . --------------cutγ 0 . . . -------------------cut δ0 . . . --------------------------cutα . . . --------------cut δ0 . . . ------------------------cutα . . . Thus, by Lemma 22 applied to the paths γ 0 s n and δ 0 r m we know that cut α = cut γ k = cut δ l for some 0 ≤ k ≤ n and 0 ≤ l ≤ m hence γ k = α = δ l . Furthermore k = n and l = m by acyclicity of G(π). Now consider any γ i with 0 ≤ i < n. Since γ i α, we can apply Lemma 23 and get either cut α cut γi or cut α cut γi or cut α cut γi . Since by Lemma 22 cut γi must be above cut α , we conclude cut α cut γi . With the same reasoning we can conclude that cut α cut δj for all 0 ≤ j < m. We are therefore in case 2. If cut α cut δ0 then we are in both of the following two situations:

. . .

-----∃s n . . . . . . -------------------cutα . . . . . . . . . . . .
-----∀γ 0 . . . -----------------cutγ 0 . . . --------------------cut δ0 . . . ----------------------------------r . . .

and

. . .

-----∃r m . . . . . . -------------------cutα . . . . . . . . .

-----∀ δ0 . . . -----------------cut δ0 . . . ---------------------------------r . . .

By Lemma 22 applied to the paths γ 0 → . . . → s n and δ 0 → . . . → r m , the rule r coincides with cut γi and cut δj for some 0 < i < n and 0 < j < m, therefore γ i = δ j (by Observation 14), and we are in case 1. It remains to treat the case n = 0 or m = 0. If m = n = 0 then we are trivially in case 2 (there is no 0 ≤ i < n or 0 ≤ j < m). If n = 0 and m > 0, we can apply Lemma 22 to the path δ 0 → . . . → r m and obtain an l ∈ {0, . . . , m} such that we are in the situation -------------------cutα . . . . . . . . .

-----∀ δ0 . . . -----------------cut δ0 . . . ---------------------------------cut δl . . .

But by the same argument as at the beginning of the proof, we also have that ∀ α and ∀ δ0 cannot be in parallel (α and δ 0 both appear in t), and therefore either cut δ0 cut α or cut α cut δ0 . Since δ 0 α, the only possibility is cut α cut δ0 , by Lemma 23. Thus cut α = cut δ l , and therefore l = m and we are in case 2. The case m = 0 and n > 0 is similar.

The following is the main result of this section: Proposition 25. Let π be a simple proof that contains a subproof ψ, shown on the left below, -----------------------------

ψ = ψ1 Γ, A, A --------c Γ, A ψ2 A, ∆ --------------------cut Γ, ∆ ; ψ1 Γ, A, A ψ2ρ A, ∆ ---------------------cut Γ, ∆, A ψ2ρ A, ∆ -
(π ). Let F ∈ [[π]] = L(G(π))
and D be its derivation. If the duplicated cut is quantifierfree, then P = P ρ ∪ P ρ hence Dρ (as well as Dρ ) is a derivation of F in G(π ). If the duplicated cut contains a quantifier, let α be its eigenvariable, let t 1 , . . . , t k be its terms coming from the left copy of A and t k+1 , . . . , t n those from the right copy of A and let Q = {α → t 1 , . . . , α → t n } ⊆ P . We then have

P = (P \ Q)ρ ∪ {α → t1, . . . , α → t k } ∪ (P \ Q)ρ ∪ {α → t k+1 , . . . , α → tn} .
If D does not contain α, then Dρ (as well as Dρ ) is a derivation of F in G(π ). If D does contain α, then by Lemma 6 we can assume that it uses only one α-production, say α

→ t i . If 1 ≤ i ≤ k, then Dρ is a derivation of F in G(π ) and if k < i ≤ n, then Dρ is a derivation of F in G(π ). Let us now show [[π ]] ⊆ [[π]]: let F be a formula in [[π ]] = L(G(π ))
, and let D be a derivation of F in G(π ). We construct D = D (ρ ) -1 (ρ ) -1 by "undoing" the renaming of the variables in ψ 2 . Then D is a derivation for F , using the production rules of G(π), but possibly violating the rigidity condition.

First, observe that only non-terminals α ∈ EV(ψ 2 ) can violate the rigidity condition in with n(D, α) > 0. We now pick one such α which is minimal with respect to ≺ * (which exists since G(π) is acyclic). Let p 1 and p 2 be α-positions in D with p 1 = p 2 and F | p1 = F | p2 , let p be the maximal common prefix of p 1 and p 2 and let q be the maximal prefix of p where a production rule has been applied in D. Due to the tree structure of F , the position q is uniquely defined, and q is a β-position for some non-terminal β, and some production rule β → t has been applied at position q in D, and we have two paths:

D: if β / ∈ EV(ψ 2 )
β → t γ0 → s0 γ1 → s1 . . . → sn-1 γn = α → sn β → t δ0 → r0 δ1 → r1 . . . → rm-1 δm = α → rm
where γ 0 and δ 0 occur at two different positions in t. Thus, we can apply Lemma 24, giving us the following two cases:

We have γ i = δ j for some 0 ≤ i < n and 0 ≤ j < m. Say η = γ i = δ j , and let p γ and p δ be the positions of γ i and δ j (respectively) in D. Since η ≺ + α we know that η does not violate the rigidity condition (we chose α to be minimal), and therefore

F | pγ = F | p δ = F . Let D γ : γ i → * G(π)
F and D δ : δ j → * G(π) F be the two subderivations of D starting in positions p γ and p δ , respectively. Without loss of generality, we can assume that n(D γ ) ≤ n(D δ ). Then let D be the derivation obtained from D by replacing D δ by D γ . Then D is still a derivation for F , but n( D) < n(D). For all 0 ≤ i < n and 0 ≤ j < m we have cut α cut γi and cut α cut δj . So all inferences of the path γ 0 → . . . → s n-1 as well as all inferences of δ 0 → . . . → r m-1 are in ψ 2 . Therefore all variables of of these paths are in EV(ψ 2 ). As α violates the rigidity in D one of p 1 , p 2 must be a α -position and the other a α -position in D because D does satisfy the rigidity condition. Without loss of generality we can assume that p 1 is the α -position and p 2 the α -position. As the paths are contained completely in ψ 2 we have γ 0 ∈ EV(ψ 2 )ρ and δ 0 ∈ EV(ψ 2 )ρ which is a contradiction as no term can contain both a variable from EV(ψ 2 )ρ and one from EV(ψ 2 )ρ .

Herbrand-Confluence

We now turn to cut reduction sequences that start with a simple proof. All the reductions shown in Figure 1 preserve simplicity, except the following:

• • • • • • --------∀α • • • --------------------cutα • • • • • • --------∀ β • • • ------------------------------------cut β • • • ; • • • • • • --------∀α • • • • • • --------∀ β • • • ----------------------------cut β • • • ------------------------------cutα • • •
where cut α is permuted down under cut β (using the bottommost reduction in Fig. 1) and the cut formula of cut β has its ancestor on the right side of cut α . So in the following, when we speak about a reduction sequence of simple proofs we require that the above reduction is immediately followed by permuting ∀ α down as well, in order to arrive at

• • • • • • • • • --------∀ β • • • ------------------------cut β • • • --------∀α • • • ----------------------------cutα • • •
which is again simple. Recall that for our result this step is not strictly needed. We only add it here to simplify the presentation.

Collecting together the results proved in this paper we then obtain the following theorem.

This corollary shows that [[π]

] is an upper bound (w.r.t. the subset relation) on the Herbrand-disjunctions obtainable by cut-elimination from π. Let us now compare this result with another upper bound that has previously been obtained in [START_REF] Hetzl | On the form of witness terms[END_REF]. To that aim let G 0 (π) denote the regular tree grammar underlying G(π) which can be obtained by setting all nonterminals to non-rigid. In this notation, a central result of [START_REF] Hetzl | On the form of witness terms[END_REF], adapted to this paper's setting of proofs of non-prenex formulas, is Theorem 28. If π π and π is cut-free, then H(π ) ⊆ L(G 0 (π)).

While the above theorem 28 applies also to non-simple proofs, Corollary 27 is stronger in several respects:

First, the size of the Herbrand-content is by an exponential smaller than the size of the bound given by Theorem 28. Indeed, it is a straightforward consequence of Lemma 12 that C S L ' 1 2 the language of a totally rigid acyclic tree grammar with n production rules is bound by n n . On the other hand, there are acyclic regular tree grammars G n with 2n productions and |L(G n )| = n n n (by encoding in G n the construction of a tree of depth n and branching degree n with an independent choice between n constant symbols at each leaf). These grammars can be obtained from appropriately constructed proofs.

Secondly, the class of totally rigid acyclic tree grammars can be shown to be in exact correspondence with the class of simple proofs in the following sense. Not only can we use a totally rigid acyclic tree grammar to simulate the process of cut-elimination, we can also-in the other direction-use cut-elimination to simulate the process of calculating the language of a grammar. It is shown in [START_REF] Hetzl | Applying Tree Languages in Proof Theory[END_REF] how to transform an arbitrary acyclic totally rigid tree grammar G into a simple proof that has a normal form whose Herbrand-disjunction is essentially the language of G.

The third and-for the purposes of this paper-most important difference is that the bound of Corollary 27 is tight (in a sense that we are going to make precise now). This property of the Herbrand-content leads naturally to a confluence result for classical logic.

For tightening this bound, a first obvious observation is that there is no mechanism for deletion in the grammar but there is one in cut-elimination: the reduction of weakening. So, any cut-elimination strategy that does exactly compute [[π]] must be non-erasing. Consequently we define the non-erasing cut-reduction ne as without the reduction rule for weakening. Note that a ne -normal form π is an analytic proof as well, e.g. H(π) is a (tautological!) Herbrand-disjunction. In contrast to a -normal form (which might contain implicit redundancy) a ne -normal form might also contain explicit redundancy in the form of cuts whose cut-formulas are introduced by weakening on one or on both sides. Non-erasing reduction is also of interest in the context of the λ-calculus where it is often considered in the form of the λI-calculus and gives rise to the conservation theorem (see Theorem 13.4.12 in [START_REF] Pieter | The Lambda Calculus[END_REF]). Our situation here is however quite different: neither nor ne is confluent and neither of them is strongly normalizing. Nevertheless we obtain: Proof. Inspection of the proof of Theorem 26 shows that the reduction of weakening is the only step that does not preserve the Herbrand-content.

Definition 30 (Herbrand-confluence). A relation -→ on a set of proofs is called Herbrandconfluent iff π -→ π 1 and π -→ π 2 with π 1 and π 2 being normal forms for -→ implies that H(π 1 ) = H(π 2 ).

Corollary 31. The relation

ne is Herbrand-confluent on the set of simple proofs.

How do these results fit together with ne being neither confluent nor strongly normalizing? In fact, note that it is possible to construct a simple proof which permits an infinite ne reduction sequence from which one can obtain normal forms of arbitrary size by bailing out from time to time. This can be done by building on the propositional double-contraction example found e.g. in [START_REF] Vincent Danos | A New Deconstructive Logic: Linear Logic[END_REF][START_REF] Gallier | Constructive Logics. Part I: A Tutorial on Proof Systems and Typed λ-Calculi[END_REF][START_REF] Urban | Classical Logic and Computation[END_REF] and in a similar form in [START_REF] Zucker | The Correspondence Between Cut-Elimination and Normalization[END_REF]. While these infinitely many normal forms do have pairwise different Herbrand-disjunctions when regarded as multisets, Corollary 31 shows that as sets they are all the same. This observation shows that the lack of strong normalization is taken care of by using sets instead of multisets as data structure.

But what about the lack of confluence? Results like [START_REF] Baaz | On the non-confluence of cut-elimination[END_REF] and [START_REF] Hetzl | The Computational Content of Arithmetical Proofs[END_REF] show that the number of normal forms with different Herbrand-disjunctions can be enormous. On the other hand we have just seen that

Conclusion

We have shown that non-erasing cut-elimination for the class of simple proofs is Herbrandconfluent. While there are different and possibly infinitely many normal forms, they all induce the same Herbrand-disjunction. This result motivates the definition of this unique Herbrand-disjunction as Herbrand-content of the proof with cut. As future work, the authors plan to extend this result to arbitrary first-order proofs. The treatment of blocks of quantifiers is straightforward: the rigidity condition must be changed to apply to vectors of non-terminals. Treating quantifier alternations is more difficult: the current results suggest to use a stack of totally rigid tree grammars, each layer of which corresponds to one layer of quantifiers (and is hence acyclic). Concerning further generalizations, note that the method of describing a cut-free proof by a tree language is applicable to any proof system with quantifiers that has a Herbrand-like theorem, e.g., even full higher-order logic as in [START_REF] Miller | A Compact Representation of Proofs[END_REF]. The difficulty consists in finding an appropriate type of grammars.

Given the wealth of different methods for the extraction of constructive content from classical proofs, what we learn from our work is this: the first-order structure possesses (in contrast to the propositional structure) a unique and canonical unfolding. The various extraction methods hence do not differ in the choice of how to unfold the first-order structure but only in choosing which part of it to unfold. We therefore see that the effect of the underspecification of algorithmic detail in classical logic is redundancy.

C S L ' 1 2

 2 cut Γ, ∆, ∆ = = = = = = = = = c * Γ, ∆ = ψ and let π be the proof obtained from π from replacing ψ by ψ shown on the right above, where ρ = [α\α ] α∈EV(ψ2) and ρ = [α\α ] α∈EV(ψ2) are substitutions that replace all eigenvariables in ψ 2 by fresh copies. Then [[π]] = [[π ]]. Proof. Let us first show [[π]] ⊆ [[π ]]: write P for the productions of G(π) and P for those of G

  violates the rigidity condition then there are β-positions p 1 , p 2 in D with F | p1 = F | p2 and as βρ ρ = β the positions p 1 , p 2 are also β-positions in D and they violate the rigidity condition in D which is a contradiction to D being a G(π )-derivation. Now define for each α ∈ EV(ψ 2 ) the value n(D, α) to be the number of pairs (p 1 , p 2 ) ∈ Pos(F ) × Pos(F ) where p 1 and p 2 are α-positions in D with p 1 = p 2 and F | p1 = F | p2 , and define n(D) = α∈EV(ψ2) n(D, α). We proceed by induction on n(D) to show that D can be transformed into a derivation which does no longer violate rigidity. If n(D) = 0 then D obeys the rigidity condition, and we are done. Otherwise there is at least one α ∈ EV(ψ 2 )

Theorem 26 .

 26 If π π is a reduction sequence of simple proofs, then [[π]] ⊇ [[π ]]. Proof. By induction on the length of the reduction π π making a case distinction on the applied reduction step. If π i π i+1 is a propositional reduction, an axiom reduction or a rule permutation, we even have G(π i ) = G(π i+1 ). If it is a quantifier reduction, then [[π i ]] = [[π i+1 ]] by Lemma 7. If it is the reduction of a contraction, then [[π i ]] = [[π i+1 ]] by Proposition 25. If it is the reduction of a weakening, then [[π i ]] ⊇ [[π i+1 ]] by Lemma 8. Corollary 27. If π π is a reduction sequence of simple proofs and π is cut-free, then H(π ) ⊆ [[π]].

Theorem 29 .

 29 If π ne π is a reduction sequence of simple proofs, then [[π]] = [[π ]].

  ne induces only a single Herbrand-disjunction: [[π]]. The relation between [[π]] and the many Herbrand-disjunctions induced by is explained by Corollary 27: [[π]] contains them all as subsets.

Acknowledgments

The authors would like to thank Paul-André Melliès for helpful comments on this work. The first author was supported by a Marie Curie Intra European Fellowship within the 7th European Community Framework Programme and by the projects I-603 N18 and P22028 of the Austrian Science Fund (FWF).