Subnets of Proof-nets in MLL^{−}

G. Bellin ^{∗}  J. van de Wiele

December 21, 1994

Abstract

The paper studies the properties of the subnets of proof-nets. Very simple proofs are obtained of known results on proof-nets for MLL^{−}, Multiplicative Linear Logic without propositional constants.

Contents

1 Preface 1

2 Proof Nets for Propositional MLL^{−} 3 2.1 Propositional Proof Structures and Proof Nets . . . . . . . . . . 3 2.2 Subnets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Empires and Kingdoms: Existence and Properties . . . . . . . . 8 2.4 Sequentialization Theorem . . . . . . . . . . . . . . . . . . . . . 12 2.5 Permutability of Inferences in the Sequent Calculus . . . . . . . 13

3 Proof Nets for First Order MLL^{−} 15 3.1 First-Order Proof-Structures . . . . . . . . . . . . . . . . . . . . 15 3.2 Subnets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.3 Empires and Kingdoms: Existence and Properties . . . . . . . . 19 3.4 Sequentialization . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.5 Permutability of Inferences in the Sequent Calculus . . . . . . . 21

1 Preface

The theory of proof-nets for MLL^{−}, multiplicative linear logic without the propositional constants 1 and ⊥, has been extensively studied since Girard’s fundamental paper [5]. The improved presentation of the subject given by Danos and Regnier [3] for propositional MLL^{−} and by Girard [7] for the first-order case has become canonical: the notions are defined of an arbitrary proof-structure and of a ‘contex-forgetting’ map ( . )^{−} from sequent derivations to proof-structures which preserves cut-elimination; correctness conditions are given that characterize proof-nets, the proof-structures R such that R = (D)^{−}, for some sequent calculus derivation D. Although Girard’s original correctness condition is of an exponential computational complexity over the size of the proof-structure, other correctness conditions are known of quadratic computational complexity.

∗Research supported by EC Individual Fellowship Human Capital and Mobility, contract n. 930142

A further simplification of the canonical theory of proof-nets has been obtained by a more general classification of the subnet of a proof-net. Given a proof-net R and a formula A in R, consider the set of subnets that have A among their conclusions, in particular the largest and the smallest subnet in this set, called the empire and the kingdom of A, respectively. One must give a construction proving that such a set is not empty: in Girard’s fundamental paper a construction of the empires is given which is linear in the size of the proof-net. When the notion of kingdom is introduced, the essential properties of proof-nets – including the existence of a sequent derivation D such that R = (D)^{−} (Theorem 1, sequentialization theorem) – can be easily proved using simple properties of the kingdoms and empires, in particular the fact that the relation X is in the kingdom of Y is a strict ordering. ^{1}

Moreover the map ( . )^{−} identifies equivalence classes of sequent derivations, where D_{i} and D_{j} are equivalent if they differ only for permutations of inferences. Now consider the set of derivations B which have A as a conclusion, and that are subderivations of some derivation D_{i} in an equivalence class. The kingdom and the empire of a formula A in the proof-net (D_{i})^{−} yield the notions of the minimum and the maximum, respectively, in such a set of subderivations (Theorem 2). This fact gives evidence that the notions is question do not depend on accidental features of the representation; therefore satisfactory generalizations of our results to larger fragments or to other logics should include Theorem 2.

Such a generalization is impossible in any logic with any form of Weakening, e.g., in the fragment MLL of multiplicative linear logic with the rule for the constant ⊥. Indeed a minimal subderivation in which a formula A may be introduced by Weakening is an axiom; but the process of permuting Weakening upwards in a derivation is non-deterministic and does not always identify a unique axiom as the minimum in our set of subderivations; hence in such a logic we cannot have a meaningful notion of kingdom.

1The notion of kingdom and the discovery of its properties originated in the Équipe de Logique in the winter 1991-92 and appeared in discussions through electronic mail involving Danos, Girard, Gonthier, Joinet, Regnier, (Paris VII), Gallier and de Groote (University of Pennsylvania) and the author (University of Edinburgh).

2 Proof Nets for Propositional MLL^{−}

We give a simple presentation of the well-known basic theory of proof nets for Multiplicative Linear Logic without propositional constants (MLL^{−}). The main novelty is the use of the structural properties of subnets of a proof-net, in particular the tight relations between kingdoms and empires. A pay-off is a simple and elegant proof of the following theorems:^{2}

Theorem 1. There exists a “context-forgetting” map ( . )^{−} from sequent derivations in MLL ^{−} to proof nets for MLL ^{−} with the following properties:

(a) Let D be a derivation of Γ in the sequent calculus for MLL ^{−}; then (D)^{−} is a proof net with conclusions Γ.

(b) (Sequentialization) If R is a proof net with conclusions Γ for MLL ^{−}, then there is a sequent calculus derivation D of Γ such that R = (D)^{−}.

(c) If D reduces to D′, then D^{−} reduces to (D′)^{−}.

(d) If D^{−} reduces to R′ then there is a D′ such that D reduces to D′ and R′ = (D′)^{−}.

Theorem 2. (Permutability of Inferences) (i) Let D and D′ be a pair of derivation of the same sequent ⊢ Γ in propositional MLL ^{−}. Then (D)^{−} = (D′)^{−} if and only if there exists a sequence of derivations D = D_{1}, D_{2}, …, D_{n} = D′ such that D_{i} and D_{i+1} differ only for a permutation of two consecutive inferences.

(ii) Let R be a proof-net and let A be a formula occurrence in R. Then there exists a derivation D with (D)^{−} = R and a subderivation B of D such that (B)^{−} = eA. A similar statement holds for kA.

2.1 Propositional Proof Structures and Proof Nets

A link is an m+n-ary relation between formula occurrences, for some m, n ≥ 0, m + n ≠ 0. Suppose X_{1},…, X_{m+n} are in a link: if m > 0, then X_{1}, …, X_{m} are called the premises of the link; if n > 0, then X_{m+1}, …, X_{m+n} are called the conclusions of the link. If m = 0, the link is called an axiom link.

2Here we prove part (a) and (b) of Theorem 1; the proof of parts (c) and (d) are clear from [5, 7].

Links are graphically represented as

\frac{X_{1}, …, X_{m}}{X_{m+1}, …, X_{m+n}}

We consider links of the following forms:

Identity Links:

axiom links: \overline{A A^{⊥}} cut links: \frac{A A^{⊥}}{cut}

Multiplicative Links:

times links: \frac{A B}{A ⊗ B}  par links: \frac{A B}{A℘B}

Convention. We assume that the logical axioms and cut links are symmetric relations. Other links are not regarded as symmetric. The word “cut” in a cut link is not a formula, but a place-holder; following common practice, we may sometimes omit it.

Definitions 1. (i) A proof structure S for propositional MLL^{−} consists of (i) a nonempty set of formula-occurrences together with (ii) a set of identity links, multiplicative links satisfying the properties:

1. Every formula-occurrence in S is the conclusion of one and only one link;

2. Every formula-occurrence in S is the premise of at most one link.

We write X ≺ Y if X is a hereditary premise of Y; in this case we also say that ‘X is above Y ’. We shall draw proof structures in the familiar way as non-empty, not necessarily planar, graphs.

(ii) We define the following reductions on propositional MLL^{−} proof structures:

Axiom Reductions

⋮  ⋮
X  X^{⊥} X  reduces to X
⋮  ⋮

Symmetric Reductions

⋮_{1}  ⋮_{2}  ⋮_{3}  ⋮_{4}  ⋮_{1}  ⋮_{3}  ⋮_{2}  ⋮_{4}
X  Y  X^{⊥} Y^{⊥}  X  X^{⊥}  Y  Y^{⊥}
X ⊗ Y  X^{⊥}℘Y^{⊥}  reduces to

Definitions 2. Let R be a propositional proof structure for MLL^{−}.

(i) A Danos-Regnier switching s for R consists in the choice for each par link L in R of one of the premises of L.

(ii) Given a switching s for R, we define the undirected Danos-Regnier graph s(R) as follows:

• the vertices of s(R) are the formulas of R;

• there is an edge between vertices X and Y exactly when:

1. X and Y are the conclusions of a logical axioms or the premises of a cut link; or

2. X is a premise and Y the conclusion of a times link; or else

3. Y is the conclusion of a par and X is the occurrence selected by the switching s.

Definition 3. Let R be a multiplicative proof-structure. R is a proof-net for propositional MLL^{−} if for every switching s of R, the graph s(R) is acyclic and connected (i.e., an undirected tree).

2.2 Subnets

Definitions 4. Let m : S → R be any injective map of MLL^{−} proof structures (regarded as sets of formula occurrences) such that X and m(X) are occurrences of the same formula.

(i) We say that m preserves the links if for every L in S there is a link L′ in R of the same kind such that

L : \frac{X_{1}, …, X_{k}}{X_{k+1}, … X_{k+n}}  ↦  L′ : \frac{mX_{1}, …, mX_{k}}{mX_{k+1}, … mX_{k+n}}

(ii) A proof-structure S is a substructure of a proof-structure R if there is an injective map ι : S → R preserving links. If S is a substructure of R, then the lowermost formula occurrences of S are also called the doors of S.

(iii) We write stΣ for the smallest substructure of R containing Σ.

(iv) A subnet is a substructure which satisfies the condition of proof-nets.

Remark. In definition 4.(ii) let ι be the identity map. A subset S of R (with the links of R holding among the occurrences in S) is a substructure if and only if

(1) S is closed under hereditary premises and

(2) if \overline{X_{0} X_{1}} is an axiom and X_{i} ∈ S then X_{1−i} ∈ S.

In particular, the set of formula occurrences in st(Σ) consists of Σ, of all the hereditary premises of Σ and of the axioms above them:

st(Σ) = ⋃_{Z∈Σ}\{X : X ⪯ Z\} ∪ ⋃_{Z∈Σ}\{X ∈ \overline{X Y} : Y ⪯ Σ\}.

Lemma 1. Let R_{1} and R_{2} be subnets of the proof net R. Then (i) S = R_{1} ∪ R_{2} is a subnet if and only if R_{1} ∩ R_{2} ≠ ∅.

(ii) If R_{1} ∩ R_{2} ≠ ∅ then R_{0} = R_{1} ∩ R_{2} is a subnet.

Proof. Let R be a proof net and R′ any substructure. Given a switching s′ for R′, extend s′ to a switching s for R; then s′R′ is a subgraph of sR, hence s′R′ is acyclic, since sR is. Therefore we need only to consider the connectedness of sS and sR_{0}.

To prove (i), assume R_{1} and R_{2} are subnets with nonempty intersection and fix a switching s for S = R_{1} ∪ R_{2}. For i = 1, 2 let sR_{i} be the restriction of sR to R_{i}; then sR_{i} is connected since R_{i} is a subnet. Let A be in R_{1} and B in R_{2}; if C ∈ R_{1} ∩ R_{2}, then A is connected with C since sR_{1} is connected and B is connected with C since sR_{2} is connected, hence A is connected with B as required. The converse is immediate, namely, if R_{1} ∩ R_{2} = ∅, then any Danos-Regnier graph on R_{1} ∪ R_{2} is disconnected.

To prove (ii), let s_{0} be a switching for R_{0} = R_{1} ∩ R_{2}; let s_{1}, s_{2} be extensions of s_{0} to R_{1}, R_{2}, respectively; then s = s_{1} ∪ s_{2} is a switching of R_{1} ∪ R_{2}. If A and B occur in R_{0}, then they are connected by a path π_{1} in s_{1}R_{1} and by a path π_{2} in s_{2}R_{2}; if π_{1} ≠ π_{2}, then there is a cycle in sS, which is impossible. But π_{1} = π_{2} means that A and B are connected in s_{0}R_{0}.

Proposition 1: (i) Let R_{1} and R_{2} be proof nets and let

S = Times (R_{1}, R_{2}) = \frac{{R_{1} \atop A} {R_{2} \atop B}}{A ⊗ B} or S = Cut (R_{1}, R_{2}) = \frac{{R_{1} \atop A} {R_{2} \atop A^{⊥}}}{cut}

Then S is a proof net if and only if R_{1} ∩ R_{2} = ∅.

(ii) Let R_{0} be a substructure of the proof net R and let

S = Par (R_{0}) = R_{0} ; \frac{A_{1} A_{2}}{A℘B}

Then S is a subnet if and only if R_{0} is a subnet.

Proof. (i) Let s be a switching of S = Times (R_{1}, R_{2}); since R_{1} and R_{2} are proof nets, each of the graphs sR_{1} and sR_{2} are acyclic and connected; in addition to sR_{1} ∪ sR_{2}, sS has the vertex A ⊗ B and two edges (A, A ⊗ B) and (B, A ⊗ B), which establish a connection between sR_{1} and sR_{2}; this is the only connection since R_{1} and R_{1} are disjoint. Conversely, if R_{1} ∩R_{2} ≠ ∅, then by lemma 1.(i) R_{1} ∪R_{2} is a subnet. Therefore given any switching s of S, the nodes A and B in are connected already in s(R_{1} ∪ R_{2}); also the edges along link \frac{A B}{A⊗B} yield another connection between the vertices A and B, hence there is a cycle in sS. Part (ii) is immediate: for any switching s of R, sS comes from sR_{0} by introducing an additional edge (A_{i}, A_{1}℘A_{2}) to a leaf A_{i}, where A℘B is a new leaf.

By induction on the definition of a sequent derivation in MLL^{−} we define the map ( . )^{−} from sequent derivations to proof structures (“forgetting the context”).

Theorem 1.(a) Let D be a derivation in the sequent calculus for MLL ^{−}; then (D)^{−} is a proof net.

Proof. Axioms are proof nets, and the property of being a net is preserved under the times, cut and par rules by Proposition 1.

Definitions 5. Let Σ be a set of formula-occurrences in a proof-net R.

(i) The territory tΣ of is the smallest subnet of R including Σ (not necessarily as doors). (ii) The kingdom kA [the empire eA] of a formula-occurrence A in a proof-net R is the smallest [the largest] subnet of R having A as a door. (iii) Let X ≪ Y =_{df} X ∈ kY.

Remarks. (i) Given a proof-net R and formula occurrences Σ in R, the subnet tΣ always exists by Lemma 1. (ii) Suppose for no X, Y in Σ we have that X is a hereditary premise of Y (X ≺ Y). Then stΣ, the smallest substructure containing Σ, has all the occurrences in Σ among its doors. On the other hand, there may not be a subnet having all of Σ among its doors. (iii) The existence of kA and eA is immediate by Lemma 1 once we prove there exists a subnet having A as a door. This can be done by giving an explicit construction of eA as in [5, 7] and in the following section.

2.3 Empires and Kingdoms: Existence and Properties

Among the results in this section, for the proof of the Sequentialization theorem we need only the fact that for each formula occurrence A in a proof-net R there exists a subnet having A as a door.

Definition 6. Let A be a formula occurrence in the proof net R. For a given D-R-switching s, let s(R, A) be (the set of formula occurrences and of links occurring in) the connected component of the graph sR which is obtained as follows:

• if A is a premise of a link in R with conclusion Z and there is an edge (A, Z) in the D-R-graph sR, then remove (A, Z) and let s(R, A) be the component containing the vertex A.

• otherwise, let s(R, A) be sR.

We write \overline{s(R, A)} for the connected component not containing A after the removal of the edge (A, Z) from sR, if such an edge exists; \overline{s(R, A)} is empty otherwise.

Definition 7. Let R be a proof-net and let Σ be a set of formula-occurrences in R. We write path_{s}(Σ) for the smallest subgraph of sR connecting all formulaoccurrences in Σ. Clearly path_{s}(A, B) is a path of sR, for every A, B in R and every switching s for R.

Proposition 2. (Characterizartions of empires; cf. [3, 5, 7]) Let R be a proof net. Then e(A) (the largest subnet of R containing A as a conclusion) exists and is characterized by the following equivalent conditions:

(a) ⋂_{s} s(R, A), where s varies over all possible switchings;

(b) the smallest set of formula occurrences in R closed under the following conditions:

(i) A ∈ e(A);

(ii) if \frac{X_{1} X_{2}}{Y} is a link in S and Y ∈ e(A), then X_{1}, X_{2} ∈ e(A), (↑-step);

(iii) if \overline{X_{0} X_{1}} is an axiom in S and X_{i} ∈ e(A), then X_{1−i} ∈ e(A) (→-step);

(iv) if \frac{X_{1} X_{2}}{X_{1}⊗X_{2}} is a link in S, and for i = 1 or 2 X_{i} ≠ A and X_{i} ∈ e(A), then X_{1} ⊗ X_{2} ∈ e(A) (↓-step); (v) if \frac{X_{1} X_{2}}{X_{1}℘X_{2}} is a link in S, X_{1} ≠ A ≠ X_{2} and \{X_{1}, X_{2}\} ⊂ e(A), then X_{1}℘X_{2} ∈ e(A) (⇓-step).

(According to our conventions, X_{i} ≠ A means that X_{i} and A are different formula occurrences.)

Proof. The following proof of (a) = (b) follows the argument in [7]. To show that (b) ⊆ (a) we show that the set (a) is closed under the conditions (i) − (v) defining (b). This is easy for clauses (i), (iii), (iv) and (v) of (b), and also for clause (ii), if the link in question is a times link. Now suppose that for some par link L the conclusion X_{1}℘X_{2} ∈ ⋂_{s} s(R, A), but, say, for the premise X_{2} we have X_{2} ∉ ⋂_{s} s(R, A). Then for some s we have that X_{1}℘X_{2} belongs to s(R, A) and X_{2} does not. Therefore A is premise of a link with conclusion Z and X_{2} belongs to the same connected component as Z, i.e., to \overline{s(R, A)}; let π be path_{s}(X_{2}, Z), the path connecting X_{2} and Z in \overline{s(R, A)}. Since the switching s in L is Left and the edge (X_{1}, X_{1}℘X_{2}) belongs to s(R, A), it plays no role in the connections π between X_{2} and Z. Therefore if s′ is like s, except that the switch on L is changed from Left to Right, then we still have a connection π between X_{2} and Z; since X_{1}℘X_{2} ∈ ⋂_{s} s(R, A), π can be extended to a connection path_{s′}(A, Z), between A and Z in s′(R, A); but then in s′A we have a cycle, and this is a contradiction. Therefore {X_{1}, X_{2}} ⊂ eA.

To show that (a) ⊆ (b) we consider a principal switching s for A: this is a switching such that for every par link L, if a premise X_{i} of L is in (b), but the conclusion X_{0}℘X_{1} is not, then s chooses X_{1−i}. We claim that if s is a principal switching, then s(R, A) is precisely (b).

Notice that any set S closed under clauses (i) − (v) has the property that if S contains X, then it contains also every formula occurrence Z such that X and Z are in a link L, in all cases except perhaps the following:

(1) X is A and a premise of L, while Z is the conclusion of L;

(2) L is a par link, X is a premise and Z the conclusion of L, and the other premise Y is not it S.

It follows that the set (b) is a substructure of R whose doors can only be conclusions of R, or cuts, or occurrences X as in (1) or (2).

Now suppose a formula-occurrence W is in (a) but not in (b); choose a switching s principal for A. Since s(R, A) is connected and (b) is a substructure, the path π connecting A with W in s(R, A) must exit (b) from a door X as in cases (1) or (2). But this is impossible by the definition of principal switching and of s(R, A). Hence (a) ⊆ (b) as claimed.

We must show that A is a door of the substructure equivalently defined by (a) and (b). Let Z ∈ ⋂_{s} s(R, A) and suppose A ≺ Z. Choose a switching s such that if \frac{X_{0} X_{1}}{X_{0}℘X_{1}} is a link such that A ⪯ X_{i} ≺ Z, then s chooses X_{1−i}.

We claim that there must be a times link \frac{B C}{B ⊗ C} in s(R, A) such that, say,

A ⪯ C ≺ Z: otherwise, Z ∉ s(R, A), by the choice of s and the definition of s(R, A). Thus let L be the uppermost such link: then the path π connecting A and B in s(R, A) does not pass through C; but then in sR we have two distinct paths connecting A and B, and this contradicts the acyclicity of sR.

Since (b) is a substructure satisfying the condition (a), for each s the restriction of s(R, A) to (b) is acyclic and connected, hence (b) is a subnet. We have proved that given a proof-net R and a formula-occurrence A in R, a subnet with conclusion A always exists.

But (a) is also the largest among such subnets: let S be a substructure of R with A as a door and suppose Z ∈ S \ (a); then for some s, we have Z ∉ s(R, A), from which it follows that no path connects A and Z in sS; hence S is not a subnet. We conclude that e(A) = (a) = (b).

The construction of a principal switching was given first in Girard’s Trip Theorem (cf. [5], 2.9.5.); using Girard’s notion of a trip the principal switching constructed ‘dynamically’, by making the following choices during a trip.

Starting from A, the trip proceed upwards in R, and at a branching point, i.e., at times link, we choose arbitrarily;

• if the trip reaches a par link for the first time from below, then we fix s arbitrarily and the trip continues to the chosen premise;

• if the trip reach a par link for the first time from a premise, then we let s choose the other premise.

The Trip Theorem shows that eA is exactly the set of occurrences visited between the first and the second visit to A. The algorithm is transfered to our setting using the correspondence between trips and D-R-graphs established by Danos and Regnier [3]. One advantage of such a formulation is that the following corollary becomes completely obvious.

Corollary. The complexity of the computation of eA is linear on the size of the proof-net.

Proposition 3.(I) (properties of territories). Let R be a proof-net and let Σ be a set of occurrences in R. Then the territory tΣ satisfies

tΣ = t(path_{s}(Σ)) = ⋃_{X∈path_{s}(Σ)} tX

Subnets of proof-nets in MLL^{−} 11

for any switching s. Proposition 3.(II) (characterizations of kingdoms).^{3} Let R be a proof net. Then the kingdom kA of A in R (the smallest subnet of R having A as a conclusion), exists and is characterized by the following equivalent conditions:

(a) tA;

(b) the smallest set satisfying the following conditions (Danos et al.): (o) A ∈ kA.

(i) Let \overline{X X^{⊥}} occur in R. Then \overline{X X^{⊥}} = kX = t(X, X^{⊥}) = kX^{⊥}.

(ii) Let L : \frac{A B}{A ⊗ B} be a link in R. Then

kX ⊗ Y = kX ∪ kY ∪ {X ⊗ Y }.

(iii) Let L : \frac{X Y}{X℘Y} be a link in R. Then

kX℘Y = ⋃{kC|C ∈ path_{s}(X, Y)} ∪ {X℘Y }

for any switching s.

(c) the smallest set of formula occurrences closed under the following conditions:

(i) A ∈ k(A);

(ii) if \frac{X_{1} X_{2}}{Y} is a link in S and Y ∈ k(A), then X_{1}, X_{2} ∈ k(A) [similarly, if \frac{X[t/y]}{∃y.X} is a link in S and ∃y.X ∈ k(A), then X[t/y] ∈ k(A)] (↑-step);

(iii) if \overline{X_{0} X_{1}} is an axiom in S and X_{i} ∈ k(A), then X_{1−i} ∈ k(A) (→-step); (iv) if \frac{...X...}{Y} is a link in S X ≠ A ≠ Y, X ∈ k(A), then Y ∈ kA iff A ∉ eX

(↓-step).

The proof is left to the reader; for case (c)(iv), see the following Lemma 2.

3Characterization (b) is due to Danos and others, as specified in footnote 1. Characterization (c) was suggested to us by J-Y. Girard.

2.4 Sequentialization Theorem

Lemma 2. (Empire-Kingdom Nesting) Let L_{1} : \frac{...A...}{C} and L_{2} : \frac{...B...}{D} be distinct links in a proof net R for MLL ^{−}. Suppose B ∈ eA; then D ∉ eA if and only if C ∈ kD.

Proof. Clearly B ∈ eA ∩ kD, hence R_{0} = eA ∩ kD and S = eA ∪ kD are subnets of R. If C ∉ kD and D ∉ eA, then S is a subnet with conclusion A, which is larger than eA, since it contains D: this contradicts the definition of the empire of A. If C ∈ kD and D ∈ eA, then R_{0} is a subnet with conclusion D, which is smaller than kD since it does not contain C: this contradicts the definition of the kingdom of D.

Lemma 3. (Kingdom Ordering) (i) Let R be a proof net and let X, Y occur in R. If X ≪ Y and Y ≪ X then either X and Y are the same occurrence or they occur in an axiom \overline{X Y} of R. (ii) Hence ≪ is an ordering of the conclusions of non-axiom links.

Proof. For an axiom A = \overline{X X^{⊥}} we have kX = A = kX^{⊥}. Otherwise, let X ∈ kY, with X and Y distinct; if also Y ∈ kX, then kY ∩ kX is a subnet, and necessarily kX = kX ∩ kY = kY.

If X is X_{1}℘X_{2} in a link L: \frac{X_{1} X_{2}}{X_{1}℘X_{2}} then the result of removing X and L from

kY is still a subnet, and this contradicts the definition of kY.

If X is X_{1} ⊗ X_{2} in a link \frac{X_{1} X_{2}}{X_{1} ⊗ X_{2}} then clearly kX = k(X_{1}) ∪ k(X_{2}) ∪ \{X\},

hence for i = 1 or 2, Y ∈ k(X_{i}); but by Lemma 2, Y is not even in e(X_{i}).

Theorem 1.(b) (Sequentialization) If R is a proof net with conclusions Γ, then there is a sequent calculus derivation D of Γ such that R = (D)^{−}.

Proof. By induction on the size of R. If R is an axiom, then D is an axiom sequent. If one of the lowermost links is a par or for all link, then we remove such a link, we apply the induction hypothesis to the resulting subnet and we conclude by applying a suitable par inference. Now suppose that all the conclusions of R are conclusions either of an axiom or of a times link: we choose a terminal times link L whose conclusion X = A_{i} ⊗ B_{i} is maximal w.r.t. ≪. In this case eA_{i} and eB_{i} split R \ {A_{i} ⊗ B_{i}}. Suppose not; then there is a link L : \frac{...D...}{C} such that, say, D ∈ eB_{i} and C ∉ eB_{i}. But C occurs at or above another conclusion Y = A_{j} ⊗B_{j}. By the lemma 2 X = A_{i} ⊗B_{i} ∈ kC; also C ∈ kY hence kC ⊂ kY; thus we obtain X ∈ kY, contradicting the choice of X.

Remark. The computational complexity of Girard’s no-short-trip condition and of Danos-Regnier’s requirement that all D-R-graphs be acyclic and connected is clearly exponential on the size of the given proof-structure. It is known (see, e.g., [3, 4, 1]) that there are procedures to decide whether or not a proof-structure R for MLL^{−} is a proof-net in time quadratic over the cardinality of R.

2.5 Permutability of Inferences in the Sequent Calculus

Given a derivation D and two formula-occurrences X_{1} and X_{2} in some sequents of D, if X_{1} is an ancestor of X_{2} then certainly the inference introducing X_{1} must occur above the inference introducing X_{2}. We are concerned with occurrences X_{1} and X_{2} in D such that neither one is an ancestor of the other. Suppose X_{1} is introduced above X_{2} in D, we ask whether there is a derivation D′ which is obtained from D by successive permutation of the inferences and such that X_{1} is introduced below X_{2} in D′.

Counterexample. The following is a derivation in MLL^{−} in which the applications of the ⊗-rule and of the ℘-rule cannot be permuted.

⊢ P^{⊥}, P ⊢ Q, Q^{⊥} ⊗

⊢ P^{⊥}, P ⊗Q, Q^{⊥}

exchange

⊢ Q^{⊥}, P^{⊥}, P ⊗Q ℘

⊢ Q^{⊥}℘P^{⊥}, P ⊗Q

Remark. In the sequent calculus for propositinal MLL^{−} ⊗/℘, cut/℘ and ∃/∀ are the only exceptions to the permutability of inferences where neither one of the principal formulas is an ancestor of the other.

A full characterization of permutability of inference in MLL^{−} is obtained using the ‘context-forgetting’ map ( .)^{−} of derivations into proof-nets and the notions of empire and kingdom. Such a map uniquely associates each inference I in D other than Exchange with a link L in (D)^{−} and the principal formula(s) of I with the conclusion(s) of L.

Theorem 2. (i) Let D and D′ be a pair of derivation of the same sequent ⊢ Γ in propositional MLL ^{−}. Then (D)^{−} = (D′)^{−} if and only if there exists a sequence of derivations D = D_{1}, D_{2}, …, D_{n} = D′ such that D_{i} and D_{i+1} differ only for a permutation of two consecutive inferences.

(ii) Let R be a proof-net and let A be a formula occurrence in R. Then there exists a derivation D with (D)^{−} = R and a subderivation B of D such that (B)^{−} = eA. A similar statement holds for kA.

Proof. (i) The “if” part is clear. To prove the “only if” part, let (D)^{−} = R = (D′)^{−}; consider a branch of D and let I_{0} the last inference from bottom up where D agrees with D′. If I_{0} is an axiom, then D and D′ entirely agree in the order of inferences in this branch. Otherwise, let I_{A} be the inference immediately above I_{0} in the branch of D under consideration, and let I′_{A} be the inference of D′ such that the principal formulas of I_{A} and I′_{A} are mapped to the same formula occurrence A of R: such an I′_{A} exists, since (D)^{−} = (D′)^{−}.

Moreover, let I′_{1}, …, I′_{k} be the inferences which occur in D′ between I′_{A} and I_{0} (proceeding downwards). Notice that if the principal formula of any I′_{i} for i ≤ k is mapped to a formula B of R, then the inference I_{B} of D whose principal formula is mapped to B also occurs above the inference I_{0}, by our assumption that D and D′ agree in the given branch up to I_{0}. It follows that no descendant of A is active in I′_{1}, …, I′_{k}.

If the inference I′_{A} is an instance of the par rule, then clearly it can be permuted below I′_{1}, …, I′_{k}. If I′_{A} is a times rule, say, A is A_{1} ⊗ A_{2}, then we have

I_{A} : \begin{matrix}B_{1} ; ⋮ . ; ⊢ Γ_{1}, A_{1} & B_{2} ; ⋮ . ; ⊢ Γ_{2}, A_{2} \\ ⊢ Γ_{1}, Γ_{2}, A_{1} ⊗ A_{2} \end{matrix} I′_{A} : \begin{matrix}B′_{1} ; ⋮ . ; ⊢ Δ_{1}, A_{1} & B′_{2} ; ⋮ . ; ⊢ Δ_{2}, A_{2} \\ ⊢ Δ_{1}, Δ_{2}, A_{1} ⊗ A_{2} \end{matrix}

If I′_{1} is another times rule, then clearly it can be permuted above I′_{A}. If I′_{1} is a par rule, then consider the inference I_{C} of D such that the principal formulas of I′_{1} and I_{C} are mapped to the same formula occurrence C = C_{0}℘C_{1} of R. Now (B_{j})^{−} is a subnet of R with A_{j} as a conclusion, hence (B_{j})^{−} ⊆ e(A_{j});

similarly (B′_{j})^{−} ⊆ e(A_{j}). Since I_{C} occurs above I_{A}, the link \frac{C_{0} C_{1}}{C_{0}℘C_{1}} occurs in

e(A_{j}); moreover, e(A_{j}) ∩ e(A_{1−j}) = ∅, hence the active formulas C_{0} and C_{1} of I_{1} are both in the same branch B′_{j} of D′. It follows that I_{1} can be permuted above I′_{A}.

(ii) Let (D)^{−} = R; let I_{A} be the inference in D whose principal formula is mapped to A in R; let B_{A} be the subderivation of D ending with I_{A}. To find a derivation D′ and a subderivation B′ such that (B′) = eA, let k be the number of formula-occurrences in eA \ (B_{A})^{−}: then there are also k inferences in D which must be successively permuted above I_{A}. We proceed by induction on eA, as characterized by Proposition 2. We need to consider only the following cases:

↓-step for times, clause (iv): X ∈ eA and X ≠ A implies X⊗Y ∈ eA. By induction hypothesis we may assume that X is introduced above I_{A}. If I′ introduces X ⊗ Y and occurs below I_{A}, then X is a passive formula of every sequent between I_{A} and I′. If we permute I′ with the inference I′′ immediately above it, we do not increase the number of formulas in eA\(B)^{−}, After a finite number of steps, the inference introducing X⊗Y is permuted above I_{A} and we have reduced k.

⇓-step for par links, clause (v): X ∈ eA, Y ∈ eA and X ≠ A ≠ Y imply X℘Y ∈ eA. By induction hypothesis we assume that both X and Y are introduced above I_{A}, and let I′ be the inference introducing X℘Y below I_{A}. It follows that for each application of the ⊗-rule between I_{A} and I′ the ancestors of X℘Y occur in one branch only, namely that containing I_{A}. Therefore the inference I′ can always be permuted with the inference I′′ immediately above it, even in the case when I′′ is a ⊗-rule. After a finite number of steps we reduce k.

Finally, to find a derivation D′′ and a subderivation B′′ such that (B′′) = kA, consider the doors of k(A) which are premises of some link; let X_{1}, …, X_{n} be the conclusions of such links. Since X_{i} ∉ kA by Lemma 2, we have A ∈ e(X_{i}) and by the above argument, the inference I_{A} can be permuted above the inference I_{i} introducing X_{i} in D. The argument can be repeated for all i ≤ n, without permuting I_{A} below a previously considered I_{j}; the result follows.

3 Proof Nets for First Order MLL^{−}

This section is essentially based on Girard [7].

3.1 First-Order Proof-Structures

We work with a first-order language for MLL^{−} and consider multiplicative proof-structures with the addition of the following links.

First-order links:

for all: \frac{A}{∀x.A}  exists: \frac{A[t/x]}{∃x.A}

Definition 8. The variable x (possibly) occurring free in the premise of a for

all link L : \frac{A}{∀x.A} is called the eigenvariable associated with the link L. Notice

that the same variable x occurs free in the premise and bound in the conclusion of L. We associate with each eigenvariable x a constant \underline{x}. Obviously, a link

of the form \frac{A[\underline{x}/x]}{∀x.A} is incorrect.

Definitions 9. (i) A proof structure for first order MLL^{−} is defined as before with the addition of the following conditions:

3. (a) Each occurrence of a quantifier link uses a distinct bound variable.

(b) If a variable occurs freely in some formula of the structure, then the variable is the eigenvariable of exactly one ∀-link.

(c) The conclusions of the proof structure are closed formulas.

4. We say that in a first-order proof-structure S eigenvariables are used strictly if no substitution of any set of occurrences of an eigenvariable x with the constant \underline{x} yields a correct proof structure with the same conclusions as R. We require also that in first-order proof-structures eigenvariable are used strictly.^{4}

(ii) Let R be a proof structure for MLL^{−} and let x be an eigenvariable in R. The free range of x in S is the set of all formula occurrences in which the eigenvariable x occurs freely. The existential border of x is the set of all the

formula occurrences which are the conclusion of a link L : \frac{B[t/y]}{∃y.B} where x

occurs in the premise but not conclusion of L. We say also that the link L is in the existential border of x.

(iii) We define the following additional reductions.

Symmetric Reductions

⋮ R(x)  ⋮ R[t/x]
A[t/x]  A^{⊥}  reduces to A[t/x] A^{⊥}[t/x]
∃x.A ∀x.A^{⊥}  cut

cut

where R(x) is the smallest substructure containing all occurrences of the eigenvariable x and R[t/x] results from R(x) by replacing t for x everywhere.

The definition of Danos-Regnier graph for first order proof structures is extended as follows.

Definitions 10. Let R be a proof structure for first order MLL^{−}.

(i) A Danos-Regnier switching s in a first order proof structure R for MLL^{−} consists in a switch for each par and for all link of R, where

• a switch for a par link is the choice of one of the premises of the link and • a switch for a for all link with associate eigenvariable x is a choice of

4We modify the setting of Girard [7] only with the condition of a strict use of the eigenvariables; this is enough to give a smooth tratment of kingdom and empires.

either (1) the premise of the link or of a formula occurrence in (2) the free range or in (3) the existential border of x (case (1) is needed if x does not occur free in R).

(ii) Given a switching s for R, we define the undirected Danos-Regnier graph s(R) as follows:

• the vertices of s(R) are the formulas of R;

• there is an edge between vertices X and Y exactly when:

(a) X and Y are the conclusions of a logical axioms or the premises of a cut link;

(b) X is a premise and Y the conclusion of a times or exists link;

(c) Y is the conclusion of a par or for all link and X is the occurrence selected by the switching s.

(iii) R is a proof net for first order DL [MLL^{−}] if for every switching s of R, the graph s(R) is acyclic [and connected].

The requirement that eigenvariable should be used strictly guarantees that the following structure is incorrect:

A(x)  A^{⊥}(x)  B(x)  B^{⊥}(x)
∀x.A  ∃x.A^{⊥}  ∃x.B  ∃x.B^{⊥}
∃x.A^{⊥} ⊗ ∃x.B

and must be rewritten as

A(x)  A^{⊥}(x)  B(c)  B^{⊥}(c)
∀x.A  ∃x.A^{⊥}  ∃x.B  ∃x.B^{⊥}
∃x.A^{⊥} ⊗ ∃x.B

where c is a new constant.

The following is an equivalent way of characterizing the same property.

Definition 11. An x-tread in a proof-structure R is a sequence C_{1}, …, C_{n} of formula occurrences which contain the free variable x and such that for each i < n there is a link L such that either (1) C_{i} is the premise and C_{i+1} is the conclusion of L or (2) C_{i} and C_{i+1} are conclusions of L (an axiom link) or (3) C_{i} is the conclusion and C_{i+1} is the premise of L.

Fact 1. In a proof structure eigenvariables are used strictly if and only if every occurrence of an eigenvariable x belongs to an x-thread ending with the ∀-link associated with x.

3.2 Subnets

The definition of a substructure S_{0} of a proof-structure S must take into account the requirement that all conclusion of S_{0} should be closed formulas.

Definitions 12. (i) Let S be a proof structure for first order MLL. A set of formula occurrences and links S_{0} is a substructure of S if S_{0} is a proof structure and there is an injective map ι : S_{0} → S preserving links such that X and ι(X) are the same formula or X comes from ι(X) by a substitution of a free variable x with \underline{x}. (We will usually omit to mention the map ι.) As before, a subnet is a substructure which satisfies the condition of proof-nets.

Fact 2. If S is a substructure of a first order proof-structure R and a link

L : \frac{A}{∀x.A} occurs in S, then the free range of x and its existential border are

contained in S.

Proof. All eigenvariables are used strictly in S by definition. Suppose L occurs in S but x occurs outside S; then there is an x-thread ‘crossing the border of’ S, say at a door C. This means that any substitution of \underline{x} for x in C spoils the link L, i.e., S cannot be a substructure, a contradiction.

Lemma 1 (first order case) In first order MLL^{−}, the intersection and the union of subnets are subnets if and only if the intersection is nonempty.

Proof. The argument for the propositional case applies here; we need only to make sure that if R_{1} and R_{2} are subnets of a proof-net R with R_{1} ∩ R_{2} ≠ ∅, then S = R_{1} ∪ R_{2} and R_{0} = R_{1} ∩ R_{2} are first-order substructures, and in particular, the eigenvariables are used strictly and their conclusions are closed. If a ∀-link of R does not occur in S, then the associated eigenvariable z is replaced by \underline{z} in the subnets R_{1} and in R_{2}, hence in S too. If a ∀-link with eigenvariable z occurs in R_{0}, then (since eigenvariables are used strictly in R) z also occurs inside R_{0} but not in any door of R_{0}, by the Fact 2. Finally, if a ∀ link with eigenvariable z occurs, say, in R_{1} \ R_{2}, then any occurrence of z in the substructure R_{0} is replaced by \underline{z}. Moreover z does not occur in the doors of S: indeed by the same corollary, z does not occur in the doors of R_{1}, hence it does not occur in R_{2} \ R_{1} either.

Proposition 1. (first order cases) Let R_{0} be a substructure of the proof net R. Then (iii)

S = For All (R_{0}) = {R_{0}[x/\underline{x}] \atop Γ \frac{A}{∀x.A}}

is a subnet if only if R_{0} is a subnet and \underline{x} does not occur in Γ. (iv) The substructure

S = Exists (R_{0}) = R_{0} ; \frac{A[t/x]}{∃x.A}

is a subnet if R_{0} is one.

Proof. (iii) S is a substructure, since the substitution of x for \underline{x} does not affect the conclusions of S, which remain closed. Given a switching s for S, sS differs from sR_{0} only for having a leaf ∀x.A connected by an edge to some vertex of R_{0}; thus sS is acyclic and connected, since sR_{0} is. (iv) is similar but easier.

Remark. It is not true that if S = Exists R_{0} and S is a proof-net then R_{0} is a proof-net: for instance in A[t/x] the term t may contain the eigenvariable of some for all link which occur in R_{0}.

As before Theorem 1.(a) follows as a corollary. (Notice that if ⊢ Γ is the end sequent of D and a free variable x occurs in Γ, then (D)^{−} = (D[\underline{x}/x])^{−}, a proof-structure with conclusions Γ[\underline{x}/x].)

Theorem 1.(a) (first-order case) Let D be a derivation in the sequent calculus for first order MLL ^{−}; then (D)^{−} is a proof net.

3.3 Empires and Kingdoms: Existence and Properties

As in the propositional case, we need to prove that given a proof-net R and a formula A in R, there always exists a subnet of R having A among its conclusions. Proposition 2. (Characterization of empires, first-order case; cf. [7]) Let R be a proof net for first order MLL^{−} and let A occur in R. Then the empire eA of A in R exists and is characterized by the following equivalent conditions:

(a) ⋂_{s} s(R, A), where s varies over all possible switchings;

(b) the smallest set of formula occurrences in R closed under conditions (b)(i)-(v) of Proposition 2 for propositional multiplicative links and moreover

(vi) if \frac{X[t/y]}{∃y.X} is a link in S and X[t/y] ≠ A, then ∃y.X ∈ e(A) if and only if

X[t/y] ∈ e(A), (↑- and ↓-steps);

(vii) if \frac{X}{∀y.X} is a link in S and X ≠ A, then ∀y.X ∈ eA if and only if the free

range of y and the occurrences in its existential border belong to eA (⇑- and ⇓-steps).

Proof. We follow Girard [7]. (vii) Suppose ∀y.X ∈ eA, but for some C in the free range of y we have C ∉ eA. Then A must be a premise of some link with conclusion Z, and for some s we have ∀y.X ∈ s(R, A) and C ∈ \overline{s(R, A)}, where \overline{s(R, A)} is the connected component not containing A after removal of the edge (A, Z) from sR. Therefore in s(R, A) there is a path connecting A and ∀y.X and moreover in \overline{s(R, A)} there is a path connecting Z and C which obviously does not depend on the switch for ∀y.X. Now if we change the switch for ∀y.X to choose C leaving all other choices unchanged, then we obtain a switch s′ such that s′R is cyclic: indeed there still remains a connection between Z and C in \overline{s′(R, A)} (which lies outside eA) and there certainly is a distinct connection between A and ∀y.X in s′(R, A) (since ∀y.X ∈ eA). But then s′R contains a cycle, a contradiction.

The example at the beginning of the present section shows that an eigenvariable x can occur outside the kingdom of ∀x.A, unless a strict use of eigenvariables is required. We have the following characterization of kingdoms in first order MLL^{−} (which is not true in in the setting of [7]).

Proposition 3. (Inductive definition of kingdoms, first-order cases) Let R be a proof net for first order MLL ^{−}. Then kA, the kingdom of a in R exists and is characterized as the smallest set of formula occurrences closed under conditions (i)-(iv) of Proposition 3 for multiplicative propositional links and moreover

(ii)’ if \frac{X[t/y]}{∃y.X} is a link in S and ∃y.X ∈ k(A), then X[t/y] ∈ k(A), (↑-step);

(v) if \frac{X}{∀y.X} is a link in S and ∀y.X ∈ kA, then the free range of y and the

occurrences in its existential border belong to kA (⇑-step).

3.4 Sequentialization

The proof of Lemma 2 extends to the first-order case without modificatons.

Lemma 2. (Empire-Kingdom Nesting) Let L_{1} : \frac{...A...}{C} and L_{2} : \frac{...B...}{D} be distinct links in a proof net R. Suppose B ∈ eA; then D ∉ eA if and only if C ∈ kD.

Lemma 3. (Ordering of the kingdoms, first-order case) In proof-nets for first order MLL^{−} the relation ≪ is a strict ordering of formula-occurrences that are not conclusions of axiom links.

Proof. Suppose X ∈ kY, where X and Y not the conclusions of axioms links. Two cases are to be added to the propositional proof.

Let X be the conclusion of a link \frac{A[t/x]}{∃x.A}. It follows from the definition of

kingdom and proposition 1 that kX = k(∃x.A) = k(A[t/x]) ∪ {∃x.A}. If X and Y are distinct and also Y ∈ kX, then Y ∈ k(A[t/x]) and this is absurd, since Y ∉ e(A[t/x]) follows from ∃x.A ∈ kY by lemma 2.

Finally, let X be the conclusion of a link \frac{A}{∀x.A}. If follows from proposition

1 that kX \ {∀x.A} ⊂ eA. If X and Y are distinct and also Y ∈ kX, then Y ∈ eA, and this contradicts lemma 2.

Theorem 1.(b) The Sequentialization Theorem holds in first order MLL ^{−}.

Proof. We consider first the lowermost par and for all links, if such links exist. Otherwise, we choose a terminal link L whose conclusion is maximal w.r.t. ≪. If L is an exists link, then the result of removing it is still a proof-net. Suppose

not; then L: \frac{A[t/x]}{∃x.A} is in the existential border of y, where y is associated with

\frac{B}{∀y.B} then ∃x.A ∈ k(∀y.B), by Fact 2, hence ∃x.A it cannot be maximal w.r.t.

≪. The rest of the proof is as before.

3.5 Permutability of Inferences in the Sequent Calculus

Counterexample. Let x occur free in P. The following is a derivation in MLL^{−} in which the applications of the ∃-rule and of the ∀-rule cannot be permuted.

⊢ P^{⊥}, P

∃ ⊢ P^{⊥}, ∃x.P

∀ ⊢ ∀x.P^{⊥}, ∃x.P

Theorem 2. (first order case) The Theorem on permutability of inferences holds in first order MLL ^{−}.

Proof. (i) Assuming the pure parameter property, the argument is similar to the propositional case, where for all rules behave like par rules and exists rules like times rules. The nontrivial case is the following: an inference I′_{A} of D′ has the principal formula A = ∃x.A_{1} and must be permuted below a for all rule I′_{1}. As before we argue that in D we have an inference I_{B} such that I′_{1} and I_{B} are mapped to B = ∀y.B_{1} and that such an inference must occur above the inference I_{A} whose active formula is A_{1}[t/x]; by the pure parameter property of D, y does not occur in t, and the permutation is permissible.

(ii) As before, the argument is by induction on eA \ (B_{A})^{−}; to the propositional cases we add the following cases (the cases of existential links being unproblematic):

(⇑-step) for all link, clause (vii): By the pure parameter property the eigenvariables occur only above the associated ∀-inference, which already occurs above I_{A} by induction hypothesis. (⇓-step) for all links, clause (vii): Let I′ be the inference introducing ∀y.X below I, where ∀y.X ∈ eA. By induction hypothesis the eigenvariable y occurs only in sequents above I_{A}, except for one occurrence of a formula X(y) (an ancestor of ∀y.X) for each sequent between I_{A} and I′. Hence we can always permute I′ with the inference immediately above it.

References

[1] G. Bellin. Mechanizing Proof Theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information, Phd Thesis, Stanford University. Available as: Report CST-80-91, June 1990, Dept. of Computer Science, Univ. of Edinburgh.

[2] G. Bellin. Proof Nets for Multiplicative and Additive Linear Logic, Report LFCS-91-161, May 1991, Dept. of Computer Science, Univ. of Edinburgh.

[3] V. Danos and L. Regnier. The Structure of Multiplicatives, Arch. Math. Logic (1989) 28, pp. 181-203.

[4] J. Gallier. Constructive Logics. Part II: Linear Logic and Proof Nets, preprint, Dept. of Computer and Information Science, University of Pennsylvania, 200 South 33rd St., Philadelphia, PA 19104, USA, Email:

jean@saul.cis.upenn.edu

[5] J-Y. Girard. Linear Logic, Theoretical Computer Science 50, 1987, pp. 1-102.

[6] J-Y. Girard. Quantifiers in Linear Logic, Proceedings of the SILFS conference held in Cesena, January 1987.

[7] J-Y. Girard. Quantifiers in linear logic II. Preprint, Équipe de Logique Mathématique, Université Paris VII, Tour 45-55. 5^{e} étage, 2, Place Jussieu, 75251 PARIS Cedex 05. France.

Gianluigi Bellin and Jacques van de Wiele Équipe de Logique Université de Paris VII Tour 45-55, 5^{e} étage 2 Place Jussieu 75251 Paris Cedex 05 France