Subnets of Proof-nets in Multiplicative Linear Logic with MIX

G. Bellin ^{∗}

January 23, 1996

Abstract

The paper studies the properties of the subnets of a proof-net for first order Multiplicative Linear Logic without propositional constants ( MLL^{−}), extended with the rule of Mix: from ⊢ Γ and ⊢ Δ infer ⊢ Γ, Δ. Asperti’s correctness criterion and its interpretation in terms of concurrent processes is extended to the first order case. The notion of kingdom and empire of a formula are extended from MLL^{−} to MLL^{−} + Mix. A new proof of the sequentialization theorem is given. As a corollary, a system of proof-nets is given for De Paiva and Hyland’s Full Intuitionistic Linear Logic with Mix; this result gives a general method to translate Abramsky-style term assignments into proof-nets, and viceversa.

Contents

1 Preface 2 1.1 The Mix Rule: why not? . . . . . . . . . . . . . . . . . . . . . 2 1.2 Why Proof-Nets? . . . . . . . . . . . . . . . . . . . . . . . . . 6 2 Subnets of Proof-nets in MLL^{−} + Mix 11

∗Research supported by EC Individual Fellowship Human Capital and Mobility, contract n. 930142. Submitted March 1994; revised January 1996.

2.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2 Proof-Structures . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3 Permutation of Inferences and Subnets . . . . . . . . . . . . . 15 2.4 Paths, Chains, Loops . . . . . . . . . . . . . . . . . . . . . . . 17 2.5 Kingdoms and their Ordering . . . . . . . . . . . . . . . . . . 19 2.6 The Sequentialization theorem . . . . . . . . . . . . . . . . . . 22

3 Asperti’s concurrent processes 28 3.1 Asperti’s Correctness Condition, First-order Case . . . . . . . 30

4 Full Intuitionistic Linear Logic 33 4.1 Term Calculus for Multiplicative FILL . . . . . . . . . . . . . 34 4.2 Proof-nets with Orientations. . . . . . . . . . . . . . . . . . . 36

1 Preface

1.1 The Mix Rule: why not?

The structural rule of Mix,^{1} namely

Mix: \frac{Γ ⊢ Δ Π ⊢ Λ}{Γ, Π ⊢ Δ, Λ}

is not accepted in the system of Girard’s (classical) Linear Logic (LL). Nevertheless, the presence of Mix is ubiquitous in researches on linear logic: it is satisfied by most models of linear logic, like the denotational semantics of coherent spaces, the game-theoretic semantics and more. As the example of the game-theoretic semantics shows [2, 23], results are often obtained for LL + Mix first, additional efforts are then needed to refine them to the case of LL.

\frac{Γ ⊢ Δ, A, …, A A, …, A, Π ⊢ Λ}{Γ, Π ⊢ Δ, Λ}

1The name comes from Girard [18]; the name Mingle has been used for a similar rule in relevance logic. The name Mix was used by Gentzen for the following rule However, such a variant of Cut cannot be admitted in linear logic; therefore, there is no real danger of confusion between Gentzen’s use and Girard’s use of the term.

Several extensions of classical linear logic are possible:

(1) LL + Mix. This system has the equivalent axiomatizations:

LL + ⊥ ⊢ 1  or  LL + A ⊗ B ⊢ A℘B, for all A and B.

(2) LL + Mix + the axiom empty sequent ⊢. Equivalent axiomatization:

LL + ⊥ ⊣⊢ 1; we may call this system linear paraconsistent.

(3) LL + (A ⊗ B) ⊣⊢ (A℘B), for all A and B.

(4) LL + unrestricted Weakening: \frac{⊢ Γ}{⊢ Γ, A}. Equivalent axiomatization:

LL + ⊥ ⊢ 0. This logic is called Affine logic (AL).

It is easy to see that the sets of theorems in these systems satisfy

(1) ⊂ (2) ⊂ (3),  (1) ⊂ (4),  (2) ⊄ (4),

where inclusions are proper. We will consider only the multiplicative fragment MLL of linear logic; MLL^{−} denotes the multiplicative fragment without the propositional constants 1 and ⊥. This paper is about the fragment MLL^{−} + Mix of (1).

We want to distinguish linear logic and these extensions by their metamathematical and semantical properties. The denotational semantics of coherent spaces, which gave Girard a main motivation for the creation of LL, satisfies the system (2) as well as (1) – at least in its original form [18]. Remember that classical LL is modelled by ∗-autonomous categories (with additional structure to interpret to the exponentials) and that the logic (3) is modelled by compact closed categories; logics (1) and (2) can also be modelled by adding suitable morphisms in free ∗-autonomous categories.

Affine logic differs considerably from linear logic in its metamathematical properties. For instance, it is known that propositional AL is decidable, while propositional linear logic is not. We will not study this system here; a notion of proof-net for multiplicative AL (called there direct logic) has been given in [7].

However, the restricted Weakening rule \frac{⊢ Γ}{⊢ Γ,?A} and the ⊥-rule \frac{⊢ Γ}{⊢ Γ, ⊥}

are needed in the system of linear logic if intuitionistic and classical logics are to be interpreted within it. Now Weakening is the only rule of linear logic which makes cut-elimination non-confluent, so that the Church-Rosser property fails. Notice that ⊥ ⊢ ?A is valid for all ?A; thus we can restrict our discussion to the ⊥-rule without loss of generality.

In linear logic, as in any consistent system, the Weakening rule is justified by the valid context. On the contrary, the system (2) has ⊥-axioms; for this reason the Church-Rosser property holds of it. Intuitively and philosophically, an important threshold is trespassed from (1) to (2): if 1 and ⊥ are regarded as particular notions of truth and falsity, then the system (2) belongs to the domain of paraconsistent logics, since it allows a local form of inconsistency.

In the first paper to be dedicated to the rule of Mix [17], A. Fleury and C. Retoré postulate a duality between the rule of Mix and the axiom empty sequent; such a duality is formalized by assigning an integer (truth-level) to each sequent with the obvious assignments

⊢^{0} A^{⊥}, A  ⊢^{0} 1  \frac{⊢^{m} Γ, A  ⊢^{n} Δ, B}{⊢^{m+n} Γ, Δ, A ⊗ B}  \frac{⊢^{n} Γ, A, B}{⊢^{n} Γ, A℘B}

and finally, by letting

⊢^{1}  ⊢^{1} ⊥  \frac{⊢^{m} Γ  ⊢^{n} Δ}{⊢^{m+n−1} Γ, Δ}

The notion provable at the zero truth-level does not coincide with provable in multiplicative linear logic, e.g., ⊢^{0} ⊥ ⊗ (1℘1). But some years ago there might have been the hope that given a proof in the paraconsistent linear system (2) there could be a feasible algorithm to decide whether or not the proof already belongs to linear logic. In this case, the system of proof-nets for (2) given by Fleury and Retoré [17] would have given a very good syntactic representation for an extension of linear logic, enjoying the Church-Rosser property and allowing an easy identification of relevant and fully consistent proofs.

However by a result of Lincoln and Winkler [24], the problem of deciding whether a theorem in the logic (2) is also a theorem of MLL is NP-complete; in other words, knowing a proof D of ⊢ Γ in the logic (2) need not reduce the complexity of finding a proof of Γ in MLL. This fact may be taken as evidence that the border between relevance and irrelevance, between consistency and paraconsistency remains marked very strongly within linear logic. Thus from a logical point of view it is reasonable to “draw a line” between logics (1) and (2) and to be interested in (1) per se.

By contrast, to decide whether a theorem ⊢ Γ in MLL^{−} with Mix is also a theorem of MLL^{−} it is enough to look at Γ, according to the formula

(§)  #par + #conclusion = #times + 2(#Mix) + 2;

equivalently, if a proof-net with conclusions Γ is given, we may use

(§§)  #Mix + #axiom + 1 = #par + #conclusions + #Cut.

Both formulas are easily proved by induction on the derivations in MLL^{−} with Mix.

An argument in favor of MLL^{−} + Mix was given by Girard in his fundamental paper: “One of the arguments for MIX is that, without it, the type of communication considered in proof-nets is very totalitarian: everything communicates with everything, while MIX could accept more liberal solutions, typically two non-interconnected proof-nets, etc.” ([18] pp.99-100).

The suggestion that the logic MLL^{−} + Mix could be more suitable for the representation of parallel logical computations than MLL^{−} itself has been taken up by Asperti [3]. He has given convincing evidence of this fact, by showing that the verification of correctness for proof-nets in this logic is equivalent to the successful termination of a concurrent game in the style of Petri-nets. We will discuss Asperti’s result in more detail below.

Is the rule of Mix essentially a classical rule, or can it does it occur also in intuitionistic systems? The multiplicative fragment of intuitionistic linear logic may be axiomatized as Gentzen’s systems as follows:

(I-1) (ILL) the intuitionistic linear consequence relation, axioms, Cut, Exchange, rules for the tensor and linear implication;

(I-2) the classical two-sided linear consequence relation, axioms, Cut, Exchange, rules for the tensor and the par, without negation; (I-3) (FILL, Full Intuitionistic Linear Logic) the classical two-sided linear

consequence relation, rules for tensor, par and linear implication; special restrictions must be put on the right rule for implication to guarantee the intuitionistic nature of the connective. It was not immediately obvious how to formulate such restrictions so that the system would enjoy Cut-elimination, as Schellinx [27] first pointed out.

Thus FILL embodies simultaneously features of concurrent logical computations, induced by its connective par and the sequential properties of intuitionistic linear implication.

Remember that the systems of intuitionistic linear logic have well known categorical models: the system (I-1) is modelled by symmetric monoidal closed categories; the system (I-2) is modelled by weakly distributive categories [10, 11, 12]; the system (I-3) has also a categorical model, in fact it was inspired by one of V. de Paiva Dialectica Categories [15, 16]).

The rule of Mix can be safely added to the system (I-2); moreover, one of de Paiva’s Dialectica Category satisfies the Mix rule. Here we show that Mix can be safely added to (I-3), once the restriction on the right implication rule is correctly formulated. To this purpose, Hyland and de Paiva [20] use term assignments to the sequent calculus, recently refined by Bierman. We give an equivalent formalization by a system of proof-nets for FILL + Mix; since our system admits cut-elimination, it yields an independent verification of the restrictions by term assignments on the intuitionistic implication. This application shows that the rule of Mix need not be excluded if we use linear logic as a framework for the representation of classical and intuitionistic logic.

1.2 Why Proof-Nets?

Proof-nets are among the most fascinating constructions to have arisen from linear logic. They provide a concise graph-theoretic representation of deductions in fragments and variants of linear logic, principally, first order MLL^{−} and MLL^{−} + Mix. Each normalization step of proof-nets reduces the size of the data and the normalization process enjoys the Church-Rosser property. There is a “context-forgetting” map ( )^{−} from sequent calculus derivations in linear logic to proof-nets, such that (D)^{−} = (D′)^{−} if and only if D′ results from D by successive permutations of inferences; in other words, ( )^{−} is a bijection between proof-nets and the equivalence classes of sequent derivations modulo permutations of inferences or, equivalently, modulo the denotational semantics of coherent spaces.

A beautiful part of the subject is the interaction between the global correctness conditions, which a graph (proof-structure) must satisfy to be a proof-net, and a local normalization process. The decontextualization of inferences, represented as the vertices (links) of the graph, opens the way to a concurrent logical computation (parallelization of the syntax). Given a proofnet R, we have a polynomial time method to obtain a sequent derivation D such that (D)^{−} = R (sequentialization theorem). Several correctness conditions have been found, which are directly connected with the game-theoretic semantics of MLL^{−}, with coherence theorem in monoidal closed categories, etc. and which provide tools for the study of normalization in the “geometry of interaction”. While many correctness condition require exponential time, some terminate in quadratic time.

Girard’s no-short-trip condition [18] does not distinguish between correct and incorrect proof-structures for MLL^{−} with Mix: thus the fundamental step in the study of proof-nets for the system (1) was Danos and Regnier’s correctness condition [14], which requires the acyclicity of the D-R-graphs on the proof-nets in the case of MLL^{−} + Mix, and in addition the connectedness of such graphs in the case of MLL^{−}; of course, the additional requirement of connectedness may be replaced by counting according to the formulas (§) or (§§). This criterion is also used by Fleury and Retoré [17]. However, it had been independently discovered in the tradition of direct logic [22, 5, 7], where it was applied to automated deduction [21]. Girard’s treatment of proof-nets for first order MLL^{−} is a straightforward generalization of the propositional case [19]. The main technical idea is to define D-R-graphs so that the conclusion of a for all link may be alternatively connected either to the premise of the link or to any other formula containing the eigenvariable associated with that link.

A significant contribution to proof-nets for MLL^{−} with Mix has been given by A.Asperti [3]. His criterion appears as the right generalization to MLL^{−} with Mix of Girard’s no-short-trip condition. While Girard’s trip are sequential processes, Asperti’s trips are distributed processes. Initially, a token of type ↑ occurs on each conclusion and Cut of the proof-structure; they propagate upwards, according to A-switchings for the times and Cut links; whenever both conclusions of an axiom are reached by tokens ↑, these are replaced by tokens ↓ which propagate downwards; both premised must be reached to descend par link; when a times link is reached for the second time, the trip continues with a token ↑ on the premise not yet reached, and so on. The process terminates successfully when there are tokens ↓ on all conclusions. A proof structure is correct if for every A-switching, Asperti’s trip terminates successfully.

Asperti’s trips can also be interpreted in terms of concurrent processes: formula-occurrences as processes; the activation or termination of a process A is the act of putting a token ↑ or ↓, respectively, on a formula A. A process A℘B is executed by executing in parallel the processes A and B. The rules of the game on axioms and par links are syncronization requirements between processes. The execution of a process A ⊗ B is the execution of A and B as mutually exclusive processes, in the order determined by an A-switch. Each A-switching imposes restrictions on the order of the execution of the processes, called a causal dependencies; Asperti proved that some trip ends in a deadlock if and only if there is a cyclic causal chain. Asperti’s result gives a motivation to reconsider the treatment of proof-nets for MLL^{−} with Mix given by the author in his thesis [5].

Our contribution here is the extension of Asperti’s criterion to the firstorder case: when the premise of a for all link is activated, its eigenvariable is declared a global variable; now the premise of an exists link or of a Cut is activated only if all the eigenvariables occurring in it occur also in the list of global variables. Thus the correctness criterion for the first order case is a natural requirement of synchronization between the activation of processes occurring in for all and exists links.

The bridge between local and global properties of proof-nets, thus the key to many results in the subject, is the study of the subnets of proof-nets; here it is more instructive to study subnets not just as subgraphs, but as subderivations of formulas: in particular, we consider the kingdom k(A) and the empire e(A) of an occurrence A in a derivation, i.e., the smallest and the largest subnet having A as a conclusion.

In the case of MLL^{−} without Mix it has been shown by J. van de Wiele and the author (see Theorem 13, pp. 35-45, in [8]) that certain Girard’s trips on a proof-net correspond to translations of intuitionistic MLL^{−} (namely, the multiplicative fragment of ILL, see I-1 above) into classical MLL^{−}. More precisely, there is an operation G mapping sequents Γ ⊢ A in intuitionistic MLL^{−} into sequents ⊢ Γ_{I}, A_{O} in classical MLL^{−}, where p_{O} = p = p_{I}^{⊥} and p_{I} = p^{⊥} = p_{O}^{⊥} and moreover

(A ⊗ B)_{O} = A_{O} ⊗ B_{O} (A ⊗ B)_{I} = A_{I}℘B_{I}
(A −∘ B)_{O} = A_{I}℘B_{O} (A −∘ B)_{I} = A_{O} ⊗ B_{I};

G maps proofs of ILL into proofs of CLL consequently. Conversely, we have the following fact: given a cut-free proof-net R with conclusions Γ, A in MLL^{−}, every trip in the sense of Girard [18] on a proof-net reintroduces an input-output orientation and thus corresponds to a derivation D′ in intuitionistic MLL^{−} such that R may be regarded as (G(D′))^{−}. If R contains cut-links, then only trips which are compatible with the process of cut-elimination (computationally consistent orientations) yield such an intutionistic derivation.

Does an analogous result hold for MLL^{−} with Mix? The intuitionistic system ILL permits the use of Mix only with severe restrictions, which are removed in the systems (I-2) and (I-3), i.e., in FILL. Now the translation of the system FILL into proof-nets is easy, once an adequate restrictions on the intutionistic implication rule has been found: the key notion here is that of a directed chain, yielding the requirement that for every par link A_{I}℘B_{O}, if a directed chain from A_{I} eventually terminates in X_{O}, then X = B (functionality of implication). On the other hand, the converse result has no analogue: there are proof-nets for MLL^{−} that are not in the image of any FILL^{−} derivation, e.g., the only subnet with conclusions p℘q, q^{⊥}℘r, r^{⊥}℘q^{⊥}, where functionality of implication fails for every admissible inputoutput orientation.

The dynamical interpretation of this result is that every cut-elimination process in classical MLL^{−} can be simulated by some cut-elimination process in intuitionistic MLL^{−}; the classical nature of the dynamics of proof-nets emerges only in the fact that the correspondence is many-one. On the other hand, when Mix is introduced there are cut-elimination processes in classical MLL^{−} + Mix which have no intuitionistic counterpart in FILL^{−} with Mix.

In conclusion, in this paper we present the following results:

1. a generalization of the theory of empire and kingdoms in [9] from MLL^{−} to MLL^{−} with Mix;

2. a proof of the sequentialization theorem MLL^{−} with Mix;

3. an extension of Asperti’s criterion to the first order case;

4. a system of proof-nets for the multiplicative fragment of de Paiva and Hyland Full Intuitionistic Linear Logic [20] with Mix.

The following facts should be remarked:

1. The theory of subnets of a proof-net in MLL^{−} with Mix does not coincide with that for MLL^{−} without Mix (see [9]). Indeed the notion of subnet is trivialized here; instead we need the notion of a normal subnet, i.e., a subnet whose sequentialization may be a subderivation of the sequentialization of the whole proof-net. In MLL^{−} without Mix every subnet is normal.

2. Our argument for the proof of the sequentialization theorem for MLL^{−} with Mix is different from the other existing arguments in that we do not reduce to the case of MLL^{−} without Mix. We argue directly about the graph-theoretic configuration of chains and about the nesting of kingdoms.

3. The characterization of first order proof-nets in terms of Asperti’s games gives an efficient and intuitive alternative and an interpretation in terms of parallel processes of the graph-theoretic condition of acyclicity.

4. The specific form of our sequentialization argument for MLL^{−} with Mix easly extends to a proof-net representation of Full Intuitionistic Linear Logic with Mix; the method used here to translate sequent calculi with λ-term assignments in the style of Abramsky [1] into proof-nets, and viceversa, may be more generally applicable.

It would be desirable to give these rather technical features of proof nets a more abstract mathematical presentation. We will not do this here, except for the following elementary remarks. Every proof-structure can be associated with a proof in the logic (3), or in other words it can be regarded as a morphism in a free compact-closed category. There is a functor F from ∗-autonomous categories to compact closed categories. There are morphisms in a free compact closed category which are not in the image of F, e.g., g ∘ f where f : 1 → A ⊗ A^{∗} and g : A ⊗ A^{∗} → ⊥. The test of the correctness conditions and the sequentialization algorithm on a proof-structure R are related to the construction of a morphism f in a free ∗-autonomous category such that F (f) corresponds to R; such a construction does not seem to be functorial.

Moreover, there is a functor G from symmetric monoidal closed categories to ∗-autonomous categories, which can be described as forgetting the inputoutput orientation of an intuitionistic derivation. Conversely, the result by Bellin and van de Wiele [8] describes a process of costructing a map in a free symmetric monoidal closed category, given a map in a compact closed category; such a process does not seem to be functorial.

R.Blute made an essential use of proof-nets for MLL^{−} with Mix in his study of coherence in monoidal categories [10]. Moreover, (two sided) proofnets have been used to give categorical models of various extensions of the system (I-2) of weakly distributive categories [10, 11]; hence proof-nets already play a role in the study of monoidal categories.

Further examples of uses of Mix and of non-interconnected proof-nets arise in the study of non-commutative linear logic [25]. Braided proof nets are proof-nets embedded in the space R^{3}; the embedding of proof-nets in R^{2} yields a representation of commutative linear logic in a non-commutative enviromnent with the explicit rule of exchange [6]. In that context, we find a natural development of the results presented here, as well as in Asperti [3].

2 Subnets of Proof-nets in MLL^{−} + Mix

2.1 Definitions

The first-order language of linear logic is defined in [18]; we consider the fragment of first-order MLL^{−} (Multiplicative Linear Logic without Constants). Remember that the operation ( . )^{⊥} (linear negation) applies to atomic formulas only; formulas are built from atoms p_{1}, …, and their negations using the binary connectives ⊗ (times) and ℘ (par) and the quantifiers ∀ (for all) and ∃ (exists); negation of non-atomic formulas is defined: p_{i}^{⊥⊥} =_{d} p_{i}, (A ⊗ B)^{⊥} =_{d} A^{⊥}℘B^{⊥}, (A℘B)^{⊥} =_{d} A^{⊥} ⊗ B^{⊥}, (∀x.A)^{⊥} =_{d} ∃x.(A^{⊥}), (∃x.A)^{⊥} =_{d} ∀x.(A^{⊥}).

The sequent calculus for first order MLL^{−} [18] contains logical axioms, cut, the structural rule of exchange and the logical rules for times, par, for all and exists.

logical axiom: ⊢ A^{⊥}, A

cut: ; \frac{⊢ Γ, A^{⊥} ⊢ Δ, A}{⊢ Γ, Δ}

exchange:

\frac{⊢ Γ, A, B, Δ}{⊢ Γ, B, A, Δ}

times: \frac{⊢ Γ, A ⊢ Δ, B}{⊢ Γ, Δ, A ⊗ B,}  par: ; \frac{⊢ Γ, A, B}{⊢ Γ, A℘B}  for all: ; \frac{⊢ Γ, A}{⊢ Γ, ∀x.A} where x ∉ Γ; exists: \frac{⊢ Γ, A[t/x]}{⊢ Γ, ∃x.A}

We focus on the extension of MLL^{−} with the structural rule of Mix:

Mix:  \frac{⊢ Γ  ⊢ Δ}{⊢ Γ, Δ}

We use the standard terminology concerning sequent calculi, namely we speak of the passive, active and principal formulas in an inference; e.g., all formula occurrences are passive in a Mix, the cut formulas are active in a Cut, etc. Let I_{1}/I_{2} be a pair of consecutive inferences in a derivation such that the principal formula of I_{1} is not active in I_{2}; observe that we can always permute the order of these inferences, unless indicated in the following table.

I_{1}:  Cut Mix  ⊗  ℘ ∀  ∃

I_{2}:

Cut

Mix

⊗

℘  no  no  no
∀  no

∃

2.2 Proof-Structures

For the original definitions of links and proof-structures we refer to the definitions in the paper “Subnets of proof-Nets in MLL^{−}” [9]. The following variant definition is simpler, and evidently equivalent to the standard one; it is therefore adopted here, except for occasional uses of the original notation.

Definitions. (i) A proof-structure is a graph whose edges are oriented and labelled with occurrences of formulas. (Usually we will not keep the distiction between edges and their labels in our text.) Vertices are either conclusions, with one incident edge, or links: axioms, for all, exists links, of incidence 2, and cut, times and par links, of incidence 3. The arrows pointing at a link are its premises, the other incident arrows are its conclusions, as indicated in the following table:

AXIOM  CONCLUSION  CUT A^{⊥}  A  B A  A^{⊥} A  cut A  B  ∀ A  A[t/x] FOR ALL PAR TIMES  EXISTS ⊗  ℘ A ⊗ B  A℘B  ∀x.A  ∃ ∃x.A

(ii) First-order proof-structures must satisfy the following conditions on free and bound variables; for further details and motivations, see [9]. Remember that an eigenvariable is a free variable which becomes bound in a universal quantification; to each eigenvariable x associate a distinct constant \underline{x}.

(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.

(d) (Strictness condition) No substitution of any number of occurrences of an eigenvariable x with the constant \underline{x} yields a correct proof structure with the same conclusions.

(iii) A Danos-Regnier graph (D-R-graph) is the graph resulting from the following transformations:

• for each par link select one premise and remove its connection with the link;

• for each for all link L with conclusion ∀x.A select a link L′ whose premise B contains the eigenvariable x; introduce an edge between L and L′ and at the same time remove the existing connection between the edge A and the link L; if no such B exists, then leave the link unchanged.

The set of these choices is called a switching; if s is a switching on a proof-structure R, the D-R-graph is written sR. A path ending with the edges A and B in the D-R-graph sR will be denoted by path_{s}(A, B).

(iv) A proof-structure R is a proof-net for MLL^{−} with Mix if for every switching s the D-R-graph sR is acyclic.

(v) A substructure R′ of a proof-structure R is a proof-structure together with an embedding ι : R′ → R such that if A = ι(A′), then A′ results from A by substitution of eigenvariables with constants (each eigenvariable x being replaced by a distinct constants \underline{x}). Obviously, in the propositional case we may let ι be the identity function on a subgraph. Given a formula A in a proof-structure R, which is conclusion of a link v, we write st(A), or st(v), for the smallest substructure with A as a conclusion.

(vi) A subnet of a proof-net is a substructure which is a proof-net.

One aim of this paper is to give a new proof of the following theorem:

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

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

(b) (Sequentialization) If R is a proof net with conclusions Γ for MLL ^{−} with Mix, 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′)^{−}.

Parts (a), (b) and (d) are easy; we will focus on part (b).

2.3 Permutation of Inferences and Subnets

Another aim of this paper is to develop a theory of subnets of proof-nets which yields an answer to the following question: given an inference I in a sequent derivation D in MLL ^{−} with Mix, which inferences I′ of D can be permuted above or below I?

For the system MLL^{−} without Mix the answer is given by Theorem 2 in [9]. The largest and the smallest subnet having A as a conclusion are called the kingdom kA and the empire eA of A, respectively. Now let I, I′ be inferences in D and let v, v′ be the correponding links in (D)^{−}; suppose v is a par or times link with premises A, B and conclusion C. Now I′ can be permuted below I if v′ does not occur in kC. To see whether I′ can be permuted above I, we look whether v′ occurs in eA ∪ eB if I is a times rule; if I is a par rule, we look whether v′ occurs in eC.

We will obtain a similar result for MLL^{−} with Mix, but in order to do this we must strengthen the notions of kingdom and empire. In order to see this, consider following derivations:

D_{1}:  D_{2}:
⊢ A^{⊥}, A ⊢ B, B^{⊥} ⊢ A^{⊥}, A ⊢ B, B^{⊥} Mix  ⊗
⊢ A^{⊥}, A, B, B^{⊥}  ⊢ A^{⊥}, A ⊗ B, B^{⊥} exchanges  exchanges
⊢ A, B, B^{⊥}, A^{⊥}  ⊢ A ⊗ B, B^{⊥}, A^{⊥} ℘  ℘
⊢ A, B, B^{⊥}℘A^{⊥}  ⊢ A ⊗ B, B^{⊥}℘A^{⊥}

The “context forgetting” map sends D_{1} and D_{2} to the following proof-nets for MLL^{−} + Mix:

R_{1} = (D_{1})^{−} :  R_{2} = (D_{2})^{−} :

A  B  B^{⊥}  A^{⊥}  A  B  B^{⊥}  A^{⊥}
B^{⊥}℘A^{⊥}  A ⊗ B  B^{⊥}℘A^{⊥}

In MLL^{−} with Mix R_{1} is the largest subnet of R_{2} having A as a conclusion. However, D_{1} is not a subderivation of D_{2} nor of any derivation resulting from D_{2} by permutations of inferences; also, we cannot permute the par rule above the times rule in D_{2}. Notice that in MLL^{−}, R_{1} is a substructure of R_{2}, not a subnet; but in MLL^{−} with Mix any substructure of a proof-net satisfies the acyclicity condition, hence it is a subnet.

Definitions. (i) A non-logical axiom is a link with no premise and n conclusions, for some n. We consider proof-structures with non-logical axioms; D-R-graphs for such structures are defined as before. A proof-net with nonlogical axioms for MLL^{−} with Mix is a proof-structure with non-logical axioms which satisfies the acyclicity condition.

(ii) Let R be a proof-structure for MLL^{−} and let S be a substructure of R with conclusions C_{1}, …, C_{n}. The complementary substructure \overline{S} of S in R consists of all edges and links in R \ S and, in addition, the edges C_{1}, …, C_{n} and a new non-logical axiom \overline{C_{1}, …, C_{n}} with these edges as conclusions.

(iii) Let R be a proof net for MLL^{−} with Mix. A subnet S of R is normal if the complementary substructure \overline{S} of S is a proof-net with a non-logical axiom.

(iv) The kingdom kA [or the empire eA] of A in R is the smallest [the largest] normal subnet of R which has A as a conclusion.

Proposition 1. Let R be a proof net for MLL ^{−} with Mix. A subnet S of R is normal if and only if the following condition is satisfied: for every X and Y in S and for every switching s of R, if there is a path_{s}(X, Y) connecting X and Y in sR, then such a path belongs also to sS (where we use the same symbol s for the switching of R and its restriction to S).

Corollary. The intersection of two normal subnets is a normal subnet. The union of two normal subnets need not be normal.

Proof. Exercise.

It is not immediately obvious how to prove that given a proof-net R for MLL^{−} + Mix and a formula-occurrence A in R, there exists a subnet which is normal and has A as a conclusion. Girard’s inductive definition of empires (see [9], Proposition 2 sections 2.3 and 3.3) cannot be used for this purpose in MLL^{−} + Mix : in the following example the inductive definition in question applied to A℘B does not identify a normal subnet with A℘B as a conclusion.

\overline{D D^{⊥}} B^{⊥}  A^{⊥} \overline{C^{⊥} C}  A  B
D^{⊥}℘B^{⊥}  A^{⊥}℘C^{⊥}  A℘B
(D^{⊥}℘B^{⊥}) ⊗ (A^{⊥}℘C^{⊥})

2.4 Paths, Chains, Loops

A path in D-R-graph is undirected. The relation between premises and conclusions of links induce an orientation on proof-structures which will be called the structural orientation. A chain may be regarded simply as path with the structural orientation. In fact how the notion of a correction graph was first introduced by [22] in this more concrete form. The structural orientation of chains is essential in Asperti’s games and for the related notion of a causal path (see [3], and the section below).

Definitions. (i) The relation between a premise and the conclusion of a link has a transitive closure, which we denote by ≺ ; if A ≺ X, then we say that A is a hereditary premise of X or that X is a hereditary conclusion of A. Obviously, ≺ is also an ordering of links. It may be called the structural orientation of the proof-structure.

(ii) In a first-order proof-structure the for all switches introduce edges between links which are not in the ≺ relation; thus, given a switching s, we consider the order ≺_{s} of links defined as follows: v ≺_{s} w if and only if there are for all links w_{1}, …, w_{n} and links v_{1}, …, v_{n} such that the switching s yields s(w_{i}) = v_{i} and, moreover, we have v ⪯ v_{1}, w_{1} ⪯ v_{2}, …, v_{n} ⪯ w.

(iii) Let R be a proof-structure and consider path_{s}(v, w), the path from the links v and w ending with edges A to B in the D-R-graph sR, also written path_{s}(A, B). Then path_{s}(v, w) is called a chain of the type indicated by the following table:

TYPE :  v has A as a  w has B as a
⌈v, w⌉ or ⌈A, B⌉ :  premise ;  premise;
⌈v, w⌋ or ⌈A, B⌋ :  premise;  conclusion;
⌊v, w⌉ or ⌊A, B⌉ :  conclusion;  premise;
⌊v, w⌋ or ⌊A, B⌋ :  conclusion;  conclusion.

The notation “|A, B⌉” stands for “either ⌈A, B⌉ or ⌊A, B⌉”, and similarly for ⌈A, B|, |A, B|. We call the links w_{i} lower links of the chain γ; A, B and the conclusions of the links w_{1}, …, w_{n} are called the lower members of γ. We abbreviate “a chain γ of type ⌈A, B⌉” as “a chain ⌈A − γ − B⌉”.

(iv) A chain ⌈A − γ − B⌉ where A and B are premises of a par link will be called a loop. The par link in question (or its conclusion) is called the exit of the loop.

(v) We define a relation ≪ thus: let X ≪_{0} Y if X ≺ Y [or X ≺_{s} Y for some switching s, in the first order case]. Moreover let X ≪_{1} Y if X is in a loop γ with exit Y. Let ≪ be the transitive closure of ≪_{0} and ≪_{1}. Obviously, these relations apply to links as well.

The proofs of the following propositions are left as an easy exercise.

Proposition 2. (i) Let R be a proof-net. Let A be the conclusion of a link v in R. The smallest substructure of R with A as a conclusion, denoted by st(A), or st(v), is characterized as the set of links w such that w ≪_{0} v, together with the edges adjacent to any such w.

Proposition 3. (i) A chain γ of type ⌈A, B⌉ in R or ⌊A, B⌋ has the form

CHAIN OF TYPE ⌈A, B⌉  CHAIN OF TYPE ⌊A, B⌋ w_{n+1} w_{1}  w_{n} . . . . . .  v_{n+1} v_{1} A  B …  B . . . . . . v_{n} … v_{1} Aw_{1}

where the w_{i} are Times or Cut links and the v_{j} are either axioms or links selected by a ∀-switch. In a chain of type ⌊A, B⌋ we have w_{i} ≫_{0} v_{i} ≪_{0} w_{i+1} for i ≤ n, and moreover A ≪_{0} w_{1}, B ≪_{0} w_{n+1}. Similar facts hold for chains of other types.

Proposition 4. (i) Let R be a proof-net containing the chains γ_{1} = path_{s′}(u, v) and γ_{2} = path_{s′′}(v, w) which are incident to v by different edges. Suppose it is not the case that

(§)  v is a par or for all link and s′ and s′′ disagree at v;

• If γ_{1} ∩ γ_{2} = {v} then there exists a chain γ = path_{s}(u, w), for some s, the concatenation of γ_{1} and γ_{2}, written γ = γ_{1} ∗ γ_{2};

• otherwise there exists a par or for all link v′ such that

γ_{1} = |u − γ_{1}^{1} − v′⌋ ∗ ⌈v′ − γ_{1}^{2} − v|, γ_{2} = |v − γ_{2}^{1} − v′⌉ ∗ ⌊v′ − γ_{2}^{2} − w|

and γ_{1}^{2} ∗ γ_{2}^{1} is a loop with exit v′.

2.5 Kingdoms and their Ordering

Lemma 1. If R a proof-net for MLL ^{−} with Mix and A ≪ B, then there exist chains γ of type |A, B⌉. Moreover we may assume that either A is a lower member of γ or γ is of type ⌊A, B⌉.

Proof. The argument is by induction on ≪. For the base case, let path_{s}(C, D) be any loop with exit v, say, a par link with conclusion C℘D. If A ∈ path_{s}(C, D), then obviously we have a chain |A − γ − C℘D⌉. Also if A ≪_{0} X ≪_{1} C℘D ≪_{0} B, then by choosing suitable switches we find a chain ⌊A − γ − B⌉.

Let C_{n} − γ_{n} − D_{n}, …, C_{0} − γ_{0} − D_{0} be loops with exits v_{n}, …, v_{0} such that

v_{n} ≪_{0} u_{n} ≪_{1} v_{n−1} ≪_{0} u_{n−1} … u_{0} ≪_{1} v_{0} ≪_{0} B.

By induction hypothesis we have a chain ⌊C_{n}℘D_{n} − γ − B⌉. We show that γ_{n} ∩ γ = {v_{n}}. Suppose not: starting from v_{n}, follow γ and let u be the first link in γ, different from v_{n}, such that u ∈ γ ∩ γ_{n}.

If case (§) of proposition 4 does not apply to u, then we have subchains \overline{γ_{n}} of γ_{n} and \overline{γ} of γ whose concatenation ⌈v_{n} − \overline{γ_{n}} ∗ \overline{γ} − v_{n}⌋ is cyclic, and this is impossible in a proof-net.

Therefore u is a par or for all link. It follows that the subchain \overline{γ} of γ from v_{n} to u is of type ⌊v_{n}, u⌉ and, moreover, that there is a lower link w ∈ γ_{n} such that u ≪_{0} w. But γ_{n} is a loop, and therefore we can find a subchain \overline{γ_{n}} of γ_{n} of type ⌊u, v_{n}⌉ such that \overline{γ_{n}} ∩ \overline{γ} = \{v_{n}, u\}. Thus \overline{γ} ∗ \overline{γ_{n}} is cyclic, again a contradiction.

Hence γ_{n} ∩ γ = ∅. The argument for the base case yields a subchain γ′ of γ_{n} of type |X, D_{n}℘E_{n}⌉ and the result is given by γ′ ∗ γ.

X  ℘ X_{n} ⊗ Y_{n}  ℘  ℘ X_{n}  Y_{n−1} X_{n−1} ⊗ Y_{n−1} Y_{0}  Y X_{0} ⊗ Y_{0}

Corollary. In a proof net for MLL^{−} + Mix the relation ≪ is an ordering.

Proof. If D_{0}℘E_{0} occurred in any of the loops γ_{0}, …, γ_{n−1}, then we would obtain a cyclic chain by taking D_{0}℘E_{0} for X.

Lemma 2. Let R be a proof net for MLL^{−} with Mix and let A be a formulaoccurrence in R. Then kA, the smallest normal subnet having A as a conclusion, exists and is characterized by the following equivalent conditions:

(a) the smallest set closed under the inductive conditions

(o) A ∈ kA.

(i) If v = \overline{X X^{⊥}}, then k(v) = kX = kX^{⊥}.

(ii) If v = \frac{X Y}{X ⊗ Y} then k(v) = k(X ⊗ Y) = kX ∪ kY ∪ \{X ⊗ Y \}.

(iii) If v = \frac{X Y}{X℘Y} then

k(v) = kX℘Y =⋃_{s} ⋃_{Z∈path_{s}(X,Y)} kZ ∪ {X℘Y }

where s ranges over all switchings of R;

=⋃_{⌈X−γ−Y ⌉} ⋃_{Z∈γ} kZ ∪ {X℘Y },

where γ ranges over loops.

(b) ⋃_{X≪A} st(X) ∪ st(A).

Proof. It is easy to see, by induction on ≪, that conditions (a) and (b) define the same set, call it kA: indeed

kA =st(A) ∪ ⋃_{X℘Y ⪯A} k(X℘Y)
=st(A) ∪ ⋃_{X℘Y ⪯A} ⋃_{Z∈⌈X−γ−Y ⌉} kZ

where γ ranges over loops

=st(A) ∪ ⋃_{X≪_{1}A} kX

from which the result follows by the induction hypothesis. Now the set (b) is clearly a substructure of R, hence (in MLL^{−} with Mix) it is a subnet of R. The fact that kA has A as a conclusion follows from the fact that ≪ is an order. It remains to show that kA is a normal subnet.

Let V and Z occur in S and let γ = path_{s}(V, Z) be any chain such that γ ⊄ kA. Starting from V, follow γ and let U be the first element such that U is in kA but the next element U′ is not. Similarly, continuing from U′ along γ, let W′ be the first element such that W′ does not belong to kA, but the next element W does. By Lemma 1 we have chains A − γ_{U} − U⌉ and A − γ_{W} − W ⌉; also we have a subchain ⌊U′ − \overline{γ} − W′⌋ of γ, and \overline{γ} is disjoint from γ_{U} and γ_{W}. By Proposition 4 the concatenation γ_{U} ∗ \overline{γ} ∗ γ_{W} yields a loop with exit in kA; but then \overline{γ} ⊂ kA and this is a contradiction. Hence kA is a normal subnet with A as a conclusion, indeed the smallest subnet with these properties, since conditions (a) must be satisfied by any normal subnet containing A.

Remark. In a proof-net the ordering ≪ can be read as the ordering of the kingdoms.

Lemma 3. Let R be a proof net for MLL^{−} + Mix and let A be a formulaoccurrence in R. Then eA (the largest normal subnet having A as a conclusion) exists and is characterized by the condition

(a)  {X : there is no chain |X, …, A⌋ in R }

Proof. Normal subnets with A as a conclusion exist, by Lemma 2. If there is a chain |X, …, A⌋ and S is a normal subnet containing X and A, then A cannot be a conclusion of S; hence every normal subnet with A as a conclusion is included in the set (a).

If a formula occurrence X is in the set (a), then all the hereditary premises of X and the axioms above them are in the set (a); therefore the set (a) is a substructure of R, hence (in MLL^{−} + Mix) it is a subnet. To see that the set (a) is normal, let X and Y be distinct formula occurrences in R and let |X − γ − Y | be a chain such that for some link w in γ we have W ∉ (a). This means that there is a chain γ′ of type |w, A⌋. We may assume that γ ∩ γ′ = {w}, (otherwise we take a subchain of γ′) and that γ is the concatenation

γ = |X − γ_{X} − w⌉ ∗ ⌊w − γ_{Y} − Y |

If γ′ has type ⌊w, A⌋, then γ_{X} ∗ γ′ is a chain of type |X, A⌋. If γ′ has type ⌈w, A⌋, then γ_{Y} ∗ γ′ is a chain of type |Y, A⌋. In both cases we contradict the fact that X and Y belong to the set (a).

2.6 The Sequentialization theorem

Since the structure of kingdoms and empires in MLL^{−} is different from that in MLL^{−} with Mix, a different proof of the sequentialization theorem is needed from the standard one for MLL^{−} (see, e.g., [9], section 2.4, pp. 259). The following argument is essentially the same as the one given in [5]; an original feature of our proof is the fact that we do not reduce the problem to the case of MLL^{−} without Mix. A novelty here is the use of the properties of kingdoms and empires in MLL^{−} with Mix. The general structure of the argument differs from that by Fleury and Retoré [17], despite similarities with parts of their proof.

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

Proof. By induction on the size of R. The following case is trivial: Case 1. (i) R is an axiom; (ii) R consists of two proof structures without axiomatic connections with each others (just apply the inductive hypothesis to them and then use the rule of Mix); (iii) one of the lowermost links of R is a par, for all link or an exists link whose premise contains no eigenvariable: just remove such a link, apply the inductive hypothesis and use the par, for all or exists rule of the sequent calculus).

Case 2. Otherwise, we may assume that among the lowermost links of R there are Cut, times or exists links, but no par or for all links. Consider a times (or Cut) link

v : \frac{A B}{A ⊗ B} , A ⊗ B ∈ Γ

maximal with respect to ≪ (the case of an exists links is entirely similar).

Subcase 2.1 The link v is splitting, i.e., its removal yields two disconnected proof structures; apply the induction hypothesis to them and then use the Times rule of the sequent calculus.

Unlike the case of MLL^{−}, in MLL^{−} with Mix a link maximal with respect to ≪ need not be splitting. For instance, there may be a sequence of chains of the forms

⌈A − γ_{A} − C_{0}⌉, ⌈D_{0} − γ_{1} − C_{1}⌉, …, ⌈D_{n−1} − γ_{n} − C_{n}⌉, ⌈D_{n} − γ_{B} − B⌉

with links L′_{i} : \frac{C_{i} D_{i}}{C_{i}℘D_{i}} for i ≤ n, where γ_{1}, …, γ_{n} are in e(A)∩e(B); clearly in this case we cannot split R by removing the link L_{0} with conclusion A ⊗ B.

In [5] this situation was described as “A ⊗ B is inside a maze”. We claim that in any case we can find a splitting link L^{∗}.

Subcase 2.2 The given link v is not splitting. Let

G_{A} = ⋃{γ : γ is a chain of type ⌈A, |}
G_{B} = ⋃{γ : γ is a chain of type ⌈B, |}

Notice that if γ ∈ G_{A} and γ′ ∈ G_{B}, then γ ∩ γ′ = ∅; otherwise, follow γ starting from A and let u be the first link in γ ∩ γ′. If u does not satisfy condition (§) of proposition 4, then we can obtain a cyclic chain; if u does satisfy condition (§), then A ⊗ B cannot be maximal with respect to ≪.

Furthermore, notice that any chain ⌈B, X| can be extended to a chain ⌊A, X| including the times link v, and conversely, every chain ⌊A, X| can be reduced to a chain ⌈B, …, X|. Since

eA ∩ eB = {X : there is no chain of type ⌊A, X| nor of type ⌊B, X|}

and R is a proof-net, it follows that the following is a partition of R

R = G_{A} ∪ G_{B} ∪ (eA ∩ eB) ∪ {A ⊗ B}.

Since by the hypothesis of the subcase R cannot be decomposed in two disconnected proof-structures, eA ∩ eB is nonempty. Now suppose we have a chain ⌈A − γ_{A} − u⌉ and a chain ⌈u − γ_{1} − z| such that γ_{1} ⊂ e(A) ∩ e(B) and u satisfies property (§) (Proposition 4), e.g., u is a par link with conclusion C_{0}℘D_{0}.

Let v_{0} be the lowermost link of the proof-net such that u ≺ v_{0}: by the assumption of the case, v_{0} is a times, cut or exists link.

Subcase 2.2.1 If v_{0} is also maximal with respect to ≪, then we repeat the argument of Case 2, applied to v_{0}. Notice that the chain γ_{A} is extended to a chain ⌈v − γ′ − v_{0}⌉.

Subcase 2.2.2 If v_{0} is not maximal with respect to ≪, then it belongs to a loop with exit u_{1}. Consider the lowermost link v_{1} of the proof-structure such that u_{1} ≺ v_{1}: by the assumption of the case, v_{1} is a times, cut or exists link. Since v_{0} is in a loop, clearly there is a chain ⌊u − γ^{+} − v_{1}⌉. We claim that γ_{A} ∩ γ^{+} = {u} so that the chain γ_{A} ∗ γ^{+} properly extends γ_{A}.

Suppose the claim fails. Following γ_{A} starting from u, let w be the first link different from u such that w ∈ γ_{A} ∩γ^{+}. By proposition 4, u is the exit of a loop; such a loop is the concatenation of a subchain of γ_{A} and of a subchain of γ^{+}. More precisely, γ_{A} splits as γ_{A,1} ∗ γ_{A,2}, with ⌈w − γ_{A,2} − u⌉ and the loop in question is γ_{A,2} ∗ \overline{γ^{+}}, where ⌊u − \overline{γ^{+}} − w⌉ is a subchain of γ^{+}. It follows that γ_{A,1} is of type ⌈v, w⌋. But then the concatenation

⌈v − γ_{A,1} − w⌋ ∗ ⌈w − \overline{γ^{+}} − u⌋ ∗ ⌈u − γ_{1} − z|

belongs to G_{A} and this implies that γ_{1} is not in e(B).

A  B ⊗  w  u  γ_{1} \overline{γ^{+}} γ_{A,2} γ_{A,1} v  v_{0}

The claim is proved. Since in passing from v to v_{0} and to v_{1} we extend the chain starting from A, and since R is finite, the process must eventually terminate in a link v^{∗} which is maximal with respect to ≪ and “not in a maze”.

Theorem 2. (Permutability of Inferences) (i) Let D and D′ be a pair of derivation of the same sequent ⊢ Γ in propositional MLL^{−} + Mix. 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. Part (ii) is an immediate consequence of the definition of normal subnet and of the sequentialization theorem (generalized to proof-nets with non-logical axioms). Part (i) is obvious in the if case. The only if case is proved by induction on the size of the proof-net R such that (D)^{−} = R = (D′)^{−}.

First notice if B is any subderivation of D, then (B)^{−} is a normal subnet of R; hence given a chain ⌈A − γ − B⌉ in R, if A, B ∈ (B)^{−} then also γ ⊂ (B)^{−}.

Now 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 the inferences in this branch. Otherwise, let I, I′ be the inferences immediately above I_{0} in D and in D′, respectively, and let B and B′ be the subderivations of D and D′ ending with I and I′, respectively.

Case 1. Both I and I′ are Mix rules. Thus B and B′ have the forms

I : \begin{matrix}B_{1} ; ⋮ . ; ⊢ Γ_{1}, Γ_{2} & B_{2} ; ⋮ . ; ⊢ Γ_{3}, Γ_{4} \\ ⊢ Γ \end{matrix} I′ : \begin{matrix}B′_{1} ; ⋮ . ; ⊢ Γ_{1}, Γ_{3} & B′_{2} ; ⋮ . ; ⊢ Γ_{2}, Γ_{4} \\ ⊢ Γ \end{matrix}

respectively, where Γ = Γ_{1}, Γ_{2}, Γ_{3}, Γ_{4} and one of the Γ_{i} may be empty. Consider the subnets

{S_{1} \atop Γ_{1}} = (B_{1})^{−} ∩ (B′_{1})^{−}  and  {S_{2} \atop Γ_{2}} = (B_{1})^{−} ∩ (B′_{2})^{−}.

We claim that S_{1} and S_{2} are disjoint. In fact, in R there can be no axiom link connecting hereditary premises of Γ_{1} and Γ_{2} nor any chain with Cuts as lower members connecting Γ_{1} and Γ_{2}: this holds since (B′)^{−} is a normal subnet of R in which the hereditary premises of Γ_{1} and Γ_{2} belong to two separated proof-nets (B′_{1})^{−} and (B′_{2})^{−}. By the same argument we have two disjoint subnets S_{3} and S_{4} with conclusions Γ_{3} and Γ_{4}, respectively.

By the sequentialization theorem we have derivations D_{1}, …, D_{4} such that S_{i} = (D_{i})^{−} and

D_{1,2} M_{1} : \begin{matrix}D_{1} ; ⋮ . ; ⊢ Γ_{1} & D_{2} ; ⋮ . ; ⊢ Γ_{2} \\ ⊢ Γ_{1}, Γ_{2} \end{matrix} D_{3,4} M_{2} : \begin{matrix}D_{3} ; ⋮ . ; ⊢ Γ_{3} & D_{4} ; ⋮ . ; ⊢ Γ_{4} \\ ⊢ Γ_{3}, Γ_{4} \end{matrix}

are derivations ending with Mixes; by induction hypothesis, D_{1,2} can be obtained from B_{1} and D_{3,4} can be obtained from B_{2} by successive permutations of inferences.

If we repeat exactly the same argument for B′, we obtain derivations

D_{1,3} M_{3} : \begin{matrix}D_{1} ; ⋮ . ; ⊢ Γ_{1} & D_{3} ; ⋮ . ; ⊢ Γ_{3} \\ ⊢ Γ_{1}, Γ_{3} \end{matrix} D_{2,4} M_{4} : \begin{matrix}D_{2} ; ⋮ . ; ⊢ Γ_{2} & D_{4} ; ⋮ . ; ⊢ Γ_{4} \\ ⊢ Γ_{2}, Γ_{4} \end{matrix}

such that D_{1,3} can be obtained from B′_{1} and D_{2,4} can be obtained from B′_{2} by successive permutations of inferences. Now it is evident that by successive permutations of the mixes M_{3} and M_{4} with I′ we identify

I : \frac{D_{1,2} D_{3,4}}{⊢ Γ} and I′ : \frac{D_{1,3} D_{2,4}}{⊢ Γ}

Case 2. One of I, I′ is not a Mix, say I. Let I have principal formula A and let I′_{A} be the inference of D′ corresponding to the same link of R as I; 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).

If A = A_{1}℘A_{2}, then the par rule I_{A} clearly can be permuted below I′_{1}, …, I′_{k}, as required.

If A = A_{1} ⊗ A_{2} and I′_{A} cannot be permuted below some I′_{i} it must be the case that I′_{i} is a par rule, say, with principal formula B. Let I_{B} be the inference of D which corresponds to the same link of R as I′_{i}. Now I_{B} occurs above the inference I_{0}, by our assumption that D and D′ agree in the given branch up to I_{0}; hence the subderivation D_{B} of D ending with I_{B} is a proper subderivation of B and does not contain I; hence A ∉ k(B), since A ∉ (D_{B})^{−}.

Let D′_{B} be the subderivation of D′ ending with I′_{i}. By part (ii) of the theorem and induction hypothesis, D′_{B} can be transformed by successive permutations of inferences into a derivation D^{∗} where the inference with principal formula B occurs above that with principal formula A: namely, B^{∗} contains a proper subderivation B^{∗∗} with (B^{∗∗})^{−} = k(B) and therefore we may suppose the last inference of B^{∗} has principal formula A.

If A = cut or if A = ∀x.A_{1} the argument is similar. By repeating the argument, we eventually permute A below I′_{k}, as required.

3 Asperti’s concurrent processes

We consider a variant of Asperti’s token game [3]; the original formulation by Asperti is in terms of Petri Nets; we speak informally of trips of tokens in a proof-structure and regard this condition as the right generalization of Girard’s no-short-trip condition to the case of MLL^{−} + Mix.

There are tokens of type ↑ and ↓. There is a Left or Right switches on each times link (Asperti’s switching). Given a multiplicative proof-structure R, in the initial position we have a token of type ↑ on each conclusion of R; the game succeeds if it reaches the terminal position where there is a token of type ↓ on each conclusion of R; the permissible movements of the tokens are those in accordance with the following instructions:

• case of an axiom link \overline{A A^{⊥}}:

from a pair ↑A, ↑A^{⊥} go to the pair ↓A, ↓A^{⊥}

• case of a par link \frac{A B}{A℘B}:

from ↑A℘B go to the pair ↑A, ↑B;
from the pair ↓A, ↓B, go to ↓A℘B;

• case of a times link \frac{A B}{A ⊗ B}:

Right Switch  Left Switch
(1) from ↑A ⊗ B, go to ↑B  from ↑A ⊗ B, go to ↑A
(2) from ↓B, go to ↑A from ↓A, go to ↑B
(2) from ↓A, go to ↓A ⊗ B  from ↓B, go to ↓A ⊗ B

The case of cut is identical to that of a times link.

Definitions. (i) A deadlock for a given switching is a position of the tokens which is reachable from the initial position from which the game cannot successfully terminate.

(ii) Given a proof-structure and a switching for the Asperti game, a causal path or causal chain is a path of n + 1 edges together with n transitions such that the transition t_{i} takes a token from the edge e_{i−1} and puts a token in the edge e_{i}. A causal path is cyclic if the edges A_{1} and A_{n+1} coincide. A causal path where the first transition is of the form ↑A and the last is ↑B is said of type ↑A, ↑B; similarly for the types ↑A, ↓B, etc.

Asperti’s Theorem. A propositional proof-structure is a proof-net if and only if for every A-switching there is no deadlock in Asperti’s game.

To prove Asperti’s theorem, the following facts are needed. Given a proofstructure and a switching for the Asperti game, let M_{0} and M_{T} denote the initial and terminal successful position, respectively.

Proposition A-1. (i) In any computation M_{0} ⇒ M′ every transition can be fired at most once.

(ii) We cannot have infinite computations starting from M_{0}.

(iii) In any computation M_{0} ⇒ M_{T} every transition is fired exactly once.

Proof. Exercise (see [3], 3.13, 3.15, 3.16).

Proposition A-2. In some computation M_{0} ⇒ M′ there is a deadlock if and only if there is a cyclic causal path if and only if in R there is a cyclic chain.

Proof. Exercise (see [3], Theorem 3.24).

Finally, notice that an Asperti game is reversible: the dual of a given transition is obtained by changing the kind of the tokens, by choosing the opposite switch in the case of a times link and by performing the transition in the reverse order; notice that the dual of a transition is a transition. Finally, the dual of an Asperti game is obtained by performing the dual transitions in the reverse order.

Proposition A-3. The dual of an Asperti game is an Asperti game.

Proof. Exercise (see [3], 3.20.

In the process interpretation, a causal path ↑ A, ↑ B for a certain Aswitching s means that under the restrictions on the order of the execution of the processes, induced by s, the activation of A must precede the activation of B or, in other terms, there is a causal dependency between the activations of those processes. The proofs of propositions A-2 and A-3 yield the following

Corollary. Chains are related to causal dependencies between processes as follows:

• the termination of A [B] may depend on the activation of B [A] if and only if there exists a chain of type |A, B|.

• the activation of A [B] may depend on the termination of B [A] if and only if there exists a chain of type ⌊A, B⌋;

• the activation of A may depend on the activation of B if and only if there exists a chain of type ⌊A, B|; dually,

• the termination of A may depend of the termination of B if and only if there exists a chain of type |A, B⌋.

Also the empire of a formula A in a proof-net has the following characterization (see [3], the Remark after Proposition 4.10.):

eA = {X : the activation of A cannot depend on the activation of X}

3.1 Asperti’s Correctness Condition, First-order Case

The main technical idea in Girard’s treatment of quantifiers [19] is to define D-R-graphs so that the conclusion of a for all link may be alternatively connected either to the premise of the link or to any other formula containing the eigenvariable associated with that link. Given the characterization of the empires in Lemma 3, the requirement that such a D-R-graph should be acyclic implies that an eigenvariable associated with a for all link cannot occur outside the empire of the premise of such a link. The refinement in [9], requiring the strictest possible use of eigenvariables, implies that an eigenvariable cannot occur outside the kingdom of the premise of its associated link.

We extend Asperti’s characterization of proof-nets to the first-order case.^{2} The restriction on the eigenvariables is interpreted here as a syncronization requirement. The resulting correctness condition seems more intuitive than the official one using for all switchings.

To a proof-structures we associate a list of global variables which is empty at the beginning of the verification of the correctness condition. Asperti’s games are defined as before, with the addition of the following cases:

• case of a for all link \frac{A}{∀x.A}:

from ↑∀x.A go to ↑A;

and add x to the list of global variables;

from ↓A, go to ↓∀x.A;

• case of an exists link \frac{A[t/x]}{∃x.A}:

from ↑∃x.A go to ↑A[t/x]

if every eigenvariable occurring in t occurs already in the list of global variables;

from ↓A[t/x], go to ↓∃x.A.

• case of a cut link \frac{A A^{⊥}}{cut} :

as in the case of times link, except that the transition from ↑cut is not activated unless every eigenvariable occurring in A already occurs in the list of global variables.

2This section results from a discussion with A.Fleury.

Theorem 3. A first-order proof-structure R is a proof-net if and only if for every A-switching there is no deadlock in Asperti’s game for R.

Sketch of proof. The restriction on the exists case, i.e., the synchronization of an exists process with a for all process, may be regarded as a transition rule

from ↑∀x.A and ↑∃y.B to ↑B[t/y]

Clearly this corresponds to the chain ⌊B[t/y], ∀x.A⌉, in the sense that if v and w are the for all and exists links in question, then the transition from ↑ ∀x.A to ↑ B[t/y] may be regarded as passing through the edge between v and w in the D-R-graph determined by a switch for ∀x.A. A similar remark applies to the restriction on the cut process.

As in the propositional case, we must prove Proposition A-2. Using the previous paragraph, it can be shown that if there is a deadlock, then there is a cyclic causal path and this may be regarded as a cyclic chain. Conversely, if there is a cyclic chain, then first apply the Proposition 5 below and consider a cyclic chain where the conclusions of every for all links are connected to an exists or cut link. Now consider a D-R-switching s yielding a chain γ of type ⌊v, w|, where v has ∀x.A as a conclusion and w has B[t/y] as a premise, which becomes cyclic when we add the edge induced by the switch s(v) = w, so that the eigenvariable x must occur in t. By induction on γ we find an A-switching which determines a causal path from ↑B[t/y] to ↑∀x.A; i.e. the activation of ∀x.A depends on the activation of B[t/y]. But the transition from ↑∃y.B to ↑B[t/y], where t contains x, is permissible only if x is already declared a global variable, and this requires that ↑ ∀x.A has already been reached: thus the activation of B[t/y] depends on the activation of ∀x.A and this is a deadlock.

Proposition 5. Let R be a first-order proof-structure. If in R there is a cyclic chain, then we can find a cyclic chain where every for all switch selects either the premise of its link or the premise of an exists link or the premise of a Cut.

Proof. Suppose sR contains a cycle γ, ∀x.A is in γ and s(∀x.A) = B. If B is the premise of a link v which is not an exists link, let C be the conclusion of v. We can certainly modify s to an s′ where s′(∀x.A) = C and s′R still contains a cycle. Indeed, suppose v is a par or for all link and s(C) ≠ B: if C also belongs to γ, then by letting s′ be like s except for s′(∀x.A) = C we obtain a cycle in s′R shorter than γ; if C does not belong to γ, then we may let s′ be like s except for s′(∀x.A) = C and s(C) = B and still obtain a cycle in s′R. Repeating this process, we obtain a switching s^{∗} with a cyclic s^{∗}(R) where s^{∗}(B) is either a premise of an exists link, or of a Cut, as required.

Example. The solid arrows indicate the mutual causal dependency.

A^{⊥}(x, y)  A(x, y) ∃  ∃ ∀y.A(x, y) ∃x.∀y.A(x, y) ∀x.A^{⊥}(x, y) ∃y.∀x.A^{⊥}(x, y) ∀  ∀

4 Full Intuitionistic Linear Logic

In previous work by G.Bellin and J. van de Wiele (see [8], section 5.4) it has been shown that each sequent derivation of multiplicative intuitionistic linear logic ILL can be represented as a classical proof-net of MLL^{−} together with an Input-Output orientation; conversely, each proof-net for MLL^{−} corresponds to a set of sequent derivations in ILL, where each translation from MLL^{−} to ILL is determined by an I-O orientation satisfying certain conditions. Moreover, suitable orientations are related to D-R-graphs, in particular in the case of a cut-free proof-net each D-R-graph determines a suitable orientation.

In this section we show how to extend this result to MLL^{−} with Mix.^{3} It turns out that the right intuitionistic system for this purpose is Full Intuitionistic Linear Logic FILL introduced by M. Hyland and V. de Paiva [20]. We will not discuss the considerations of categorical logic which motivate Hyland and de Paiva’s work. We consider only the multiplicative fragment of FILL.

3The question what fragment of intuitionistic linear logic could be represented in MLL^{−} + Mix by an extension of the I-O-translations for MLL^{−} was asked by P. Scott to the author in private communication.

The language of this fragment has the connectives ⊗ (times), ℘ (par), −∘ (linear implication) and their units, the propositional constants ⊥ and 1 for falsity and truth. We use the same symbols as in classical linear logic, although the meaning is obviously different. Linear negation is defined as A^{⊥} =_{df} A −∘ ⊥.

The consequence relation of FILL is classical linear ; thus sequents have the form Γ ⊢ Δ, where Δ may contain several occurrences of formulas.

4.1 Term Calculus for Multiplicative FILL

We give here the basic definitions of de Paiva and Hyland’s term calculus.

Definitions. (i) Given a set X of variables and constant terms ∘, −, define the set P_{X} of patterns with variables in X by the inductive clauses

x ⊗ y ∈ P_{{x,y}} x ℘ − ∈ P_{{x}} − ℘ y ∈ P_{{x}}

Then define the set T_{X} of linear terms with variables in X inductively as follows:

• ∘ ∈ T_{{}}, − ∈ T_{{}};

• x ∈ T_{{x}};

• t ∈ T_{X}, u ∈ T_{Y}, X ∩ Y = ∅ implies tu ∈ T_{X∪Y};

• t ∈ T_{X∪{x}}, x ∉ T_{X} implies λx.t ∈ T_{X};

• t ∈ T_{X}, u ∈ T_{Y}, X ∩ Y = ∅ implies t ⊗ u, t℘u ∈ T_{X∪Y};

• t ∈ T_{X}, p ∈ P_{Y}, e ∈ T_{Y ∪Z}, X ∩ Z = ∅, Y ∩ Z = ∅ implies let t be p in e ∈ T_{X∪Z}.

(ii) The sequent calculus rules with the associated term assignment are as follows. We use \overline{x}, \overline{y}, \overline{z}, \overline{v} \overline{f} for sequences of variables, \overline{r}, \overline{s}, \overline{t}, \overline{u} for sequences of terms. If \overline{f} is the sequence of terms f_{1}, …, f_{n}, then \overline{f}[t/x] is the sequence f_{1}[t/x], …, f_{n}[/x].

If \overline{x} and \overline{y} are the variables occurring in the premises of a two-premised sequent rule, then it is understood that no variable in \overline{x} occurs in \overline{y} and viceversa.

Identity

Axiom : x : A ⊢ x : A Cut : \frac{\overline{x} : Γ ⊢ \overline{u} : Δ, t : A x : A, \overline{y} : Π ⊢ \overline{f} : Λ}{\overline{x} : Γ, \overline{y} : Π ⊢ \overline{u} : Δ, \overline{f}[t/x] : Λ}

Times

⊗ − R : \frac{\overline{x} : Γ ⊢ \overline{r} : Δ, t : A \overline{y} : Π ⊢ \overline{s} : Λ, u : B}{\overline{x} : Γ, \overline{y} : Π ⊢ \overline{r} : Δ, \overline{s} : Λ, t ⊗ u : A ⊗ B}

⊗ − L : \frac{\overline{v} : Γ, x : A, y : B ⊢ \overline{t} : Δ}{\overline{v} : Γ, z : A ⊗ B ⊢ \overline{t′} : Δ}

where for each t′_{i} ∈ \overline{t′} we have

t′_{i} = \{ \begin{matrix}let z be x ⊗ y in t_{i}, & if x or y occurs in t_{i}; \\ t_{i}, & otherwise. \end{matrix}

Par

℘ − R : \frac{\overline{x} : Γ ⊢ x : A, y : B, \overline{u} : Δ}{\overline{x} : Γ, ⊢ x ℘ y : A℘B, \overline{u} : Δ}

℘ − L : \frac{\overline{x} : Γ, x : A ⊢ \overline{r} : Δ \overline{y} : Π, y : B ⊢ \overline{s} : Λ}{\overline{x} : Γ, \overline{y} : Π, z : A℘B ⊢ \overline{r′} : Δ, \overline{s′} : Λ}

where for each r′_{i} ∈ \overline{r′} we have

r′_{i} = \{ \begin{matrix}let z be x ℘ − inr_{i}, & if x occurs in r_{i} \\ r_{i}, & otherwise. \end{matrix}

and for each s′_{j} ∈ \overline{s′} we have

s′_{j} = \{ \begin{matrix}let z be − ℘ y in r_{i}, & if y occurs in s_{j} \\ s_{j}, & otherwise. \end{matrix}

Linear Implication

−∘ − R : \frac{\overline{x} : Γ, x : A ⊢ t : B, \overline{u} : Δ}{\overline{x} : Γ ⊢ λx.t : A −∘ B, \overline{u} : Δ} where x does not occur in \overline{u}.

−∘ − L : \frac{\overline{x} : Γ ⊢ \overline{r} : Δ, t : A x : B, \overline{y} : Π ⊢ \overline{s} : Λ}{\overline{x} : Γ, f : A −∘ B, \overline{y} : Π ⊢ \overline{r} : Δ, \overline{s}[f(a)/x] : Λ}

Structural Rules

The term assignments for the rules Mix, Exchange Left and Right are straightforward. For instance, in the case of Mix we have

Mix : \frac{\overline{x} : Γ ⊢ \overline{t} : Δ \overline{y} : Π ⊢ \overline{u} : Λ}{\overline{x} : Γ, \overline{y} : Π ⊢ \overline{t} : Δ, \overline{u} : Λ}

where \overline{x} ∩ \overline{y} = ∅, as indicated above.

Multiplicative Propositional Constants

Axiom : ⊢ ∘ : 1 1 − L : \frac{\overline{x} : Γ ⊢ \overline{u} : Δ}{− : 1, \overline{x} : Γ ⊢ \overline{u} : Δ}

Axiom : x : ⊥ ⊢ ⊥ − R : \frac{\overline{x} : Γ ⊢ \overline{u} : Δ}{\overline{x} : Γ ⊢ \overline{u} : Δ, − : ⊥}

4.2 Proof-nets with Orientations.

The consideration of the units is essential in the logic FILL, although it makes sense to consider the subsystem FILL^{−} with the axioms 1-right and ⊥-left, but without the rules 1-left and ⊥-right. To represent FILL + Mix in MLL + Mix, with the propositional constants 1 and ⊥, one considers proof-nets with links of the form

1 − axiom: \overline{1} ⊥ − axiom: \overline{⊥}

where the ⊥-axioms are attached to other links \overline{⊥} ⇁ v in correspondence with

a Weakening: \frac{⊢ Γ}{⊢ Γ, ⊥}. An attachment induces an edge in every D-R-graph.

We have the reduction:

1-Reductions

1 ⊥ ⇁ X  reduces to X
⋮  ⋮

For the reasons given in the preface, the theory of proof-nets for such a system is not fully satisfactory; however, almost all the basic results hold modulo a given choice of attachments. In a sequent derivation we can permute the ⊥-rule downwards, unless its principal formula becomes active in another inference; this corresponds to attaching the ⊥-axiom as low as possible and gives a sort of “normal form” for the attachment. On the other hand, we can always permute the ⊥-rule upwards, but in the case of a times or mix inference the choice of the branch is arbitrary; thus the notion of kingdom of a ⊥-axiom is not well defined.

Definition. (i) Given such a proof net S, an orientation is a map δ : S → {O, I} satisfying the following restrictions:

axiom:(0) \overline{O I}  \overline{I O}

tensor: (1) \frac{O I}{I}  (2)\frac{I O}{I}  (3)\frac{O O}{O}  (4) \frac{I I}{I}

par: (5) \frac{I O}{O}  (6)\frac{O I}{O}  (7) \frac{I I}{I}  (8)\frac{O O}{O}

For the units we have all possibilities δ(1) = I, O, δ(⊥) = I, O. We write A_{I}, A_{O} for δ(A) = I, δ(A) = O, respectively.

(ii) An orientation δ : S → {O, I} has a deadlock if it makes the assignments

\frac{A_{I} A_{I}^{⊥}}{cut} or \frac{A_{O} A_{O}^{⊥}}{cut} to some cut link; it is deadlock-free otherwise. If a proof-

net S reduces to S′ by a cut-reduction, then an orientation δ : S → {O, I} when restricted to S′ is still an orientation. It is easy to see (e.g., in case the links immediately above a cut have orientations (2) and (5) above) that δ : S → {O, I} may be deadlock-free, but not δ : S′ → {O, I}.

(iii) An orientation δ : S → {O, I} is computationally consistent if no sequence of cut reductions yields an orientation with a deadlock.

We can extend the map ( )^{−} of Theorem 1 so that, given a sequent derivation D in multiplicative FILL + Mix, we obtain a proof-net with orientation (D)^{−} = δ : R → {O, I}. The only question is: what condition should correspond to the restriction on the implication introduction rule?

Definitions. Let δ : R → {I, O} be a proof-net for MLL^{−} + Mix with orientation.

(i) A chain γ is directed if it does not pass through an attachment and for every times link L which occurs in γ

1. if L is a lower times link, then it has one of the orientations

(1) \frac{O I}{I} or (2) \frac{I O}{I};

2. if L is not a lower link, then the two formula occurrences X_{i} and X_{0} ⊗ X_{1} which belong to γ have the same orientation.

(ii) A par link with orientation (5) \frac{I O}{O} or (6) \frac{O I}{O} will be called an

implication. Let L be \frac{A_{I} B_{O}}{(A℘B)_{O}}: the orientation δ : R → \{I, O\} makes the

implication L functional if for every directed chain of type ⌈A_{I}, C_{O}⌉ where C is a door of e(A) we have that C is precisely the formula occurrence B.

(iii) We say that δ : R → {I, O} is a proof-net for multiplicative FILL + Mix if R is proof-net for MLL + Mix and δ is a computationally consistent orientation which makes all implications functional.

Remark. It is easy to see that if γ is a directed chain of type ⌈A_{I}, B_{O}⌉ and

L: \frac{C_{O} D_{I}}{(C ⊗ D)_{I}} is a lower link of the chain, then γ consists of the subchains

⌈A_{I}, C_{O}⌉ and ⌈D_{I}, B_{O}⌉ connected by L.

Example.

c′ : C_{O}^{⊥} b′ : B_{O}^{⊥}

a : A_{I} b : B_{I}  e : (C^{⊥}℘B^{⊥})_{O}  d : D_{I}^{⊥}
z′ : (A ⊗ B)_{I} c : C_{I}  f : ((C^{⊥}℘B^{⊥}) ⊗ D^{⊥})_{I}  f(e) : D_{O}
z : ((A ⊗ B) ⊗ C)_{I}  λf.f(e) : (((C^{⊥}℘B^{⊥}) ⊗ D^{⊥})℘D)_{O}
t : A_{O}^{⊥}  λzf.f(e) : (((A ⊗ B) ⊗ C)℘(((C^{⊥}℘B^{⊥}) ⊗ D^{⊥})℘D))_{O}

(The term assignment arises from the attempted translation into FILL.) Of the two implications in the example, the higher one is functional, since there is only one directed chain ⌈((C^{⊥}℘B^{⊥})⊗D^{⊥})_{I}, D_{O}⌉ between its premises, but the lower one is not, because of the directed chain ⌈((A ⊗ B) ⊗ C)_{I}, A_{O}^{⊥}⌉. Indeed, letting

t = let z be z_{1}℘− in (let z_{1} be a℘− in a),
b′ = let z be z_{1}℘− in (let z_{1} be −℘b in b),

c′ = let z be −℘c in c e = c′℘b′

we have that

z : (A^{⊥}℘B^{⊥})℘C^{⊥} ⊢ t : A^{⊥}, λf.f(e) : ((C^{⊥}℘D^{⊥}) −∘ D) −∘ D

is provable in multiplicative FILL, but

⊢ t : A^{⊥}, λzf.f(e) : (A^{⊥}℘B^{⊥})℘C^{⊥} −∘ ((C^{⊥}℘D^{⊥}) −∘ D) −∘ D

is not. The general case is given by the following result.

Lemma 4. Let D be a derivation in multiplicative FILL + Mix of \overline{v} : Γ ⊢ \overline{t} : Δ and let (D)^{−} = δ : R → \{I, O\}. For each v_{i} : C_{i} in \overline{v} and every t_{j} : D_{j} in \overline{t}, v_{i} occurs in t_{j} if and only if there exists a directed chain ⌈C_{i}, D_{j}⌉ in (D)^{−}.

Proof. By induction on D. If D is an axiom the result is clear. If the last inference of D is Mix, the result is immediate from the inductive hypothesis and the fact that the variables occurring in different branches of a derivation are distinct. If the last inference is ⊥-right or 1-left, then the term assignments to the passive formulas are unchanged and the directed chains in D^{−} do not propagate through the new attachment. If the last inference of D is Times Left or Par Left, then the variable z : A ∘ B assigned to the principal formula occurs in the term t′ : D in the succedent of the conclusion if and only if one of the variables x : A or y : B occurs in t : D in the succedent of the premise. By induction hypothesis this is the case if and only if there is a directed chain of type ⌈A, D⌉ or ⌈B, D⌉ in (D)^{−} if and only if there is a directed chain of type ⌈A ∘ B, D⌉. The cases when the last inference of D is Times Right or Par Right or Linear Implication Right are similar.

Now suppose the last inference of D is Linear Implication Left. If the variable v and the term t are both assigned to passive formulas and have immediate ancestors in the same branch of the derivation, then the result is immediate from the induction hypothesis.

Fon any passive formula L in the succedent of the conclusion, the variable f : A −∘ B occurs in w : L if and only if w = s[f(t)/x] if and only if there is a directed chain ⌈B_{I}, L_{O}⌉ if and only if there is a directed chain ⌈(A⊗B)_{I}, L_{O}⌉.

For any passive formula C in the antecedent of the left premise and any passive formula L in the succedent of the right premise, the variable v : C occurs in the term w : L if and only if w is s[f(t)/x] and v occurs in t if and only if there are chains ⌈C_{I}, A_{O}⌉ and ⌈B_{I}, L_{O}⌉ connected by the link

\frac{A_{O} B_{I}}{(A ⊗ B)_{I}}.

Finally, for any passive formula P in the antecedent of the right premise and any passive formula D in the succedent of the left premise, the variable y : P does not occur in the term r : D and any chain ⌈P, D⌉ cannot be directed, since it must consist of two disjoint subchains of types ⌈P_{I}, B_{I}⌉ and

⌈A_{O}, D_{O}⌉ connected by the link \frac{A_{O} B_{I}}{(A ⊗ B)_{I}}, and by the above Remark this is

impossible in a directed chain. The case of Cut is similar.

We need also the following fact.

Proposition 6. Let R be a proof-net for MLL + Mix and let δ : R → {I, O} be an orientation satisfying as in (0) - (8) above and let C be a conclusion of R such that δ(C) = I. Every maximal directed chain starting from C_{I} has one of the forms

(o) ⌈C_{I}, …, D_{O}⌉ or (i) ⌈C_{I}, …, 1_{I}⌋

where D is a conclusion of R and \overline{1} is an axiom.

Proof. A directed chain path_{s} is obtained by determining the switching s according to the orientation as follows.

1. Start from C_{I} and proceed upwards.

2. Going up, always remain within formulas marked I, fixing the switching, if necessary, so that from a conclusion marked I the path reaches a premise marked I. The step is determined in cases (1) and (2) (times); an arbitrary choice is made in cases (4) (times) and (7) (par links).

3. At an axiom or cut, change the direction.

4. Going down, remain within formulas marked O whenever possible; namely, proceed from a premise marked O to the conclusion marked O in cases (3) (times links) (5) and (6) and (8) (par) fixing the switching accordingly.

5. If going down a times link is reached with conclusion marked I (cases (1) and (2)), then from the premise marked O proceed up to the premise marked I and continues as in step 2.

Since every path is acyclic, the process terminates, either (i) going downwards at a conclusion D_{O} or (ii) going upwards at a link \overline{1_{I}}, as claimed.

The proof of the sequentialization theorem for FILL^{−} + Mix is essentially the same as the proof for MLL^{−} + Mix. It is in the treatment of the axioms ⊥ ⊢ of FILL that the specific graph theoretic analysis contained in the proof becomes necessary.

Theorem 3. There exists a “context forgetting” map ( )^{−} from sequent derivations in first-order multiplicative FILL + Mix to proof-nets for FILL + Mix with the following properties:

(a) Let D be a derivation of \overline{x} : Γ ⊢ \overline{t} : Δ then (D)^{−} is a proof-net with conclusions ⊢ Γ_{I}, Δ_{O}.

(b) If δ : R → {I, O} is a proof-net net for FILL + Mix with conclusions ⊢ Γ_{I}, Δ_{O}, then there is a sequent calculus derivation D of \overline{x} : Γ ⊢ \overline{t} : Δ such that (D)^{−} = δ : R → {I, O}.

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

(d) If (D)^{−} = δ : R → {I, O} and R reduces to R′, then there is a D′ such that D reduces to D′ and (D′) = δ : R′ → {I, O}.

Proof. To prove (a) use Lemma 4. (b) If R consists of an axiom, of disconnected structures, if a terminal ⊥-axiom is attached to some link in R or if R ends with a par link (case 1), then the argument is easy; when a terminal par link is an implication we use Lemma 4. When no terminal link is a par link (case 2.) the algorithm in our proof selects a splitting times link: we need to show that the two splitting substructures still satisfy the condition that all implications are functional.

This is immediate if the selected link v has orientations (3) \frac{O O}{O} or

(4) \frac{I I}{I}. Now suppose the orientation of v is of type (1) or (2), say (1)

\frac{A_{O} B_{I}}{(A ⊗ B)_{I}}, and let S_{A} and S_{B} be the splitting substructures. Notice that

since v is maximal with respect to ≪, for every implication w : \frac{C_{I} D_{O}}{(C℘D)_{O}} and

every directed chain γ of type ⌈C_{I}, D_{O}⌉, the link v cannot be a lower link of γ; however, v may be a lower link of a maximal directed chain of type ⌈C_{I}, 1⌋. If every maximal directed chain γ starting from B_{I} is of type ⌈B_{I}, 1_{I}⌋, then

it may very well be the case that an implication w : \frac{C_{I} D_{O}}{(C℘D)_{O}} is no longer

functional in S_{A}, while it was functional in R, if some directed chain γ′ from C_{I} passes through A ⊗ B and A ⊗ B ∈ e(C℘D). To conclude the proof it is enough to refine our argument for the sequentialization theorem as follows.

Suppose v is splitting as in subcase 2.1. If in S_{A} all implications are functional, then we are done. Otherwise, we have a chain γ′ as above, and since C℘D is not a conclusion of R, we consider the lowermost link v_{0} :

\frac{A_{0} B_{0}}{A_{0} ⊗ B_{0}} occurring below C℘D. If v_{0} was v then C℘D ≺ A and hence

A ∉ e(C℘D); so we may suppose that v_{0} is different from v. Notice that we have extended γ′ to a longer chain (not necessarily directed) passing through A ⊗ B and A_{0} ⊗ B_{0}.

We now proceed like in Subcase 2.2. of our proof of the sequentialization theorem for MLL^{−} + Mix:

Subcase 2.2.1. If v_{0} is maximal with respect to ≪, then we test whether v_{0} is splitting and whether removing v_{0} preserves the functionality of all implications, as in the case of v; if this is the case we are done;

Subcase 2.2.2. otherwise, we find another terminal times ot Cut link v_{1} and a chain γ′′ properly extending γ′ and passing through A_{0} ⊗ B_{0}. In this case, we repeat the argument with v_{1} in place of v_{0}.

And so on. Since R is finite, eventually we must find a splitting link such that the resulting structures have functional implications. This proves (b).

The proof of (c) is routine. Finally, to prove (d) we must show that our correctness condition for FILL is preserved under cut-elimination, i.e., that if a proof-net δ : R → {I, O} reduces to δ : R′ → {I, O}, then all implications in δ : R′ → {I, O} are functional. This is immediate for cuts with orientations

\frac{\frac{I  I}{I}  \frac{O O}{O}}{cut}  reduces to  \frac{I  O}{cut}  \frac{I  O}{cut}

In the remaining cases, e.g. in

\frac{\frac{A_{I}^{⊥} B_{O}}{(A^{⊥}℘B)_{O}}  \frac{A_{O}  B_{I}^{⊥}}{(A ⊗ B^{⊥})_{I}}}{cut}  reduces to  \frac{A_{I}^{⊥} A_{O}}{cut_{1}}  \frac{B_{O}  B_{I}^{⊥}}{cut_{2}}

we argue thus. Let \frac{C_{I} D_{O}}{(C℘D)_{O}} be an implication in δ : R′ → \{I, O\} and let γ

be a directed chain of type ⌈C_{I}, X_{O}⌉.

Suppose γ reaches cut_{2} first. Notice that γ cannot pass through cut_{1}, since otherwise by the above Remark γ would be the concatenation

⌈C_{I} − γ_{1} − B_{O}⌉ ∗ ⌈B_{I}^{⊥} − γ_{2} − A_{O}⌉ ∗ ⌈A_{I}^{⊥} − γ_{3} − X_{O}⌉

and γ_{2} would yield a cyclic chain in R. Therefore γ results from a chain γ′ = ⌈C_{I} − γ′_{1} − (A^{⊥}℘B)_{O}⌉ ∗ ⌈(A ⊗ B^{⊥})_{I} − γ′_{2} − X_{O}⌉ in δ : R → {I, O}, where all implications are functional, so X = D.

Now suppose γ reaches cut_{1} first. Then γ must also reach cut_{2}: indeed in

δ : R → \{I, O\} the implication \frac{A_{I}^{⊥} B_{O}}{(A^{⊥}℘B)_{O}} is functional, and so in any chain

of type ⌈A_{I}^{⊥}, Y_{O}⌉ we have Y = B. Therefore γ has the form

⌈C_{I} − γ_{1} − A_{O}⌉ ∗ ⌈A_{I}^{⊥} − γ_{2} − B_{O}⌉ ∗ ⌈B_{I}^{⊥} − γ_{3} − X_{O}⌉.

But then

γ′ = ⌈C_{I} − γ_{1} − A_{O}⌉ ∗ ⌈B_{I}^{⊥} − γ_{3} − X_{O}⌉

is a directed chain in δ : R → {I, O}, where all implications are functional, so X = D.

References

[1] S. Abramsky. Computational Interpretations of Linear Logic, Theoretical Computer Science , 111, 1993, pp. 3-57.

[2] S. Abramsky and R. Jagadeesan. Games and Full Completeness Theorem for Multiplicative Linear Logic, J. Symbolic Logic, Vol.59, No.2, pp. 543-574.

[3] A. Asperti. Causal Dependencies in Multiplicative Linear Logic with MIX. Mathematical Structures in Computer Science, September 1995.

[4] A. Asperti. A linguistic approach to deadlock. Rapport de Recherche du Laboratoire d’Informatique de l’Ecole Normale Supérieure de Paris, LIENS-91-15, October 1991.

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

[6] G. Bellin and A. Fleury. Braided Proof-Nets for Multiplicative Linear Logic with Mix. Submitted to the Archive for Mathematical Logic, special number devoted to papers from the Logic Colloquium 1995.

[7] G. Bellin and J. Ketonen. A Decision Procedure Revisited: Notes on Direct Logic, Linear Logic and its Implementation, Theoretical Computer Science 95: 115-142, 1992.

[8] G. Bellin and P. J. Scott. On the π-calculus and linear logic, with an Introduction by S. Abramsky, Theoretical Computer Science 135 (1994), pp. 11-65.

[9] G. Bellin and J. van de Wiele. Subnets of Proof-nets in MLL^{−}, in Advances in Linear Logic, J-Y. Girard, Y Lafont and L. Regnier editors, London Mathematical Society Lecture Note Series 222, Cambridge University Press, 1995, pp. 249-270.

[10] R.F. Blute. Linear Logic, Coherence and Dinaturality, Theoretical Computer Science 115, 3-41.

[11] R.F. Blute, J.R.B. Cockett, R.A.G. Seely. ! and ?, Storage as tensorial strength, submitted to Mathematical Structures in Computer Science.

[12] J.R.B. Cockett, R.A.G. Seely. Weakly distributive categories, in Fourman, Johnstone and Pitts eds., Applications of Categories to Computer Science, London Mathematical Society Lecture Note Series 177, 1992, pp. 45-65.

[13] V. Danos. La logique linéaire appliquée à l’étude de divers processus de normalisation et principalement du λ-calcul, Thèse de doctorat, U. Paris VII, April 1990.

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

[15] V.C.V. de Paiva. The Dialectica Categories, in Categories in Computer Science and Logic (J.W.Grey and A.Scedrov eds.) Contemporary Mathematics 92, American Mathematical Society, 1989, pp. 47-72.

[16] V.C.V. de Paiva. A Dialectica-like Model of Linear Logic, in Category Theory and Computer Science, Manchester, UK, September 1989 (D.H.Pitts and others eds.) Springer Lecture Notes in Computer Science 389, 1989, pp.341-356.

[17] A. Fleury and C. Retoré. The Mix Rule, Mathematical Structures in Computer Science 4, 1994, pp. 273-85.

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

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

[20] J. M. Hyland and V. C. V. de Paiva. Full Intuitionistic Linear Logic, Annals of Pure and Applied Logic 64, 1993, pp.273-91.

[21] J. Ketonen. EKL - A Mathematically Oriented Proof Checker, Proceedings of the Seventh Conference on Automated Deduction, (Shostak ed.), Springer Lecture Notes in Computer Science 170, pp. 65-79, 1984.

[22] J.Ketonen and R.Weyhrauch. A Decidable Fragment of Predicate Calculus, Theoretical Computer Science 32: 297-307, 1984.

[23] M. Hyland and L. Ong. Fair Games and Full Completeness for Multiplicative Logic without the rule of Mix, manuscript, Computer Laboratory and Department of Pure Mathematics and Mathematical Statistics, University of Cambridge.

[24] P.Lincoln and T.Winkler. Constant-Only Multiplicative Linear Logic is NP-Complete. Preprint. Computer Science Department, Stanford University, Stanford, CA 94305.

[25] C.Retoré. Réseaux et Séquents Ordonnées PhD thesis, Université Paris VII, Mathématiques, 1993.

[26] C.Retoré. Graph Theory from Linear Logic: Agregates. Preprint n.47, Équipe de Logique Mathématique, Université Paris VII, Octobre 1993.

[27] H. Schellinx. Some syntactical observations on linear logic. Journal of Logic and Computation, 1 (4) pp. 537-559, 1991.

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