Weak cut-elimination and the game-theoretic approach of Novikoff’s provability — Draft version

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

October 18, 1996

In this paper, we consider a notion of provability similar to Novikoff’s notion of regularity [2]. Such a notion of provability amounts to a notion of cut-free proofs and we introduce a notion of cuts between such cut-free proofs. We consider a cut-elimination process using a game-theoretic interpretation, defined by Coquand [1], and called “debate” by him. We show that the debate corresponds to the trace of the execution of a certain cut-elimination procedure — in the usual sense. A particularity of this procedure is that it reduces the head cut of the proof and stops when the head of the proof becomes the introduction rule of a connective. In analogy with λ-calculus terminology, such a procedure could be called weak cut-elimination or, with more emphasis, weak-head cut-elimination.

Contents

1 Novikoff’s calculus 1 1.1 Formulas and sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 The cut rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Proofs with explicit cut . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.5 Partial proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Game-theoretic interpretation 4 2.1 Strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Equivalence between winning strategies and Novikoff’s proofs . . . . . . . . . . 4 2.3 Partial strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Elimination of a cut 5 3.1 Interaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 The weak-head cut-elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.3 Termination of the weak-head cut-elimination . . . . . . . . . . . . . . . . . . . 8

4 The equivalence 8 4.1 Clean proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 4.2 Trace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.3 Conformity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

∗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”.

1 Novikoff’s calculus

We describe Novikoff’s calculus following Coquand’s description in [1]. Formulas are wellfounded trees.

1.1 Formulas and sequents

Formulas are alternately conjunctively and disjunctively branched trees of which the leaves are atoms.

• 0 and 1 are formulas and are both conjunctive and disjunctive

• if (A_{i})_{i∈I} is a family of conjunctive formulas, then Σ_{i∈I}A_{i} is a disjunctive formula

• if (A_{i})_{i∈I} is a family of disjunctive formulas, then Π_{i∈I}A_{i} is a conjunctive formula

As in Tait [3], we leave unspecified the exact form of the index sets over which Π and Σ range.

The negation of A, written A^{⊥} is inductively defined as:

• 1^{⊥} = 0 and 0^{⊥} = 1

• (Σ_{i∈I}A_{i})^{⊥} = Π_{i∈I}A_{i}^{⊥}

• (Π_{i∈I}A_{i})^{⊥} = Σ_{i∈I}A_{i}^{⊥}

The notion of occurrence is a standard notion on trees. Here, an occurrence in a given formula defines a subformula of it. We use the letters u, v, w, ... for denoting occurrences.

• <> is the occurrence of A as a subformula of itself

• if u is the occurrence of the subformula Σ_{i∈I}A_{i} of A then ui is the occurrence of the subformula A_{i} of A

• if u is the occurrence of the subformula Π_{i∈I}A_{i} of A then ui is the occurrence of the subformula A_{i} of A

The occurrence ui is called a direct extension of u.

We consider an infinite set N called the set of names. Together with this set, we consider a function New which associates to each subset X and Y of N a subset X′ such that X′ is in correspondence with X and X′ is disjoint from the X ∪ Y.

A sequent is a family of occurrences such that there exists a formula A and that the occurrences are references to conjunctive subformulas of A. The family has to be indexed on a subset of N.

The capitalized greek letters Γ, Δ denotes sequents. The meaning of a sequent is the (possibly infinite) disjunction of its constituents. Thus, a sequent is often written Σ_{x∈X}A_{x}. The notation Σ_{y∈Y} A_{y} + Σ_{z∈Z}B_{z} with Y and Z disjoint has to be understood as a sequent indexed on Y ∪ Z. Moreover [Γ_{i}]_{i∈I} stands for a family of sequent.

1.2 Proofs

A Novikoff’s proof is a well-founded tree defined inductively by means of the two following inferences:

\begin{matrix}[Σ_{x∈X\\{x_{0}\}}A_{x} + A_{j}] & j∈J \\ Σ_{x∈X}A_{x} \end{matrix} where A_{x_{0}} = Π_{j∈J}A_{j}

Σ_{x∈X}A_{x} where A_{x_{0}} = 1

Remark: By adopting the convention that 1 = Π_{i∈∅}, the second rule becomes a subcase of the first one. This identification will be made implicitly hereafter. Note that this implies 0 = Π_{i∈∅}. Since 1 becomes purely conjunctive and 0 purely disjunctive, formulas have to be “restructured” but in an unimportant way.

1.3 The cut rule

According to the Hauptsatz, the cut rule

Γ_{1} + Δ + Π_{j∈J}A_{j} Γ_{2} + Δ + Σ_{y∈Y} A_{y}^{⊥}
Γ_{1} + Γ_{2} + Δ

where (A_{j})_{j∈J} and (A_{y}^{⊥})_{y∈Y} are in correspondence is an admissible rule of inference. (A_{j})_{j∈J} and (A_{y}^{⊥})_{y∈Y} in correspondence means that there is a bijection between J and Y such that the family (A_{y}^{⊥})_{y∈Y} of occurrences exactly matches the family of occurrences of the formulas (A_{j})_{j∈J} (note that occurrences are invariant by negation and that the ^{⊥} symbol is just for consistency with the usual presentation of sequent calculus).

In the following, the cut rule only appears in the particular case where the left side comes directly from the introduction of Π_{i∈I}A_{i}. I.e. a cut only occurs in this configuration:

\begin{matrix}[Γ_{1} + Δ + Π_{i∈I}A_{i} + A_{j}] & j∈J \\ Γ_{1} + Δ + Π_{j∈J}A_{j} \end{matrix} Γ_{2} + Δ + Σ_{y∈Y} A_{y}^{⊥}
Γ_{1} + Γ_{2} + Δ

Remark: To have a common Δ and proper Γ_{1}, Γ_{2} in the cut rule is a kind of trick which avoids introducing an explicit contraction rule in the calculus with cut. This is useful since contractions appear during the process of cut-elimination.

1.4 Proofs with explicit cut

A renaming map σ is a bijection from a set X ⊂ N to a subset Y ⊂ N. The range Y of σ is denoted by Rσ.

We give an explicit term notation for proofs.

• if, for each j ∈ J, we have that p_{j} is a proof of Σ_{x∈X}A_{x} + A_{x_{0}j}, and if for each j ∈ J, Z is the set of names of the disjunctive formula A_{x_{0}j}, then !x_{0}?j ↦^{Z} p_{j} is a proof of Σ_{x∈X}A_{x}

• if, for each y ∈ Y, we have that p_{y} is a proof of Σ_{x_{1}∈X_{1}}A_{x_{1}} + Σ_{x∈X}A_{x} + A_{y} and, for each y ∈ Y, Z is the set of names of the disjunctive formula A_{y} and q is a proof of Σ_{x′_{2}∈X′_{2}}A_{x′_{2}} + Σ_{x′∈X′}A_{x′} + Σ_{y∈Y} A_{j}^{⊥} then

Cut_{(X′,σ)}(?y∈Y ↦^{Z} p_{y}, q) is a proof of Σ_{x_{1}∈X_{1}}A_{x_{1}} + Σ_{x_{2}∈X_{2}}A_{x_{2}} + Σ_{x∈X}A_{x}

where:

X′ is X_{1} ∪ X and σ is a renaming map from X′_{2} into X_{2} and from X′ into X

A cut-free proof is a proof without cut.

Remark: 1) Cut-free proofs do not fit exactly Novikoff’s proofs. The difference lies in whether or not one allows redundancies. The interest in Novikoff’s proofs is their direct correspondence with winning strategies. The interest in the allowance of redundancies is the simplification of the description of weak cut-elimination. Effectively, Novikoff’s proofs are not stable under cut-elimination: the resulting cut-free proof may have redundancies after elimination of cuts. In the sequel, we use the term Novikoff’s proof to express a cut-free proof without redundancy.

2) A proof of Π_{i∈I}A_{i} is understood as a proof of a sequent with a unique formula. We write ?i ↦^{Y} p_{i} for such a proof.

1.5 Partial proofs

We will also consider partial proofs. For this purpose, we add to the definition of proof the clause

⊥ is a proof of Γ

for any sequent Γ.

2 Game-theoretic interpretation

2.1 Strategies

Let A be a formula.

A line on A is a non empty sequence u_{1}...u_{n} of occurrences of disjunctive subformulas of A such that:

• if A is disjunctive, <> is a line (of length 1)

• if A = Π_{i∈I}A_{i}, for each i ∈ I, i is a line (of length 1)

• u_{1}...u_{n+1} is a line if u_{1}...u_{n} is a line and if there exists exactly one m ≤ n and v such that u_{n+1} is a direct extension of v and v is a direct extension of u_{m}.

A strategy for A is a function ϕ defined on a set Dom(ϕ) of lines and with values in the set of occurrences of conjunctive subformulas in A. A strategy has to satisfy two properties.

1. Dom(ϕ) contains the lines of length 1 and if ϕ(u_{1}...u_{n}) = v and v denotes Π_{i∈I}A_{i}, then for all i ∈ I, letting u_{n+1} = vi, we have u_{1}...u_{n+1} ∈ Dom(ϕ)

2. if u_{1}...u_{n+1} ∈ Dom(ϕ) then u_{1}...u_{n} ∈ Dom(ϕ), u_{n+1} is a direct extension of v = ϕ(u_{1}...u_{n}) and v is a direct extension of one of the u_{i}

A strategy ϕ is winning at u_{1}...u_{n} ∈ Dom(ϕ) if v = ϕ(u_{1}...u_{n}) denotes Π_{i∈I}A_{i} and for all i ∈ I, letting u_{n+1} = vi, ϕ is winning at u_{1}...u_{n+1}

As a special case, if ϕ(u_{1}...u_{n}) = 1 then ϕ is winning at u_{1}...u_{n}.

A strategy ϕ is winning if it is winning for all lines of length 1.

Remark: In particular, a strategy for a conjunctive formula Π_{i∈I}A_{i} is winning if it is winning for each A_{i}.

2.2 Equivalence between winning strategies and Novikoff’s proofs

There is a direct correspondence between a Novikoff’s proof of A and a winning strategy for A.

Let p be a Novikoff’s proof of A (the case A conjunctive is understood as a sequent just containing the formula A). To each subproof of p is associated a line, and conversely.

• the line <> is associated to p as a subproof of itself

• if the line associated to the subproof q is u_{1}...u_{n} and q comes from the family q_{j} by the introduction rule:

\begin{matrix}[Σ_{i∈I}A_{i} + A_{i_{0}j}] & j∈J \\ Σ_{i∈I}A_{i} \end{matrix} and A_{i_{0}} = Π_{j∈J}A_{i_{0}j}

then the line associated to q_{j} is u_{1}...u_{n}u where v is the occurrence associated to A_{i_{0}}and u = vj.

Remark: The absence of redundancies implies that the sequences u_{1}...u_{n} are effectively lines.

The translation of p into a winning strategy ϕ is now direct. The strategy ϕ associated to p has the set of lines associated to the subproofs of p as domain Dom(ϕ) and if the subproof of p corresponding to the line u_{1}...u_{n} ∈ Dom(ϕ) comes from the introduction rule

\begin{matrix}[Σ_{x∈X}A_{x} + A_{j}] & j∈J \\ Σ_{x∈X}A_{x} \end{matrix} and A_{x_{0}} = Π_{j∈J}A_{j}

then ϕ(u_{1}...u_{n}) is defined as v where v is the occurrence associated to A_{x_{0}}.

Reciprocally, Dom(ϕ) has the structure of a set of occurrences for a proof p seen as a tree. For each u_{1}...u_{n} ∈ Dom(ϕ), ϕ(u_{1}...u_{n}) determines which names is chosen in the introduction rule of which comes the subproof of p associated to u_{1}...u_{n}. The determination is unambiguous by virtue of the absence of redundancies.

2.3 Partial strategies

The analogue of partial proofs is partial strategies.

A partial strategy differs from a strategy by dropping the condition 1 of the definition of strategy.

A partial strategy ϕ is non-losing at u_{1}...u_{n} either if u_{1}...u_{n} ∉ Dom(ϕ) or, in case where u_{1}...u_{n} ∈ Dom(ϕ) and v = ϕ(u_{1}...u_{n}) denotes Π_{i∈I}A_{i}, when for all i ∈ I, letting u_{n+1} = vi, ϕ is non-losing at u_{1}...u_{n+1}.

There is a direct correspondence between a partial cut-free proof of A and a partial nonlosing strategy for A.

3 Elimination of a cut

We consider a cut between two Novikoff’s proofs p and q that we consider as objects of the calculus with explicit cut. We consider an abstract case where p is a proof of Π_{i∈I}A_{i} (a sequent with a single item) and q is a proof of Σ_{x∈X}A_{x}^{⊥} ((A_{i})_{i∈I} and (A_{x})_{x∈X} are in correspondence). In harmony with the consistency of our calculus, strictly speaking, we do not consider proofs but partial proofs. We do not expect to obtain a cut-free proof of the empty sequent but rather to show that the cut-elimination eventually stops (and yields ⊥ as proof of the empty sequent).

We first describe Coquand’s debate, then a cut-elimination procedure in the standard style.

3.1 Interaction

Let A be a disjunctive formula Σ_{i∈I}A_{i}^{⊥}. We consider a partial non-losing strategy ϕ for A and a partial non-losing strategy τ for Π_{i∈I}A_{i}.

A debate for A is a sequence d of pairs of integers and of occurrences of A such that if d(n) = (f_{n}, u_{n}) then either f_{n} = 0 and u_{n} is a direct extension of <> or f_{n} < n and u_{n} is a direct extension of u_{f_{n}}. In the following, we adopt the convention that u_{0} =<>. According to this convention, the condition “f_{n} = 0 and u_{n} is a direct extension of <>” becomes a subcase of the other condition.

The debate is inductively defined simultaneously with the lines of the debate. The sequence of lines of the debate is an important notion, since it contains all the information necessary to recover the debate.

The sequence l of lines of the debate is inductively defined by:

• if n = 0 or f_{n} = 0 then l(n) = u_{n}

• if l(f_{n} − 1) = u_{n_{1}}...u_{n_{p}} then l(n) = u_{n_{1}}...u_{n_{p}}u_{n}

Remark: Odd integers correspond to moves of ϕ, even integers to moves of τ. f_{n} is the index of the move to which the n^{th} move answers. Thus, f_{n} and n are always of distinct parity.

The debate is inductively defined by:

• if n is even then let u_{n_{1}}...u_{n_{p}} = l(n) and u_{n+1} = ϕ(u_{n_{1}}...u_{n_{p}}). If u_{n+1} is a direct extension of u_{n_{k}} then we let d(n + 1) = (n_{k}, u_{n+1}).

• if n is odd then let u_{n_{1}}...u_{n_{p}} = l(n) and u_{n+1} = τ(u_{n_{1}}...u_{n_{p}}). If u_{n+1} is a direct extension of u_{n_{k}} then we let d(n + 1) = (n_{k}, u_{n+1}).

Proposition 1 The debate between ϕ and τ eventually stops

The proof can be found in Coquand [1]

3.2 The weak-head cut-elimination

We consider a partial proof p with cuts. A pattern-matching analysis of the cut nodes of p allows to transform p into a “smaller” proof.

1. The left introduction rule selects A_{x_{0}}^{⊥} = Π_{j∈J}B_{j}^{⊥} which is a part of the cut formula

\begin{matrix}\left[{⋮ . p_{i} \atop Δ + Γ_{1} + Π_{i∈I}A_{i} + A_{i}}\right] & i∈I \\ Δ + Γ_{1} + Π_{i∈I}A_{i} \end{matrix}  \begin{matrix}\left[{⋮ . q_{j} \atop Δ + Γ_{2} + Σ_{x∈X}A_{x}^{⊥} + B_{j}^{⊥}}\right] & j∈J \\ Δ + Γ_{2} + Σ_{x∈X}A_{x}^{⊥} \end{matrix}
Δ + Γ_{1} + Γ_{2}

reduces to

[\begin{matrix}\begin{matrix}\left[{⋮ . p_{i} \atop Δ + Γ_{1} + Π_{i∈I}A_{i} + A_{i}}\right] & i∈I \\ Δ + Γ_{1} + Π_{i∈I}A_{i} \end{matrix} & {⋮ . q_{j} \atop Δ + Γ_{2} + Σ_{i∈I}A_{i}^{⊥} + B_{j}^{⊥}} \\ Δ + Γ_{1} + Γ_{2} + B_{j}^{⊥} \end{matrix} ]_{j∈J}

Δ + Γ_{1} + Γ_{2} + Π_{j∈J}B_{j}^{⊥}

{⋮ . p_{i_{0}} \atop Δ + Γ_{1} + A_{i_{0}}}

Δ + Γ_{1} + Γ_{2}

2. the left introduction rule selects a formula which goes through the cut

\begin{matrix}\left[{⋮ . p_{i} \atop Δ + Γ_{1} + Π_{i∈I}A_{i} + A_{i}}\right] & i∈I \\ Δ + Γ_{1} + Π_{i∈I}A_{i} \end{matrix} \left[{⋮ . q_{j} \atop Δ + Γ_{2} + Σ_{x∈X}A_{x}^{⊥} + Π_{j∈J}B_{+}B_{j}}\right]_{j∈J}

Δ + Γ_{2} + Σ_{x∈X}A_{x}^{⊥} + Π_{j∈J}B_{j}
Δ + Γ_{1} + Γ_{2} + Π_{j∈J}B_{j}

reduces to

[\begin{matrix}\begin{matrix}\left[{⋮ . p_{i} \atop Δ + Γ_{1} + Π_{i∈I}A_{i} + A_{i}}\right] & i∈I \\ Δ + Γ_{1} + Π_{i∈I}A_{i} \end{matrix} & {⋮ . q_{j} \atop Δ + Γ_{2} + Σ_{x∈X}A_{x}^{⊥} + Π_{j∈J}B_{j} + B_{j}} \\ Δ + Γ_{1} + Γ_{2} + Π_{j∈J}B_{j} + B_{j} \end{matrix} ]_{j∈J}

Δ + Γ_{1} + Γ_{2} + Π_{j∈J}B_{j}

3. the proof on the left is ⊥

\begin{matrix}\left[{⋮ . p_{i} \atop Δ + Γ_{1} + Π_{i∈I}A_{i} + A_{i}}\right] & i∈I \\ Δ + Γ_{1} + Π_{i∈I}A_{i} \end{matrix}  {⊥ \atop Δ + Γ_{2} + Σ_{x∈X}A_{x}^{⊥} + Π_{j∈J}B_{j}}
Δ + Γ_{1} + Γ_{2}

reduced to

{⊥ \atop Δ + Γ_{1} + Γ_{2}}

Remark: The lower cut of the first rule performs a duplication of p_{i}. Both copies, when they select a name in Γ + Γ_{1} share the same “channel” in this Γ + Γ_{1}. Thus, applying the second rule (the one which pushs the introduction rules after the cuts) to each of both copies, leads to redundancies in Γ + Γ_{1}. This is the case even if the proofs were without redundancy at the beginning. This is why multiple occurrences of the same subformula are allowed in sequents and why we use names to distinguish between them.

Now, if we consider the cut between the partial Novikoff’s proof p =?i ↦^{Y} p_{i} and q

\begin{matrix}\left[{⋮ . p_{i} \atop Γ_{1} + Δ + Π_{i∈I}A_{i} + A_{j}}\right] & j∈J \\ Γ_{1} + Δ + Π_{j∈J}A_{j} \end{matrix}  {⋮ . q \atop Γ_{2} + Δ + Σ_{y∈Y} A_{y}^{⊥}}
Γ_{1} + Γ_{2} + Δ

then the weak-head cut-elimination is a strategy of reduction based on these reduction rules which repeatedly reduces the head redex until there is no more head redex. If the pattern on the right of the cut is itself a redex, this latter is reduced first.

A simplified representation of the successive steps of reduction is the following (B_{x_{0}} = Π_{j}C_{j}):

[figure: .; .; .; ⟹; Γ + B_{y}; Γ + Π_{y}B_{y}; Δ + Σ_{y}B_{y}^{⊥}; Λ + Σ_{y}B_{y}^{⊥}; Λ + C_{k}; Γ + Δ; Γ + B_{y_{0}}; Γ + B_{y}; .; .; .; Γ + Π_{y}B_{y}; Δ + Σ_{y}B_{y}^{⊥}; Λ + C_{k}; .; .; .; .; .; .; A_{i}; Π_{i}A_{i}; Σ_{x}A_{x}; ⟹... ⟹; ⟹...; Cuts; Γ + Δ + B_{y_{0}}^{⊥}; Γ + Δ + C_{k}; Γ + Δ; Cuts]

We use a natural semantics style to formally describe the weak-head cut-elimination. We use also proofs in term notation.

!x_{0}?j ↦^{Z} p_{j} ⟹^{w}!x_{0}?j ↦^{Z} p_{j}

⊥ ⟹^{w} ⊥

{q ⟹^{w}!x_{0}?k ↦^{T} q_{k} \atop Cut_{(X,σ)}(?y∈Y ↦^{Z} p_{y}, q) ⟹^{w}!x_{0}?k ↦^{T′} Cut_{(X,σ∪σ′)}(?y∈Y ↦^{Z} p_{y}, q_{k})} x_{0} ∉ Y

where T′ = New(T, X ∪ Rσ) and σ′ is the correspondence from T to T′

{q ⟹^{w} ⊥ \atop Cut_{(X,σ)}(?y∈Y ↦^{Z} p_{y}, q) ⟹^{w} ⊥}

q ⟹^{w}!y_{0}?k ↦^{T} q_{k} Cut_{(X′,σ′′)}(?z∈Z ↦^{T′} Cut_{(X,σ∪σ′)}(?y∈Y ↦^{Z} p_{y}, q_{z}), p_{y_{0}}) ⟹^{w} r

Cut_{(X,σ)}(?y∈Y ↦^{Z} p_{y}, q) ⟹^{w} r

y_{0} ∈ Y

where X′ = X ∪ Rσ, T′ = New(T, X′), σ′ is the correspondence from T to T′ and σ′′ the identity on X

3.3 Termination of the weak-head cut-elimination

Proposition 2 Let p and q be partial proofs respectively of Π_{i∈I}A_{i} and Σ_{x∈X}A_{x}^{⊥} such that (A_{i})_{i∈I} and (A_{x})_{x∈X} are in correspondence. If p is ?i∈I ↦^{Y} p_{i} then we have Cut(?x∈X ↦^{Y}

p_{x}, q) ⟹^{w} ⊥

We need to prove something stronger: the termination of the outermost reduction.

The outermost reduction is a complete reduction procedure extending recursively the weak reduction under introduction rules.

\begin{matrix}p ⟹^{w}!x_{0}?j ↦^{Z} p_{j} & ∀j ∈ J, p_{j} ⟹^{o} r_{j} \\ p ⟹^{o}!x_{0}?j ↦^{Z} r_{j} \end{matrix}

Lemma 1 If q′ and (p′_{y})_{y∈Y} are partial cut-free proofs such that Cut(?y∈Y ↦ p′_{y}, q′) is a correct proof then, for all q and (p_{y})_{y∈Y} such that q ⟹^{o} q′, for each y ∈ Y, p_{y} ⟹^{o} p′_{y}, there exists a partial cut-free proof r such that Cut(?y∈Y ↦ p_{y}, q) ⟹^{o} r Proof: By induction on Σ_{j∈J}A_{j}^{⊥} then by induction on q′

Proposition 3 If (p_{y})_{y∈Y} and q are partial cut-free proofs such that Cut(?y∈Y ↦ p′_{y}, q′) is a correct proof then there exists r such that Cut(?y∈Y ↦ p_{y}, q) ⟹^{o} r

Proof: Directly from the lemma by letting p′_{y} = p_{y} and q′ = q.

The proof of proposition 2 follows from the definition of ⟹^{o}.

4 The equivalence

4.1 Clean proofs

Let p^{0} =?i∈I ↦^{Y} p_{i}^{0} and q^{0} be partial Novikoff’s proofs respectively of Π_{i∈I}A_{i} and Σ_{x∈X}A_{x}^{⊥} such that (A_{i})_{i∈I} and (A_{x})_{x∈X} are in correspondence.

It happens that the proofs occurring during the weak reduction of Cut(?x∈X ↦^{Y} p_{x}^{0}, q^{0}) are all of the same shape. Let us call them clean proofs.

• a partial Novikoff’s proof is a clean proof. Such a clean proof is called a leaf.

• if (p_{y})_{y∈Y} is a family of clean proofs and q a clean proof, then Cut(?y∈Y ↦ p_{y}, q) is a clean proof

Therefore, a clean proof is a tree of cut rules with partial Novikoff’s proof at the leaves. Several simple notions about the structure of clean proofs are needed. We use a special symbol α to express occurrences of cut nodes in a clean proof p. The root

occurrence is denoted by ϵ and if a node Cut(?y∈Y ↦ p_{y}, q) has occurrence w in p then q has occurrence wα and p_{y} has occurrence wy.

The rightmost branch (the ?-free branch) of a clean proof is called the main branch of the clean proof. More generally, if w is the occurrence of a cut node in p then the main branch B_{w}(p) of p at w is the branch starting from the root of p and ending with the main branch of the right subproof at node w. With this notation, the main branch is B_{ϵ}(p). A branch is referred by the occurrence of its leaf. Thus B_{ϵ} is something like α^{m} and B_{w} is something like wα^{m}.

If a cut node at occurrence w is on a branch B (i.e. if w is a proper initial segment of B), then S_{B}(w) denotes the immediate successor of this node on B.

If a leaf of a clean proof proves a sequent Σ_{x∈X}A_{x} then any x ∈ X can be traced through the net of cut nodes, possibly renamed by the renaming maps. Either it goes through until the root or it is captured by a cut node.

The line of a branch in a clean proof is the line of the partial Novikoff’s proof at the leaf of this branch. The line of a clean proof is the occurrence of the partial Novikoff’s proof (as a subproof of p^{0} or q^{0}) that we encounter at the leaf of the main branch.

4.2 Trace

Let a be a deduction of Cut(?y∈Y ↦ p_{y}, q) ⟹^{w} r.

By induction on a, we define the trace T r(a) of a. The trace is a finite sequence of clean proofs characterizing a. The empty trace is written []. The trace is the reading of a (understood as a tree) in a left-first depth-first way.

T r(!x_{0}?j ↦^{Z} p_{j} ⟹^{w}!x_{0}?j ↦^{Z} p_{j}) = T r(⊥ ⟹^{w} ⊥) = []

If T r(a′) = r′_{1}...r′_{n} then

T r(\begin{matrix}{⋮ . a′ \atop q ⟹^{w}!x_{0}?k ↦^{T} q_{k}} & x_{0} ∉ Y \\ Cut_{(X,σ)}(?y∈Y ↦^{Z} p_{y}, q) ⟹^{w}!x_{0}?k ↦^{T′} Cut_{(X,σ∪σ′)}(?y∈Y ↦^{Z} p_{y}, q_{k}) \end{matrix} ) = r_{1}...r_{n}

where r_{i} = Cut_{(X,σ)}(?y∈Y ↦^{Z} p_{y}, r′_{n}).

Similarly, if T r(a′) = r′_{1}...r′_{n} then

T r( {⋮ . a′ \atop q ⟹^{w} ⊥} ; Cut_{(X,σ)}(?y∈Y ↦^{Z} p_{y}, q) ⟹^{w} ⊥ ) = r_{1}...r_{n}

where r_{i} = Cut_{(X,σ)}(?y∈Y ↦^{Z} p_{y}, r′_{n}).

If T r(a′) = r′_{1}...r′_{n′} and T r(a′′) = r′′_{1}...r′′_{n′′} then

T r(\begin{matrix}{⋮ . a′ \atop q ⟹^{w}!y_{0}?k ↦^{T} q_{k}} & {⋮ . a′′ \atop Cut(?z∈Z ↦^{T′} Cut(?y∈Y ↦^{Z} p_{y}, q_{z}), p_{y_{0}}) ⟹^{w} r} & y_{0} ∈ Y \\ & Cut(?y∈Y ↦^{Z} p_{y}, q) ⟹^{w} r \end{matrix} ) = r_{1}...r_{n′}pr′′_{1}...r′′_{n′′}

where r_{i} = Cut(?y∈Y ↦^{Z} p_{y}, r′_{n}) and p = Cut(?z∈Z ↦^{T′} Cut(?y∈Y ↦^{Z} p_{y}, q_{z}), p_{y_{0}}) (seen as a clean proof)

The trace is the sequence of the elementary steps of reduction which constitute the complete weak-head cut-elimination. This is justified by the next lemma.

Lemma 2 Let r_{n} be the n^{th} element of the trace. Let q be the partial Novikoff’s proof at the leaf of B_{ϵ}(r_{n}). We suppose that q =!x_{0}?j ↦^{T} q_{j}. Then there is exactly one cut node capturing x_{0} on B_{ϵ}(r_{n}) and

[figure: ?x∈X; Cuts; Cuts; ?x∈X; ?y∈Y; p_{x}; p_{x}; p_{x_{0}}; q =!x_{0}?j ↦^{T} q_{j}; q_{y}; r_{n} =; r_{n+1} =]

Proof: By construction of the trace.

4.3 Conformity

The trace contains all the information to get the lines of the debate (therefore the debate). This is expressed by the property of conformity.

Let p be a clean proof, w the occurrence of a cut node in it and l_{0}...l_{n} the lines of a certain debate (f_{1}, u_{1})...(f_{n}, u_{n}). We assume that the sequence of lines may also be empty.

p conforms to l_{0}...l_{n} at w if

• either the sequence is empty and there is no capturer on B_{w}(p)

• or the proof at the leaf of B_{w}(p) is q proving Σ_{x∈X}A_{x}, its line is exactly l_{n} = u_{n_{1}}...u_{n_{k}} and for all x ∈ X, the occurrence corresponding to A_{x} is a direct extension of one of the u_{n_{i}} and x is captured at w′ on B_{w}(p) such that p conforms to l_{0}...l_{n_{i}} at w′

p is conform to the lines l_{0}...l_{n} of a given debate if p conforms to l_{0}...l_{n} at the root.

Proposition 4 Let p and q be partial Novikoff’s proofs respectively of Π_{i∈I}A_{i} and Σ_{x∈X}A_{x}^{⊥} such that (A_{i})_{i∈I} and (A_{x})_{x∈X} are in correspondence.

If r_{0} = Cut(?x∈X ↦ p_{x}, q) and r_{1}...r_{N} is the trace of the derivation of r_{0} ⟹^{w} ⊥ and l_{0}...l_{N′} are the lines of the debate between p and q, then N = N′ and for all 0 ≤ n ≤ N, we have that r_{n} conforms to l_{0}...l_{n}.

Proof:

By induction on the length of the trace.

The base case is just checking. r_{0} effectively conforms to l_{0}. The line of the main branch of r_{0} is effectively <>. q may only select an x_{0} ∈ X and the cut effectively captures x_{0}. The remaining branch is effectively capturer-free.

Between r_{n} and r_{n+1} the main change consists in the addition of an extra cut node capturing the answers to u_{n}. This change shifts some of the other cut nodes but do not disturb the structure of capturers.

Corollary 1 The sequence of lines of the main branches of r_{0}...r_{N} is exactly the sequence l_{0}...l_{N}.

Conclusion

The game-theoretic interpretation of Novikoff’s proof is quite attractive for its simplicity and the weak cut-elimination may look complicated in comparison with the debate. The introduction of names in order to answer the problem of contractions appearing during the reduction entails a complex machinery. In fact, the debate stays simple to express because we are only interested in its termination. If we would like to generalize the debate in order to obtain effective cutfree proofs, the problem of redundancy genesis would also occur. But any cut-free proof with redundancies may be transformed into a Novikoff’s proof by postponing the redundancy further and further until it collapses at the level of an axiom. Also, an alternative is to remove redundancies at the time when they are generated.

The debate needs a quite simple structure. Therefore the equivalence with the weak cutelimination gives to the latter a special status.

References

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

[2] 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.

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