Proof Nets

for Multiplicative and Additive Linear Logic

by Gianluigi Bellin

Department of Computer Science Edinburgh University Edinburgh, EH9 3JZ

Scotland

This version of the MALL was printed on June 7, 1994.

Abstract

This paper extends the theory of proof nets from Multiplicative Linear Logic to Multiplicative and Additive Linear Logic, by removing the additive boxes. This yields uniqueness of normal form for that fragment and a classification of permutability of inferences in the calculus of sequents for classical Linear Logic.

0. Introduction.

‘A mathematical proof must be perspicuous’. Only a structure whose reproduction is an easy task is called a ‘proof’. (Wittgenstein)

This paper studies the general proof theory of linear logic and direct logic, resourceaware systems that restrict the iterated use of assumptions in proofs.^{1} More specifically, it contributes to the theory of proof nets, developed by J-Y. Girard, and offers a solution to the technical problem of additive boxes. More generally, it aims at the following goals:

(I) a simple and convincing explanation of proof nets, as a multiple conclusion natural deduction system for linear logic;

(II) a formalism for linear logic enjoying uniqueness of the normal form.

Historical remark. The study of proof nets for classical linear logic is rooted in the tradition of Gentzen and Prawitz in an obvious and important way. Prawitz provides a definitive treatment of Gentzen’s natural deduction systems, at least for intuitionistic logic. Prawitz gives a strong normalization theorem for second order logic and highlights the significance of normalization theorems by presenting the following conjecture: Two formal derivations represent the same proof if and only if they reduce to the same normal form. Gentzen and Prawitz’s natural deduction for intuitionistic logic enjoys uniqueness of the normal form, modulo permutations of the ∨- and ∃-eliminations with other inferences. A many-one map from sequent calculus derivations to natural deduction derivations is defined in the fragment without ∨ and ∃ and several efforts have been made to generalize such results (e.g., Zucker , Pottinger , Ungar ). It appears that a multiple conclusion natural deduction system is needed in classical logic, where a deduction A ⊢ B is regarded as essentially the same as a deduction of ¬B ⊢ ¬A. Now proof nets appear as a significant breakthrough in the definition of such systems.

Less well known are the connections between proof nets and proof-search algorithms

in the matrix-methods, which have been pursued D. Prawitz  , Bibel  , P. An-
drews  , Ketonen and Weyhrauch  , L. A. Wallen  . In particular,

Ketonen and Weyhrauch introduced direct logic, a Contraction-free system in which Weakening is unrestricted, i.e., deductive resourced can be wasted but never reused. The logical connectives have an intensional interpretation, according to the terminology of relevance logic. A decision procedure for direct logic is described in Ketonen and Weyhrauch and implemented in the proof-checker at the Stanford Artificial Intelligence Laboratory; the notion of a proof net is implicitly contained in that procedure (for corrections, comments and descriptions of the implementation see Bellin and Ketonen ).

1 I wish to express my gratitude to my teachers S. Feferman, J. Ketonen and G. Kreisel. Thanks also to J-Y. Girard for interesting and challenging conversations.

The beginning and first development of linear logic is documented in the fundamental paper Girard . The distinction is made between multiplicative and additive connectives (corresponding to the intensional and extensional connectives of relevance logic) and the exponential operators, the main innovation of the system, are introduced. For a broad explanation of the meaning and the purpose of linear logic, see Girard . In Girard a concise language is introduced, and an efficient calculus of sequents for linear logic is presented. Also the notion of a proof net is introduced (section 1, pp. 28-47) for the multiplicative fragment (without propositional constants) of linear logic and extended to the whole system by the device boxes. A map is given from sequent calculus derivations to proof nets, which is proved to be onto (sequentialization theorem). A strong normalization theorem is proved for proof nets and the notion of a slicing of the boxes is described, which is Church-Rosser.

A proof structure is a set of formula occurrences connected by certain relations (links). Proof nets are the proof structures that represent correct linear proofs: they are characterized by certain consistency conditions on the structure as a whole. In Ketonen and Weyhrauch the global condition is acyclicity, where a cycle is defined as a chain of conjunctive subformulas satisfying certain properties. In Girard an interesting kind of algebraic invariant is introduced for the multiplicative fragment without propositional constants, the no short trip restriction (ibid., pp.30-41). The condition presented in Danos and Regnier appears to be related to that of Ketonen and Weyhrauch. Ketonen and Weyhrauch’s condition appears also in Abramsky , where an interesting typetheoretic interpretation is given, essentially focused on the dynamics of computation, i.e., on cut elimination. Boxes are retained in Abramsky as appropriate to characterize lazy evaluations.

In Girard boxes are introduced in correspondence with the propositional constants ⊥ and ⊤, the additive conjunction ⊓, the universal quantifier ∀, with the exponential ! and the (restricted) weakening rule. Then the task is set of removing these boxes (see especially op.cit. section 7, pp. 93-97). A method is outlined for the solution of the problem by slicing boxes; the contraction steps for the normalization of slices are given. Thus the problem is whether slices are a viable representation of linear derivations: ‘Each slice is in itself logically incorrect, but it is expected that the total family of slices has a logical meaning. However, there is no characterization of sets of slices which are the slices of a proof-net.” ibidem, p. 95.

Carrying this program on, Girard and achieve the elimination of ∀ boxes. Remarks. (i) The global verification of consistency conditions is a feature of natural deduction systems, in contrast with sequent calculi, where correctness of local links and global consistency are verified locally. The restriction on eigenvariables is an example in Gentzen and Prawitz’s natural deduction. In our presentation we will make the global constraints explicit as much as possible. (ii) Systems of sequent calculi and of natural deduction can be regarded as formalisms in their own right. In this case it is debatable whether the calculus of proof nets is a perspicuous method of proof, if the verification of any of the present consistency conditions is part of the formal representation of the deductive process (it would seem that the ‘no short trip’ condition is less perspicuous than the acyclicity condition). Alternatively, a proof net can be regarded as the result of an inductive inferential process, as formalized in a sequent calculus derivation. Hence a proof net would always be given together with some derivation in the calculis of sequents (or other global inductive process). This view is indeed suggested by Girard’s remark that the soundness condition is only ‘an abstract notion (just like, say, semantical soundness), whose importance lies in its relation to linear sequent calculus’ (Girard , p.33). (iii) It is possible to abstract from Girard’s proofs some consistency conditions in terms of properties of the subnets (or empires) in a proof net. The justification of such conditions is particularly natural, as they correspond to elementary properties of inductively defined structures, and the presentation of the Sequentialization Theorem is improved. Still, it is convenient to use other conditions in the proof of the Cut Elimination Theorem.

A consistency condition defining proof nets must highlight some interesting feature of inductively generated structures, and in particular, of their behavior under cut elimination. The proposal of alternative conditions should therefore be welcome. (iv) A proof structure with boxes represents a logical deduction as a collection of separate structures, in a certain ordering. On the other hand, the fact that the computation of correctness of a multiplicative structure can be done with large degree of parallelism has been regarded as very promising and significant feature of the new calculus (cf. Girard ). It would seem interesting from the point of view of parallelism to eliminate boxes and to replace them with more flexible forms of synchronization between different processes of computation.

(v) The elimination of boxes is also a main step towards a representation of deductions where normal forms are unique. To this purpose, we must eliminate commutative reductions (familiar in connection with the ∨- and ∃-elimination rules in natural deduction). More generally, we must find a representation of proofs such that two derivations that differ only in the following sequence of inferences are mapped to the same structure:

\begin{aligned}⊢ C, Γ, A & ⊢ C, Γ, B \\ ⊢ Δ, D & ⊢ C, Γ, A ⊓ B \\ & ⊢ Δ, D ⊗ C, Γ, A ⊓ B \end{aligned}  (⊓/⊗)

⊢ Δ, D ⊢ C, Γ, A  ⊢ Δ, D ⊢ C, Γ, B
⊢ Δ, D ⊗ C, Γ, A  ⊢ Δ, D ⊗ C, Γ, B

⊢ Δ, D ⊗ C, Γ, A ⊓ B (⊗/⊓)

(vi) In a ⊓ box the conclusions of two structures S′ and S′′ are ‘identified’ in some sense; because of commutative reductions, several choices may be possible for such an identification. When slicing a ⊓ box we must retain the identifications within the resulting family of slices in some form. Now it seems that the most elegant solution is a representation where all correct choices are open, and only the possibility of some identification is required for logical correctness. (vii) The ⊥ boxes confront us with the ‘disturbances’ caused by irrelevance on the geometric symmetries of proof structures. A ⊥ symbol introduced by the ⊥ rule

\frac{⊢ Γ}{⊢ Γ, ⊥}

bears no relevant connection to the occurrences in Γ (or to the axioms above them in the derivation). A box for ⊥ should be sliced into a disconnected configuration of the form

{S \atop Γ} ⊥

However, the presence of a ⊥ symbol in a proof structure is justified by its ‘attachement’ to some subtructure which contains proper axioms among its topmost formulas. Unlike in direct logic, (cf. Ketonen and Weyhrauch , Bellin and Ketonen ), such attachments create new connections that must be compatible with the global consistency conditions of multiplicative proof nets. To represent such attachments as ordinary links is unsatisfactory, since such links represent an undesirable modification of meaning: they exhibit a ‘relevant connection’ where there is none. The most satisfactory solution would be to use slices, and leave all correct attachments open, but also to make the computation of slices as multiplicative structures possible, by representing attachments is some way. (An alternative approach has been considered in Solitro , that reduces the ⊥ boxes to the ! boxes and the ⊤ axiom.) (viii) A similar discussion applies to ⊤ axiom

⊢ ⊤, X_{1}, …, X_{n}.

The ⊤ box is sliced as a disconnected configuration

⊤ X_{1} … X_{n}.

The main difference is due to the meaning of ⊤ (expressed in the property of its dual: 0 −∘ A, ex falso quodlibet). Indeed ⊤ acts like an ‘eraser’: a derivation of the form

. . . . . .
⊢ ⊤, Γ, C  ⊢ D, Δ
⊢ ⊤, Γ, C ⊗ D, Δ

reduces to

⊢ ⊤, Γ, C ⊗ D, Δ.

The above property represents garbage collection (cf. section 3.5.). It can also be described as propagation of irrelevance: if one (multiplicative) conjunct is irrelevant in a proof then the other also may be regarded as irrelevant. When a ⊤ box is sliced into a disconnected set of occurrences, a formula occurrence in a slice is said to be irrelevant if there is no axiom above it. Propagation of irrelevance is implicit in the definition of path by Ketonen and Weyhrauch in the context of a search procedure for cut-free proofs in direct logic (cf. remark (ii) in section 2.3.); it is used to improve the efficiency of the Proof Checker , based on direct logic. The issue becomes more problematic in linear logic (‘we are forced to make bricolage on such details’, Girard , p. 95), where the distinction between ⊥ and 0 is introduced and propagation of irrelevance is considered an explicit rule of contraction (zero commutation). (ix) We will not consider the problem of eliminating ! boxes.

(x) We propose to slice an additive proof structure into parts (quasi structures) such that the multiplicative conditions can still be tested within each of them.

Linear logic is mostly concerned with the computational aspects of reasoning, but is

also of significance to the study of parallelism (cf. Girard  , Asperti  , Marti-
Oliet and Meseguer  , Brown  , Gehlot and Gunter  ). A motivation for

our work is to extend some syntactical features of the multiplicative fragment that seem relevant for parallelism to the additive fragment as far as possible.

A strong normalization result for first order linear logic, with some form of Church-Rosser property, could be transfered to classical logic; this may improve our understanding of a well-known problem of general proof theory (cf. Gandy ).

In this paper we will not consider applications of the theory of proof nets as such. In Bellin and proof nets are used for proof-transformations — applied there to the Infinite Ramsey Theorem.

1. Preliminaries.

We refer the reader to Girard for a broad explanation of the meaning and the purpose of linear logic. In particular, the motivations of the syntax and the terminology are presented there.

1.1. Language.

The following fragments of classical linear logic LL are considered: MLL^{−}: multiplicative linear logic without rules for propositional constants; MLL: multiplicative linear logic with rules for propositional constants; MALL^{−}: multiplicative and additive linear logic without rules for propositional constants; MALL: multiplicative and additive linear logic with rules for propositional constants.

The above system are considered in the propositional and first order cases. NCMLL^{−}, NCMLL, NCMALL^{−}, NCMALL are the (cyclic) noncommutative corresponding systems, also considered in the propositional and first order cases. The language for the propositional systems MLL and NCMLL of Commutative and Noncommutative Multiplicative Linear Logic contain the propositional constants 1, ⊥, the unary connective ( )^{⊥} (linear negation), the binary connectives ⊗ (times) and ⊔ (par). The following axioms hold in both logics:

A^{⊥⊥} = A,  1^{⊥} = ⊥,  ⊥^{⊥} = 1.

In MLL we have

(A ⊗ B)^{⊥} = A^{⊥} ⊔ B^{⊥} (A ⊔ B)^{⊥} = A^{⊥} ⊗ B^{⊥}

and in NCMLL we have

(A ⊗ B)^{⊥} = B^{⊥} ⊔ A^{⊥} (A ⊔ B)^{⊥} = B^{⊥} ⊗ A^{⊥}.

The systems MALL and NCMALL extend the previous fragments to Additive linear logic: there are new logical constants ⊤ and 0, new connectives ⊓ (with) and ⊕ (plus), satisfying

⊤^{⊥} = 0, 0^{⊥} = ⊤

and moreover

(A ⊓ B)^{⊥} = A^{⊥} ⊕ B^{⊥} (A ⊕ B)^{⊥} = A^{⊥} ⊓ B^{⊥}.

The fragments MLL^{−} and MALL^{−} have the same language as MLL and MALL, respectively, but no axioms or rules for the propositional constants 1, ⊥, ⊤ and 0.

The languages for the first order systems MLL, NCMLL, MALL, NCMALL are defined as expected, using the quantifiers ⋀ (every) and ⋁ (some). We have the axioms

(⋀ x.A)^{⊥} = ⋁ x.(A^{⊥}) (⋁ x.A)^{⊥} = ⋀ x.(A^{⊥}).

The above axioms allow us to reduce the scope of linear negation: henceforth in our syntax linear negation will be applied only to atomic formulas.

The language for the full system LL of (classical) linear logic contains in addition the propositional operators ! (of course!) and ? (why not?), called exponentials (or modalities).

1.2. Sequent Calculus.

We list the rules of inference of the calculus of sequents for linear logic (Girard ) and for direct logic (Ketonen and Weyhrauch ), for convenience of the reader.

Sequent Calculus for LL.

Logical Axioms:  ⊢ A^{⊥}, A

Cut Rule:  \frac{⊢ Γ, A  ⊢ A^{⊥}, Δ}{⊢ Γ, Δ}

Exchange Rules:

Non Commutative  Commutative
⊢ B, Γ, A  ⊢ Γ, B, A, Δ
⊢ A, B, Γ  ⊢ Γ, A, B, Δ

1 Axiom:  ⊢ 1  ⊥ Rule:  \frac{⊢ Γ}{⊢ Γ, ⊥}

⊗ Rule:  \frac{⊢ Γ, A  ⊢ B, Δ}{⊢ Γ, A ⊗ B}  ⊔ Rule:  \frac{⊢ Γ, A, B}{⊢ Γ, A ⊔ B}

⊤ Axioms:  ⊢ ⊤, X_{1}, …, X_{p}  for p ≥ 0
⊓ Rule:  \frac{⊢ Γ, A  ⊢ Γ, B}{⊢ Γ, A ⊓ B}  ⊕ Rule:  \frac{⊢ Γ, A_{i}}{⊢ Γ, A_{0} ⊕ A_{1}} for i = 0 or 1

Dereliction: \frac{⊢ Γ, A}{⊢ Γ,?A}  Weakening: \frac{⊢ Γ, ⊥}{⊢ Γ,?A}  Contraction: \frac{⊢ Γ,?A,?A}{⊢ Γ,?A}

! Rule:  \frac{⊢ ?Γ, A}{⊢ ?Γ,!A}

where ?Γ consists only of formulas of the form ?C or ⊥. Sequent Calculi for Direct Logic: The system of sequent calculus for the logic DL consists of the rules for MLL^{−}, namely Logical Axioms and rules for multiplicative conjunction and disjunction, and also on the rule of Mingle; the calculus of sequents for DL^{+} has the rules for MLL^{−}, and in addition unrestricted Weakening.

Mingle  Weakening
⊢ Γ  ⊢ Δ  ⊢ Γ
⊢ Γ, Δ  ⊢ Γ, A

1.3. Links and Proof Structures.

A link is a m + n-ary relation between formula occurrences. For each link if X_{1},…, X_{m+n} are in the link, then X_{1}, …, X_{m} are called the premises and X_{m+1}, …, X_{m+n} are called the conclusions of the link. If m = 0, the link is an axiom link. Links are graphically represented as follows. The logical axioms and the 1 axioms are

\overline{P, P^{⊥}} \overline{1}.

The Cut, ⊗-, ⊔- ⊕-, ⋀- and ⋁-links are

\underline{X X^{⊥}}  \frac{X Y}{X ⊗ Y}  \frac{X Y}{X ⊔ Y}  \frac{X}{X ⊕ Y}  \frac{Y}{X ⊕ Y}  \frac{X(a)}{⋀ x.X}  \frac{X(t)}{⋁ x.X}

respectively. A variable a occurring in the premise of a ⋀ link is called eigenvariable, or parameter, with the convention that each eigenvariable is associated with one and only one ⋀ link. Logical and 1 axioms, Cut, ⊗- and ⊔- links are multiplicative links; the ⊤ axiom and the ⊕-link are additive. The first order links ⋀ and ⋁ should also be regarded as additive (but we will not consider here the issue of multiplicative quantifiers).

When considering the exponentials, we add the links for ?, i.e., Dereliction, Weakening and Contraction:

\frac{A}{?A}  \frac{⊥}{?A}  \frac{?A ?A}{?A}.

A proof structure S for [first order] MLL^{−} consists of

(i) a nonempty set of formula-occurrences (i.e., a multiset of formulas) together with (ii) a set of logical axioms and multiplicative links [and first order 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;

(3) an axiom link \overline{X_{1}, …, X_{n}} is identified with \overline{X_{σ(1)}, …, X_{σ(n)}}, where σ is any cyclic permutation, and a Cut link \underline{X X^{⊥}} is identified with \underline{X^{⊥} X}. Notice that a link \frac{X Y}{X∘Y} is different from \frac{Y X}{Y ∘X}. For example, a proof structure in MLL^{−} is

\begin{matrix}A  A^{⊥} & A  A^{⊥} \\ A ⊗ A^{⊥} & A ⊗ A^{⊥} \end{matrix}

We write X ≺ Y if the formula occurrence X occurs above the formula occurrence Y in S (with the obvious meaning of above).

It is convenient to put a marker for the missing conclusion of a Cut link: Girard introduces the special symbol CUT. Such a symbol is not a formula occurrence; we will call it a ghost (to reduce the number of different uses of the word ‘cut’). The premises of a Cut are called cut formulas, as usual. The formula occurrences of S which are not premises of any link are called the conclusions of S.

A proof structure S for NCMLL^{−} is defined like a proof structure for MLL^{−}, with in addition (iii) a cyclic order of the conclusions and of the cut formulas. The ordering is extended to all the formulas in S by letting X Y if and only if for some U and V such that X ⪯ U, Y ⪯ V, either (i) U ∘ V is a formula occurrence in S or (ii) U and V are conclusions or cut formulas and U V. Remark. The above syntax follows Girard , but with the technical modification of the Weakening link. The following syntax for the propositional constants is a minor departure from the tradition (see Remark (v), section 1.5):

A proof structure for MLL or NCMLL is defined as for MLL^{−} or NCMLL^{−}, respectively, allowing also \overline{1} axioms and of ⊥ links of the form

\frac{A}{A, ⊥,}

where A ≠ ⊥.

It is convenient to introduce proof structures with non-logical axioms, written as

\overline{X_{1}, …, X_{n}}

for n > 0. These correspond to sequent axioms or initial sequents in sequent calculus.

Let m : S → S′ be any injective map of proof structures (regarded as sets of formula occurrences). We say that m preserves the links

\overline{X_{1}, …, X_{n}}  \frac{A}{B}  \frac{A B}{C}

if we have

\overline{m(X_{1}), …, m(X_{n})}  \frac{m(A)}{m(B)}  \frac{m(A) m(B)}{m(C)}

Finally, let C_{1}, …, C_{n} the set of conclusions of S. We say that m preserves the conclusions if m(C_{1}), …, m(C_{n}) are all the conclusions of S′.

An injective map ι : S → S′ is an embedding if it preserves links and, moreover, X and ι(X) are occurrences of the same formula, for every X in S. A subset S′ of S is a substructure if the identity is an embedding.

1.4. Inductive Proof Structures.

A sequent derivation is inductively built from axioms by applications of the rules of inference. In a similar way, we can inductively generate the proof structures that correspond to linear derivations. More precisely, a proof structure for MLL^{−} is said inductively generated (an IPS) if it results from a finite number of applications of the following steps:

(0) An axiom

\overline{A A^{⊥}}

is an IPS;

(1) If S and S′ are IPS’s with the multisets Γ, A and A^{⊥}, Δ, respectively, as conclusions, and moreover S ∩ S′ = ∅, then

\begin{aligned}& S & & S′ \\ Γ, & & A A^{⊥} & & Δ \end{aligned}

is an IPS with the multiset Γ, Δ as conclusions;

(2) If S and S′ are IPS’s with the multisets Γ, A and B, Δ, respectively, as conclusions, and moreover S ∩ S′ = ∅, then

S  S′
Γ, A B Δ
A ⊗ B

is an IPS with the multiset Γ, A ⊗ B, Δ as conclusions;

(3) If S is an IPS with the multiset Γ, A, B as conclusions, then

\begin{aligned}& S \\ Γ, & A B \\ & A ⊔ B \end{aligned}

is an IPS with the multiset Γ, A ⊔ B as conclusions.

(4) If S is an IPS with the multiset Γ, A(a) as conclusions, and a does not occur in Γ, then

\begin{aligned}& S \\ Γ, & A(a) \\ & ⋀ x.A \end{aligned}

is an IPS with the multiset Γ, ⋀ x.A as conclusions.

(5) If S is an IPS with the multiset Γ, A(t) as conclusions, then

\begin{aligned}& S \\ Γ, & A(t) \\ & ⋁ x.A \end{aligned}

is an IPS with the multiset Γ, ⋁ x.A as conclusions.

The above definition is extended to the noncommutative case NCMLL^{−} by considering the conclusions and the cut formulas of an IPS as a set with ciclic ordering, defined arbitrarily at steps (1) and in the obvious way at each step (2) - (5). For instance, in case (2) let Γ, A = A_{0}, …, A_{n−1}, be the conclusions and the cut formulas of S; let B, Δ = B_{0}, …, B_{m−1} be the conclusions and the cut formulas of S′, where the indices represent the ordering of the conclusions mod n and mod m, respectively; then the conclusions and the cut formulas Γ, A⊗B, Δ of the resulting IPS are C_{0}, …, C_{n−1}, …, C_{n+m−2}, where the indices represent the order mod n + m − 1. Remarks. (i) The following is clear (by a glance at section 1.2). There is an obvious map ( )^{∗} that transforms any sequent derivation D in (first order) MLL or NCMLL into a proof structure S for the same fragment. If S is an IPS, then from the inductive generation of S we immediately obtain a derivation D such that S = (D)^{∗}. (ii) We refer the reader to Girard for explanations of the meaning of logical symbols in relation to their introduction rules. To motivate the formal choices it is important to keep in mind the following slogans. In step (0) the axiom \overline{A A^{⊥}} asserts the existence of a relevant connection (a “wire”) between the occurrences A and A^{⊥}. In step (3) the ⊔ link can be regarded as an introduction of a linear implication with conclusion A^{⊥} −∘ B or A ∘− B^{⊥}. Step (1) and (2) connect two separate structures in different ways: in step (2), the connective ⊗ joins the occurrences A and B as separate non-communicating entities; in step (1) the linkage of the cut formulas A and A^{⊥} creates the possibility of communication (a “plug” between wires). Similarly, thinking in terms of “formulas-as-types”, step (3) is a “symmetric lambda abstraction” and step (1) is lambda application. (iii) A Cut link may be regarded as a ⊗-link

\frac{X X^{⊥}}{X ⊗ X^{⊥}}

with the understanding that X ⊗X^{⊥} is not a formula occurrence but rather a ghost. It will be shown that from a geometric point of view, and statically (i.e., without consideration of cut elimination) Cut and ⊗ links are basically the same. In other words, the expression X ⊗ X^{⊥} can be regarded either as one of the conclusions of the deductive process or as a temporary inconsistency to be removed. More precisely, in a propositional multiplicative proof structure, with respect to its internal connections, there is no difference between a ghost and a real formula occurrrence. The difference matters (i) when we add quantifiers and additives or (ii) in the noncommutative case or (iii) when we ask, from the outside, what are the conclusions of (the deductive process represented by) a given structure.

1.5. The notion of a box.

In Girard there are boxes in correspondence with following axioms and inference rules of sequent calculus for linear logic: (1) the ⊤-axiom

⊢ ⊤, X_{1}, …, X_{n},

(2) the one-premise rule

⊥ : \frac{⊢ Γ}{⊢ Γ, ⊥}  ∀ : \frac{⊢ Γ, A(a)}{⊢ Γ, ∀x.A}  ! : \frac{⊢ ?C_{1}, …,?C_{n}, A}{⊢ ?C_{1}, …,?C_{n},!A}

(as usual, in the case of the ∀ rule a does not occur in Γ) and (3) the two-premise rule

⊓ : \frac{⊢ Γ, A ⊢ Γ, B}{⊢ Γ, A ⊓ B} .

In correspondence with each one-premise rule there is a box of the form

\begin{matrix}S′ \\ Γ Y \\ S^{o} \end{matrix}

and in correspondence with the ⊓ rule we have

\begin{matrix}S′ & S′′ \\ Γ A ⊓ B \\ S^{o} \end{matrix}

where the indicated multisets of formulas belong to a ‘new kind of link’: we may regard Γ, Y [or Γ, A ⊓ B] as non-logical axioms of S^{o} and we write sometimes \overline{Γ, Y} [or \overline{Γ, A ⊓ B}].

We have the following global restriction: (§) In all the above boxes, the lowermost formula occurrencess of S′ [and of S′′] must correspond to the non-logical axiom as follows (cf. the related inference of the calculus of sequents):

S′  S′  S′  S′  S′′
⊥: Ξ, Γ  ∀: Ξ, Γ, A(a)  !: Ξ, Γ, A  ⊓: Ξ, Γ, A  Θ, Γ, B
Γ, ⊥  Γ, ∀x.A  Γ,!A  Γ, A ⊓ B

Here Ξ and Θ are multisets of ghosts.^{2}

2 To test condition (§) we need maps between the occurrences of Γ in the conclusions of S′, S′′ and in the non-logical axiom. There may be lots of such maps. A ‘non-constructive’ operation is implicit here (which would be obvious if we considered infinitary multisets).

The additional global restrictions hold: (§§) In the ∀ box, a does not occur in Γ (but it may occur in Ξ). (§§§) In the ! box, Γ has the form ?C_{1},…, ?C_{n}, for some n. Finally, there is an obvious global restriction implicit in the above notation: (§§§§) In all the above boxes, S′, S′′ and S^{o} are pairwise disjoint sets.

A proof structure with boxes is defined like a proof structure, with the addition the new kind of link represented by the box. We may assume that the conditions (§)-(§§§) are checked by a flagging function φ, leaving the details to the reader. We will refer to Conditions (§)-(§§§§) as the Box Condition, version 1.

Also, Inductive Proof Structures with Boxes (IPSB) for the full system of linear logic can be defined by adding to the clauses for IPS the clause

(6) If S′ is an IPSB [if S′ and S′′ are IPSBs and S′ ∩ S′′ = ∅], then so is the configuration S consisting of S′ [of S′ and S′′] inside a box and of a new non-logical axiom outside the box, provided that the conclusions of S′ [of S′ and S′′] and the non-logical axiom satisfy conditions (§), (§§) and (§§§); the conclusions of S are the occurrences of the non-logical axiom.

A proof structure S with boxes and with conclusion Γ satisfying the box condition can also be regarded as a collection C of proof structures with non-logical axioms and without boxes (i.e., proof structures for MLL with ⊕ and ? links with non-logical axioms), with the following properties:

(i) There is an S_{0} in C having Γ as conclusions. (ii) There is a function φ (flagging function) with the following property: if S′ in C is different from S_{0} then φ associates to the multiset of conclusions of S′ with one nonlogical axiom occurring in some S′′, in accordance with (§)-(§§§). Every non-logical axiom occurring in some S′ ∈ C is associated by φ to the multisets of conclusions of one or two structures in C. Let S_{1} ◁^{0} S_{2} be the relation defined on C which holds if and only if the conclusions of S_{1} correspond to a non-logical axiom of S_{2} by φ; let ◁_{t} be the transitive closure ◁^{0}. The following is a global restriction equivalent to the box condition, version 1: Box condition, version 2: C satisfies (i) and (ii), the structures in C are pairwise disjoint and ◁_{t} is a strict order.

We can define proof structures for NCMALL by using the box condition, version 2: we require that each proof structure in C has a cyclic ordering (defined as in section 1.3) and that if S_{1} ◁^{0} S_{2}, then the orderings of S_{1} be compatible with that of S_{2} in an obvious sense. We leave it to the reader to fill in the details.

2. Part I. Proof Nets for Multiplicative Linear Logic.

In this section we extract from Girard  and  some conditions that

characterize multiplicative proof nets in terms of their subnets (or empires), pointing at the connections with Ketonen and Weyhrauch (cf. also Danos and Regnier ). Working with the notion of empire makes the generalization to the additives easier.

2.1. Empires.

Given a Proof-Structure S for MLL^{−} and NCMLL^{−} and a formula occurrence A ∈ S, we define e(A), the empire of A in S, as the smallest set of formula occurrences closed under the following conditions. (Remember that X_{i} ≠ A means that X_{i} and A are different formula occurrences.)

(i) A ∈ e(A); (ii) if \frac{X_{1} X_{2}}{Y} [resp. \frac{X_{0}}{Y}] is a link in S and Y ∈ e(A), then X_{1}, X_{2} ∈ e(A), [X_{0} ∈ e(A)] (↑-step); (iii) if \overline{X_{1}, …, X_{p}} is an axiom in S and X_{i} ∈ e(A) for some i, then for all j, X_{j} ∈ 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) [resp. if \frac{X}{Y} is a unary link in S, X ≠ A and X ∈ e(A), then Y ∈ 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}, ∈ e(A), X_{2} ∈ e(A), then X_{1} ⊔X_{2} ∈ e(A) (⇓-step).

A ghost or formula occurrence D ∈ e(A) which is not a premise of a link with conclusion in e(A) is called a door of e(A). It is clear that such a D which is not a ghost must be one of the following:

• A itself (main door);

• A conclusion of S (open door);

• A premise of a link \frac{C D}{C⊔D} or \frac{D C}{D⊔C} (closed door). Remark. We choose the terminology ‘open’, ‘closed’ doors since there is an analogy (to be justified below) between a closed door in a proof structure and the conclusion of an implication introduction in Gentzen-Prawitz’s natural deduction system; similarly, there is a correspondence between an open door and an open assumption.

A computation verifying that B ∈ e(A) in S consists of sequences of steps (ii)-(v), starting from A and reaching B. We can represent a computation as a tree τ : [A] → B, with root in B and leaves in A, where a branching occurs only in correspondence with a step (⇓). A tree τ : [A] → B is said normal if no sequence in it reaches twice the same formula occurrence. Every (finite) tree τ : [A] → B is reduced to a normal tree τ′ : [A] → B in finitely many steps.^{3} We write X∅Y for X ∉ e(Y) and Y ∉ e(X); X Y for X ∈ e(Y) and Y ∉ e(X); X♢Y for X ∈ e(Y) and Y ∈ e(X).

Let \frac{X(a)}{⋀ x.X} be any link in S and let b be any eigenvariable. We write

a <^{0} b if b occurs both inside and outside e(X(a)) and we let <_{t} be the transitive closure of the relation <^{0} (over the eigenvariables of S).

2.2. Proof Nets.

Let S be a proof structure for MLL^{−} or NCMLL^{−}. We consider the following requirements on S.

(0) (Noncommutative case only) If \overline{X, …, X′} and \overline{Y, …, Y′} are any pair of distinct axiom links, or \underline{X X′} and \underline{Y Y′} are any pair of disjoint Cut links, then in the induced ordering we cannot have X Y X′ Y′ or X Y′ X′ Y (the planarity condition);

(1) For every link \frac{X Y}{X⊗Y} in S, X∅Y (the [no] vicious circle condition);

(2) For every link \frac{X Y}{X⊔Y} in S, and for every X, Y that are conclusions of S or ghosts, X♢Y (the connectedness condition);

(3) The ordering <_{t} is strict (the parameters condition).

A proof structure in [first order] MLL^{−} is a proof net if it satisfies the vicious circle and connectedness [and parameters] conditions. A proof net for NCMLL^{−} must also satisfy the planarity condition. Remarks. (i) In linear logic the vicious circle condition is the main requirement of propositional consistency and the connectedness condition is the requirement of relevance. (ii) The ‘naturality’ of the above conditions, as well as the connection between the parameters condition and the usual restrictions on the eigenvariables, can be evaluated as soon as the role of empires is understood. The main fact about empires to keep in mind is the following Theorem, whose proof can be obtained using the techniques below. 2.2.1. Subnet Theorem. Let S be a proof net for MLL^{−} or NCMLL^{−} and let A be any formula occurrence in S. Then e(A) is a substructure of S which is a proof net.

2.2.2. Theorem. Every IPS in MLL^{−} or NCMLL^{−} is a proof net.

3 Such trees are particularly simple instances of inductively presented systems considered in Feferman .

The proof is by induction on the definition of IPS. For the vicious circle condition see the Remark below. The parameters condition is immediate if we make sure that different eigenvariables are used at each application of (4) (pure parameters property). The details are left to the reader. Remark. Consider step (2) in the definition of IPS, section 1.4. Clearly, the requirement that S ∩ S′ = ∅ implies e(A) ∩ e(B) = ∅ in the resulting IPS, thus A∅B. Conversely, in a proof net A∅B implies e(A) ∩ e(B) = ∅, by the Tiling Lemma below (section 2.5). By the Subnet Theorem, e(A) and e(B) are IPS.

Moreover, Step (2) corresponds to the operation of substitution of a derivation for an open assumption in natural deduction. If e(X) has no open door in S′ then e(X) remains unchanged after an application of (2). Hence consideration of the doors of an empire provides adequate information about dependencies in a subderivation, in particular about the effects of the process of substitution on a subderivation.

2.3. Chains; Properties of Empires.

Let S be a proof structure for MLL^{−} or NCMLL^{−}. Suppose X, Y and A ⊗ B are formula occurrences in S, such that X ⊀ A and Y ⊀ B. We write X − (A ⊗ B) − Y if axioms connect X with A and B with Y, i.e., if there are axioms \overline{P′, …, P} and \overline{Q, …, Q′} such that P′ ≺ X, P ≺ A, Q ≺ B, Q′ ≺ Y. A chain is a configuration of the form

X − (A_{0} ⊗ B_{0}) − (A_{1} ⊗ B_{1}) − … − (A_{n} ⊗ B_{n}) − Y.

A chain is pure if A_{i} ⊗ B_{i} is a different formula occurrence from A_{j} ⊗ B_{j}, for i ≠ j. A pure chain where Y is A_{0} ⊗ B_{0} is called a cycle (this include the case of a conjunction A_{0} ⊗ B_{0}, where A_{0} and B_{0} are connected by an axiom). We say that a proof structure satisfies the acyclity condition if it contains no cycle. 2.3.1. Quasi-Transitivity Lemma. Assume A ∈ e(B) and B ∈ e(C), and moreover suppose that τ : [B] → A is a computation tree in which no sequence contains a step of the form ↓ \frac{C}{X} or ⇓ \frac{C}{X} for any X. Then A ∈ e(C). 2.3.2. Corollary. If B C, then e(B) ⊂ e(C). Hence is a strict partial order. 2.3.3. Proposition. Suppose B ⊀ A and let α be any sequence in a normal τ : [A] → B;

(1) if the last step in α has the form (↑), then there exists C_{0} ⊗ C_{1} such that α ends with

↓ \frac{C_{i}}{C_{0} ⊗ C_{1}} , ↑ \frac{C_{1−i}}{C_{0} ⊗ C_{1}} , only (↑) steps;

(2) if the last step of α has the form (↓) or (⇓), then there exists an axiom \overline{X_{1}, …, X_{p}} such that α ends with

↑ \frac{X_{i}}{Y} , only (↓) or (⇓) steps.

2.3.4. Corollary. (i) Every α in τ : [A] → B is a chain. (ii) The acyclicity condition implies the vicious circle condition. Remarks. (i) The converse is not true, i.e., a chain need not belong to the empire of its first member. However, if the connectedness condition holds, then for every chain C there is an element A_{i} ⊗ B_{i} such that for every A_{j} ⊗ B_{j} ∈ C with j ≠ i, we have A_{j} ⊗ B_{j} ∈ e(A_{i}) ∪ e(B_{i}). Using the Tiling Lemma below, we can show that if C is cyclic, then the vicious circle fails for A_{i} ⊗ B_{i}. That is, the vicious circle and connectedness condition imply the acyclicicty condition. (ii) In general, absence of cycles is a stronger condition, of conceptual interest since it guarantees consistency for systems in which the connectedness condition is not required in general. Such systems are variants of direct logic. Consider the language of multiplicative linear logic without the constants ⊥ and 1 and let DL, DL^{+} be the logics formalized by the extension of sequent calculus for MLL with the rule of Mingle or Weakening, respectively (see section 1.2). We have the following result below, ^{4} which provides an alternative proof of the sequentialization theorem for MLL. Call a non-empty set P of axiom links in a proof structure with conclusions Γ a path for Γ if it satisfies the following relevance condition on conjunctions. We write P ↦ X if for some \overline{P, P^{⊥}} ∈ P, we have P ≺ X or P^{⊥} ≺ X; then the relevance condition on A ∘ B requires that P ↦ A if and only if P ↦ B. A path P for Γ is minimal if no proper subset is a path for Γ. It is easy to show that minimality of P is equivalent to the connectedness condition (for those disjunctions and pairs of conclusions for which the relevance condition holds). Theorem. ⊢ Γ is provable without Cut in the calculus of sequents for DL [DL^{+}] if and only if there is a proof structure S with conclusions Γ such that the axiom links are a [minimal] path for Γ and no chain is a cycle in S.

2.4. Properties of consistent Proof Structures.

2.4.1. Proposition. Let S be a proof structure for MLL^{−} or NCMLL^{−} satisfying the vicious circle condition and let τ : [A] → B be normal.

(i) if B is C_{0} ⊗ C_{1} and no α ∈ τ : [A] → B ends with a step ↓ \frac{C_{i}}{C_{0}⊗C_{1}} , then C_{i} A; (ii) If B ≺ A, then B A. (iii) if all α ∈ τ : [A] → B end with a step of the form (↑), then B A. Proof. (i) Clearly C_{i} ∈ e(A). Also, C_{1−i} ∈ e(A) and by the assumption of the case from τ : [A] → B we can build a normal tree τ : [A] → C_{1−i} which does not contain any

4 Bellin and Ketonen present a proof of the sequentialization theorem for DL^{+}. Proofs of the sequentialization theorem for DL and DL^{+} can be found in Bellin . step ↓ \frac{C_{i}}{C_{0}⊗C_{1}} . Now if A ∈ e(C_{i}) then C_{1−i} ∈ e(C_{i}), by the Quasi-Transitivity Lemma (2.3.1.),and this is a ‘vicious circle’. (ii) We assume that A ∈ e(B), in order to find a contradiction. We claim that there is a conjunction D_{0} ⊗ D_{1} ∈ e(B) and a normal tree τ : [B] → D_{0} ⊗ D_{1} with the property that B ≺ D_{j} and every β in τ : [B] → D_{0} ⊗ D_{1} ends with the step ↓ \frac{D_{1−j}}{D_{0}⊗D_{1}} . It follows from our claim that ↓ \frac{D_{j}}{D_{0}⊗D_{1}} never occurs in τ : [B] → D_{0} ⊗ D_{1}. Consider the subtree τ : [B] → D_{j−1}; since obviously B ∈ e(D_{j}), we can apply the Quasi-Transitivity Lemma to obtain D_{1−j} ∈ D_{j}, which is a ‘vicious circle’.

To prove the claim, let τ : [B] → A be normal. If some α ∈ τ : [B] → A ends with a step (↑), then the desired D_{0} ⊗ D_{1} is given by Proposition 2.3.3. in the last section. Otherwise, starting from the root A of τ : [B] → A proceed as follows. If A is X_{0} ⊔ X_{1}, then a branching ⇓ \frac{X_{0} X_{1}}{X_{0}⊔X_{1}} occurs, and we choose the subtree τ′ : [B] → X_{j} such that B ≺ X_{j}. Otherwise, A is X_{0} ⊗ X_{1} and every sequence in the tree under consideration ends with a step ↓ \frac{X_{k}}{X_{0}⊗X_{1}} . If B ⊀ X_{k}, then we must have B ≺ X_{1−k}, and we are done. If B ≺ X_{k}, then consider the subtree τ′ : [B] → X_{k}. Since there are only finitely many Y such that B ≺ Y in S, failure to encounter the desired D_{0} ⊗ D_{1} would mean that we end with a step ↓ \frac{Y_{i}}{Z} or ⇓ \frac{Y_{0} Y_{1}}{Y_{0}⊔Y_{1}} where Y_{i} is B itself. But this is absurd, since such a step is not admissible in a computation of e(B).

Part (iii) easily follows from (i), (ii) and proposition 2.3.3.

2.5. Properties of Proof Nets.

2.5.1. Proposition. Let S be a proof net for MLL^{−} or NCMLL^{−}. The following are equivalent:

(i) B A; (ii) for some door D of e(B), there is a normal τ : [A] → D such that every α ∈ τ : [A] → D ends with a step (↑); (iii) there is a normal τ : [A] → B such that every α ∈ τ : [A] → B ends with a step (↑). Proof. (iii) ⇒ (i) is part (iii) of the proposition in the last section and (i) ⇒ (ii) is trivial. (ii) ⇒ (iii). If D is the main door of e(B), then we are finished. Otherwise, the last step in every sequence in τ : [A] → D crosses a link \frac{C D}{C⊔D} by a step (↑). By changing the last step of every sequence we obtain a tree τ : [A] → C. By part (iii) in Proposition 2.4.1. e(C) ⊂ e(A). By the connectedness condition C♢D.

Next consider a normal tree τ : [C] → D and α ∈ τ : [C] → D. Since D ∈ e(C) ∩ e(B) and C ∉ e(B), α ∈ τ : [C] → D must enter e(B) through some door D′ by a step (↑). If D′ is the main door, i.e., D is B, then the subtree τ : [C] → B cannot contain steps ↓ \frac{A}{Z} or ⇓ \frac{A}{Z}, since e(C) ⊂ e(A); combining with τ : [A] → C we obtain a tree τ : [A] → B. (Notice that the computation represented by τ : [A] → B takes place outside e(B), except for the last step. If τ : [A] → C is not normal, simplification certainly yields a normal τ′ : [A] → C with the desired property.) Otherwise, D′ is a closed door of e(B) and the last step of α has the form ↑ \frac{D′}{C′⊔D′}. We obtain trees τ : [C] → C′ and τ : [A] → C′; the computations they represent take place entirely outside e(B). Again we have C′♢D′, by connectedness.

Proceeding in this way, we obtain a sequences of doors D, D′, D′′,... and a sequence C, C′, C′′,... such that

… e(C′′) e(C′) e(C) e(A) ⊂ S.

This implies that C, C′, C′′, are distinct formula occurrences in S; thus C ⊔ D, C′ ⊔ D′, C′′ ⊔ D′′,... are also distinct. But S is finite, thus we cannot have an infinite discending sequence of proper inclusions. Therefore we eventually reach a D^{∗} which is the main door of e(B), by a computation taking place outside e(B), as required. 2.5.2. Tiling Lemma. (cf. Girard , II.1, Proposition 3) Let S be a proof net for MLL^{−} or NCMLL^{−}. Let A, B ∈ S be such that A∅B. Then e(A) ∩ e(B) = ∅. Proof. Suppose X ∈ e(A) ∩ e(B). We show that A ∉ e(B) implies B ∈ e(A). Consider any sequence in a normal τ : [A] → X: since A ∉ e(B), α must enter e(B) through some door D by a step (↑). Consider the subtree τ : [A] → D and apply proposition 2.5.1. in the direction (ii) ⇒ (i).

2.5.3. Sequentialization Theorem. (cf. Girard , II.1, Remark 2.) Every proof net in MLL^{−} and in NCMLL^{−} is an IPS. Proof. (MLL^{−}) By induction on the number of formulas in S. If S is an axiom there is nothing to prove, and if the conclusions of S contain a disjunction A ⊔ B, then the result is immediate from the inductive hypothesis. Let Γ be the set of conclusions and of ghosts of S and suppose every formula occurrence in Γ is the conclusion of a ⊗ link. We need to find a link \frac{A B}{A⊗B} with the property that if S′ results from S by removing only the link in question, then S is partitioned in two subnets S_{1} = e(A) and S_{2} = e(B).

Suppose for some A ⊗ B ∈ Γ all the doors of e(A) and of e(B) are open or ghosts. Then for every C ∈ Γ \ {A ⊗ B}, either C ∈ e(A) or C ∈ e(B). To see this, let C ∈ Γ be outside e(A) ∪ e(B). There cannot be any axiom connecting C with any formula in e(A) or of e(B), since otherwise some D ≺ C would be a door of either e(A) or of e(B). This implies that A ⊗ B and C belong to substructures of S which are disconnected, i.e., we cannot have A ⊗ B♢C, a contradiction.

We show that it is enough to find an element A ⊗ B of Γ such that e(A) or e(B) is maximal with respect to inclusion. If A_{0} ⊗ B_{0} ∈ Γ is such that B_{0} has a side door D, then D ≺ A_{1} ⊗ B_{1} ∈ Γ, say D ≺ A_{1}. Since D ∈ e(B_{0}) ∩ e(A_{1}) and A_{1} ∉ e(B_{0}), the Tiling Lemma yields B_{0} ∈ e(A_{1}); hence e(B_{0}) ⊂ e(A_{1}). We also obtain e(A_{0}) ⊂ e(A_{1}) as follows. B_{0} ∈ e(A_{1}) implies A_{0} ⊗ B_{0} ∈ e(A_{1}), hence A_{0} ∈ e(A_{1}). Now A_{1} ∈ e(A_{0}) would imply D ∈ e(A_{0}) ∪ e(B_{0}), thus by the Tiling Lemma A_{0} ∈ e(B_{0}) or B_{0} ∈ e(A_{0}), a ‘vicious circle’. Hence e(A_{0}) ∪ e(B_{0}) e(A_{1}) i.e., neither e(A_{0}) nor e(B_{0}) can be maximal with respect to inclusion.

To extend the above argument to the case of NCMLL^{−}, we also need to show that in the non-trivial case there are cyclic orderings _{1} and _{2} with the following property. Let Δ, A and B, Λ be the lowermost formula occurrences in e(A) and e(B), ordered according to _{1} and _{2}, respectively: then Δ, A ⊗ B, Λ is Γ in the given ordering .

By applying a cyclic permutation to Γ, if necessary, we may assume that Γ in the given ordering is

C_{1}, …, C_{i−1}, A ⊗ B, C_{i+1}, …, C_{n}

where C_{1} is in e(A), and Δ_{1} = C_{i+1}, …, C_{n} are in e(B). Let Δ_{0} be the set of C_{j} such that C_{j} is in e(B) and j < i; suppose Δ_{0} is non-empty. By connectedness there must be an axiom \overline{P, …, P′} that connects some formula in Δ_{0} with a formula in Δ_{1}, say P ≺ Δ_{0}. Therefore we can partition Λ into Λ_{0} and Λ_{1}, according to their position relatively to P in the given ordering , say C_{1} ∈ Λ_{0} and A ∈ Λ_{1}. Again by connectedness we must have an axiom \overline{Q, ⋯, Q′} connecting Λ_{0} and Λ_{1}, say Q ≺ Λ_{0}. Hence

Q P Q′ P′

violates the planarity condition. Hence Δ_{0} is empty, and the ordering _{1} and _{2} are easily obtained.

By applying the Tiling Lemma and similar techniques we can prove the following useful facts. 2.5.2. Door Lemma. Let S be a proof net for MLL^{−} or NCMLL^{−}, let A occur in S and let D, D′ be any two doors of e(A). Then e(A) ⊂ e(D) and D♢D′. 2.5.3. Shared Empires Lemma. (cf. Girard , II.2) Let S be a proof net for MLL^{−} or NCMLL^{−} and let A♢B in S. e(A) ∩ e(B) is the set of all formula occurrences X in S such that X ∈ e(A) and X ∈ e(B) can be computed without exiting e(A) ∩ e(B).

The Subnet Lemma (section 5) is an immediate consequence of the Shared Empires Lemma.

2.6. Extension to First Order Proof Nets.

The notions of proof structure with non-logical axioms and of substructure are defined in section 1.3.

Let S′ be a proper substructure of S, where the inclusion map strongly preserves the axioms, and let Δ be the conclusions of S′. The complementary substructure \overline{S} of S′ in S is the set S \ S′, satisfying the same links as S (relatively to S \ S′) and in addition the axiom link \overline{Δ}. (Notice that strictly speaking \overline{S} is not a substructure of S.)

To sequent derivations with non-logical axioms there correspond the notions of IPS with non-logical axioms and of proof net with non-logical axioms. The results in the last sections, in particular the Tiling Lemma and Sequentialization Theorem, still hold for proof nets with non-logical axioms. Moreover we have the following 2.6.1. Lemma. If A and B both belong to S′ [to \overline{S}], then B ∈ e(A) in S′ [in \overline{S}] if and only if B ∈ e(A) in S Proof. Use the Shared Empires Lemma in the case of S′, and direct consideration of a computation tree τ : [A] → B in the case of \overline{S}. It follows that S is a proof net if and only if S′ [and \overline{S}] are proof nets [with non-logical axiom Δ.]

To prove the Sequentialization Theorem in the first order case, we reduce to the propositional case by induction on the number of eigenvariables as follows. Let S be a proof net for first order MLL^{−} with conclusions Γ, where all formulas in Γ are closed. Notice that eigenvariables may still occur in the ghosts of S, although no eigenvariable occurs in the conclusions of S. Choose an eigenvariable a maximal with respect to the ordering <_{t}, and let S_{A} be e(A(a)), where a corresponds to a link \frac{A(a)}{⋀ x.A}. Let S′ be

e(⋀ x.A), which coincides with

\begin{matrix}S_{A} \\ A(a) \\ ⋀ x.A \end{matrix}

Let \overline{S} be the complementary substructure of S′ in S. In S_{A} the eigenvariable a can be regarded as a constant without affecting correctness and no eigenvariable occurs in any conclusion, apart from the occurrences of a in A(a), since a is maximal w.r.t. <_{t}. Finally, a does not occur in \overline{S}.

We want to apply the induction hypothesis to S_{A} and to \overline{S}. We claim that the ordering <_{t} is strict in S_{A} and in \overline{S} is strict since it is strict in S. In fact, the impossiblity of b <_{t} c <^{0} b in \overline{S} follows from Lemma 2.6.1. and in S_{A} from the following 2.6.2. Proposition. Let S be a proof net for first order MLL^{−} and let a, b be eigenvariables, where a is associated with \frac{A(a)}{⋀ x.A}. If b = a or b <_{t} a, then b occurs only inside

e(A(a)).

2.7. Extension to the full Multiplicative Fragment.

To extend the above results to the fragments MLL or NCMLL containing axioms and rules for 1 and ⊥, we use the extended definition of proof structure with 1 axioms and ⊥ links, as in section 1.3. We extend the definition of empire by adding to conditions (iii) and (iv) the cases (iii) if \frac{Y}{X_{0} X_{1}} is a ⊥-link in S and X_{i} ∈ e(A), X_{1−i} ∈ e(A) (→-step);

(vi) if \frac{X}{Y ⊥} is a ⊥ link in S X ≠ A and X ∈ e(A), then Y ∈ e(A) (↓-step). All the previous results still hold in this context. Remarks. (i) Given a ⊥ box

\begin{matrix}S′ \\ Γ \\ Γ ⊥ \end{matrix}

we must choose one formula in Γ to create the ⊥ link, performing a non-deterministic operation. (ii) In sequent calculus an application of the ⊥ rule can always be permuted with the inference immediately above it.^{5} Similarly, in a proof net we can ‘move ⊥ links upwards’ and still obtain a proof net. Hence we could also generalize the definition of proof structure by introducing axiom links of the form

\overline{P, P^{⊥}, ⊥, …, ⊥},

as well as \overline{1}.

3. Part II. Proof Networks for Multiplicative and Additive Linear Logic.

We consider now the elimination of the ⊓ boxes. Our solution will be in two steps: first, we extend the characterization of proof nets in terms of empires to proof structures for MALL (or NCMALL); second, we develop Girard’s notion of slicing of a box, we introduce the notion of a quasi structure and define a generalized notion of empire over families of quasi structures. A family representing a correct proof (proof network) is one in which the multiplicative conditions (vicious circle and connectedness conditions) are satisfied by each quasi structure and the additive conditions (box and parameters conditions) are satisfied by the whole family according to the generalized notion of empire.

3.1. Empires in Proof Structures for MALL and NCMALL.

We define proof structures for MALL as for MLL, with in addition the ⊤ axioms

\overline{⊤, X_{1}, …, X_{n}}

for any X_{i} and n, and the following ⊓ and Contraction links

\frac{A B}{A ⊓ B} \frac{C′ C′′}{C} ,

5 Notice that if the latter is an ⊗ application, there is a non-deterministic choice of one branch (unless we decide that the ⊗ rule behaves ‘additively’ with respect all the formulas of the form ?A; but this may be regarded as a rather inelegant trick). where C, C′ and C′′ are occurrences of the same formula. The Contraction links are to be restricted as follows. Consider a proof structure with a ⊓ box

\begin{matrix}S′  S′′ \\ Ξ Γ′ A  Θ Γ′′ B \\ Γ  A ⊓ B \end{matrix}  (¶)

satisfying condition (§) of section 1.5, i.e., such that Γ, Γ′ and Γ′′ are the same multiset. In the case of NCMALL, we are given orderings S′, S′′ and of \overline{Γ, A ⊓ B} that preserve the correspondence (§). In the case of MALL there may be many ways of establishing the correspondence (§): we choose one. Let Γ be C_{1},…, C_{n}. Now we can regard the structure in (¶) as consisting of S′ ⋃ S′′ ⋃ Γ ⋃{A ⊓ B} with the same links and in addition and of a configuration of the form (¶¶) (a sequence of Contraction links and precisely one ⊓ link)

\frac{C′_{0} C′′_{0}}{C_{0}} … \frac{C′_{n−1} C′′_{n−1}}{C_{n−1}}  \frac{A B}{A ⊓ B} .  (¶¶)

The Contraction links in (¶¶) are justified by their association with the ⊓ link. We define a flagging function φ that associates each Contraction link with a ⊓ links and marks some ghosts and some premises of Contraction or ⊓ links as belonging to the ‘left’ or to the ‘right’ proof structure in the box. We may simply say that φ flags C′_{1},…, C′_{n}, A and the ghosts in Ξ with A and it flags C′′_{1}, …, C′′_{n}, B and the ghosts in Θ with B. Of course, if C′_{i} is flagged with A, then C′′_{i} will be flagged with B, and viceversa. A ghost is external if it is not flagged with any formula occurrence.

We assume that every proof structure S in notation (¶¶) is given together with a flagging function φ. Clearly the difference between notations (¶) and (¶¶) is inessential.

Next we extend the definition of empire (section 2.1) to proof structures in notation (¶¶) by letting clause (v) be

(v) if \frac{X_{1} X_{2}}{X_{1}⊔X_{2}} [or \frac{X_{1} X_{2}}{X_{1}⊓X_{2}} or a Contraction \frac{X_{1} X_{2}}{X}] is a link in S, X_{1} ≠ A ≠ X_{2}, X_{1} ∈ e(A) and X_{2} ∈ e(A), then X_{1} ⊔ X_{2} [or X_{1} ⊓ X_{2} or X, respectively] is in e(A) (⇓ - step). We define a proof net for first order MALL [or NCMALL] as a proof structure satisfying the (1) vicious circle, (2) connectedness, (3) parameters, (4) box [and planarity] condition.

The vicious circle, parameters and planarity conditions are as before. The connectedness condition in this context is weakened:

(2) For every link \frac{X Y}{X⊔Y} in S, and for every X, Y that are conclusions of S or external ghosts, we have X♢Y.

We take the following formulation of the box condition:

(4) The official box condition: For every link \frac{A_{0} A_{1}}{A_{0}⊓A_{1}} , (i) the connectedness condition holds among all occurrences flagged with one of its

premises, i.e., for every D, if D is flagged with A_{i}, then D♢A_{i}; (ii) the no vicious circle condition holds for the ⊓ link, i.e., A_{0}∅A_{1}, and

(iii) for every premise A′ of a ⊓ link, A_{i}♢A′ implies A′ = A_{i}.

Remark. Such a formulation of the box condition may seem awkward, like the following Box Lemma. However, the advantage is that only (i) will remain as a condition, when the boxes are sliced.

The definition of inductively generated proof structures is easily extended to MALL and NCMALL. In the clause allowing the introduction of a link \frac{A_{0} A_{1}}{A_{0}⊓A_{1}} we require that the structures containing A_{0} and A_{1} are disjoint (as the case for ⊗ links, clause (2), section 1.4). The details are left to the reader. The verification that every IPS satisfies the box condition is almost immediate, thus we have 3.1.1. Theorem. Every IPS in MALL or NCMALL is a proof net.

The properties of empires (section 2.3) and of consistent proof structures (section 2.4) remain true. In addition, the main facts about boxes are the following. 3.1.2. Box Lemma. Let S be a proof net for MALL or NCMALL and let \frac{A_{0} A_{1}}{A_{0}⊓A_{1}} be a link in S.

(i) If X ∈ e(A_{i}), then e(X) ⊂ e(A_{i}); (ii) no closed door of e(A_{i}) is a premise of a ⊔ link; (iii) the doors of A_{i} are precisely the formula occurrences flagged with A_{i} together with the ghosts flagged with some A′, where A′ A_{i}; (iv) if \frac{A′ A′′}{A′⊓A′′} is a link and A′ A_{i}, then A′′ A_{i};

(v) e(A_{0}) ∩ e(A_{1}) = ∅. Proof. (i) Let Y ∈ e(X) and consider any sequence in a normal computation τ : [X] → Y: if Y ∉ e(A_{i}), then there must be a step of the form ⇓ \frac{C D}{E}, where, say, D is a door of e(A_{i}). Since C ∉ e(A), the subtree τ : [X] → C must contain a step ⇓ \frac{C′ D′}{E′}, where, e.g., D′ is a door of e(A_{i}). Moreover C′ and C must be different formula occurrences, because τ : [X] → Y is normal; thus D is different from D′ too. By repeating this argument we obtain an infinite sequence D, D′…. of distinct doors of e(A_{i}), a contradiction, since S is finite. (ii) Let \frac{C D}{C⊔D} be a link in S with D ∈ e(A_{i}). By the connectedness condition, C♢D; by part (i), C ∈ e(A_{i}); hence D cannot be a door of A_{i}. (iii) If A and A′ are premises of two distinct ⊓ links, by the box condition we have only three possibilities, A A′ or A∅A′ or A′ A. By Corollary 2.3.2, is a strict partial ordering. Therefore we can argue by induction on over the set of premises of ⊓ links.

Fix i, say i = 0. The fact that every formula flagged with A_{0} is a door of e(A_{0}) follows from the following remarks. A_{0} is a door of e(A_{0}) by part (ii) of Proposition 2.4.1. A ghost flagged with A_{0} is obviously a door. Let X′ be flagged with A_{0} and occur in a Contraction link \frac{X′ X′′}{X}. Hence X′′ is flagged with A_{1} and A_{1} ∈ e(X′′) by the box condition. If X ∈ e(A_{0}), then also X′′ ∈ e(A_{0}), hence A_{1} ∈ e(A_{0}) by part (i), contradicting the box condition. Hence X ∉ e(A_{0}), and X′′ is a door of e(A_{0}).

We prove that every door of e(A_{0}) is flagged with A_{0}. This is true of the main door A_{0}. Let D be a door of e(A_{0}), with D ≠ A_{0}. First, D cannot be a conclusion of S nor an external ghost, since this implies A_{1} ∈ e(D) by connectedness, hence A_{1} ∈ e(A_{0}) by part (i), contradicting the box condition. Second, let D be a ghost flagged with A′. By the box condition A′ ∈ e(D); by part (i) we have A′ ∈ e(A_{0}); using again the box condition we obtain either A′ = A_{0} or A′ A_{0}, as required. Third, if D is a closed door of e(A_{0}), then it must be a premise of a ⊓-link or of Contraction link, say \frac{D C}{E}, by part (ii). Now every such premise is flagged, say D is flagged with A′ and C is flagged with A′′ for some \frac{A′ A′′}{A′⊓A′′}. As before we obtain A′ ∈ e(A_{0}). We claim that A_{0}♢A′: by the box condition the claim implies A_{0} = A′, as required. If not, the only possibility is A′ A_{0}, hence by the induction hypothesis every door of e(A′) is flagged with A′. A door X of e(A′) is certainly encountered in any normal computation τ : [A_{0}] → A′, which must contain a step ↑ \frac{X Y}{Z} . Since by induction hypothesis X is flagged with A′, Y must be flagged with A′′, and by the box condition C♢Y. But obviously Y ∈ e(A_{0}), hence C ∈ e(A_{0}), contradicting the fact that D is a door of e(A_{0}). (iv) In any α in τ : [A_{i}] → A′ consider a step of the form ↑ \frac{C D}{E}, where D is a door of A′ and apply parts (i) and (iii).

(v) Let X ∈ e(A_{0}) ∩ e(A_{1}). First notice that X can be neither a conclusion of S nor an external ghost, by the connectedness condition for S and part (i). Next, X can be neither a ghost flagged with A_{i} nor a closed door of e(A_{i}): by parts (iii) and (i) this implies A_{i} ∈ e(A_{1−i}), a contradiction.

Now suppose that X ∈ e(A_{0}) ∩ e(A_{1}) is a ghost flagged with A′, where A′ is a premise of a ⊓ link and A′ A_{i}. By part (iv) the conclusion of that link also belongs to e(A_{0})∩e(A_{1}) and we consider the first Y such that A′ ≺ Y and Y is a door of e(A_{i}). By the argument of the previous paragraph, this can only be a ghost flagged with some A′′. Proceeding this way, we obtain an infinite sequence of premises of ⊓ links

… A′′ A′ A_{i}

which is impossible, since S is finite.

Finally, if X is not a door of e(A_{0}) nor of e(A_{1}), consider the first D ∈ e(A_{0}) ⊓ e(A_{1}) such that X ≺ D and D is a door of e(A_{i}) and we apply the previous argument to D. It is now immediate that the official box condition implies version 1 of the same condition, if in (2) we take S′ = e(A), S′′ = e(B) and let

S^{o} = S \ (e(A) ∪ e(B))

with the additional non-logical axiom \overline{Γ, A ⊓ B}. It is also easy to see that version 2 of the box condition follows from the official box condition: by continuing the above decomposition until all ⊓ links are eliminated, we obtain a class C of multiplicative proof structures (with non-logical axioms and ⊗ links). The relation ◁_{t} is obtained from applied to premises of ⊓ links.

3.1.3. Proposition. Let S be a proof net for MALL or NCMALL and let C be the collection of proof nets for MLL or NCMLL ( with non-logical axioms and ⊗ links) resulting by decomposing all the ⊓ links in S. For every S_{0} ∈ C, if A and B both belong to S_{0}, then B ∈ e(A) in S if and only if B ∈ e(A) in S_{0}. Proof. By direct inspection of normal trees τ : [A] → B in S_{0} or in S. 3.1.4. Sequentialization Theorem. If S is a proof net for MALL and NCMALL, then S is an IPS. Proof. By induction on ◁_{t}, using the above proposition and the Sequentialization Theorem for MLL or NCMLL (extended with ⊕ links and non-logical axioms).

3.2. Quasi Structures and Structures.

A Quasi Structure Q is defined as a proof structure for MALL or NCMALL except that (a) there are no Contraction links and (b) ⊓ links have only one premise:

\frac{X}{X ⊓ Y} \frac{Y}{X ⊓ Y} .

Maps preserving links, axioms and conclusions are defined for Quasi Structures as in the case of proof structures.

We want to define the category Struct of Structures, whose objects are either proof structures for MALL or Quasi Structures and whose maps are embeddings (and similarly for the definition of the category of NCStrct of noncommutative structures). We need to define an appropriate notion of embedding of a Quasi Structure in a proof structure.

A segment σ in S is a sequence of occurrences C_{0},…,C_{n} of the same formula with the property that

(1) C_{0} is not the conclusion and C_{n} is not the premise of a Contraction link;

(2) if 0≤i < n, then C_{i+1} the conclusion of a Contraction link with premise C_{i}. Given a segment σ = C_{0}, …, C_{m}, we say (with some abuse of terminology) that σ is a premise [conclusion] of a link if and only if C_{m} is a premise [C_{0} is a conclusion] of it. We use the notation

\overline{σ_{1} …, σ_{k}}  \frac{σ_{1}}{σ}  \frac{σ_{1} σ_{2}}{σ}

with the obvious meaning. Given a map m : Q → S, where Q is a Quasi Structure and S a proof structure, we say that m preserves an axiom or a ∘ link

\overline{A_{1} …, A_{n}}, \frac{A_{1} A_{2}}{B} or \frac{A_{0}}{B}

if there are segments σ_{i} in S and an axiom or a ∘ link such that

\overline{σ_{1} …, σ_{k}}, \frac{σ_{1} σ_{2}}{σ} or \frac{σ_{1}}{σ}

and moreover m(A_{i}) ∈ σ_{i} and m(B) ∈ σ. Here of course [the premise of] a unary ⊓ links is mapped to [a formula occurrence in a segment which is a premise of] a binary ⊓ link. Finally, we extend the notion of preserving the conclusions in a similar way.

Let Struct^{∗} be the category whose objects (O, A) are structures O with a selected conclusion A and whose morphisms are embeddings preserving links and selected conclusion. Consider the assignments

Times  ((O_{1}, A), (O_{2}, B)) ↦ (O_{1} _{\frac{A  B}{A⊗B}} O_{2}, A ⊗ B)

Plus  (O, A) ↦ (O_{\frac{A}{A⊕B}} , A ⊕ B)  (O, A) ↦ (O_{\frac{B}{B⊕A}} , B ⊕ A)

Exists  (O, A(t)) ↦ (O_{\frac{A(t)}{∃x.A}} , ∃x.A)

Fact. The assignment Times determines a bifunctor on Struct^{∗}. Given B or t, the assigments Plus or Exists determine functors on Struct^{∗}.

3.3. Slicings of Proof Nets for MALL and NCMALL.

Let ι : O → O′ be an injective mapping such that X and ι(X) are occurrences of the same formula, for all X ∈ O. Suppose first the both O and O′ are either proof structures or quasi structures. We say that ι is a quasi-embedding if

(1) ι preserves all links different from axioms;

(2) ι preserves axioms in the weak sense that it maps an axiom

\overline{X_{1}, …, X_{n}}  to  \overline{ι(X_{1}), …, ι(X_{n}), Y_{1}, …, Y_{p}};

(3) whenever ι(X_{i}) and ι(X_{j}) occur in an axiom \overline{Y, …, ι(X_{i}), …, ι(X_{j})} of O′, then also X_{i}, X_{j} occur in one axiom of O. We extend the notion of quasi-embedding to the case ι : Q → S by considering segments as above. Example. Consider the following proof-structure S.

\begin{matrix}A  A^{⊥} & A  A^{⊥} \\ A ⊓ A^{⊥} & A ⊔ A^{⊥} \end{matrix}

There are quasi-embeddings of the following Quasi Structures Q_{1}, Q_{2} into S. Here \overline{A} and \overline{A^{⊥}} are non-logical axioms.

Q_{1} :  Q_{2} :

A^{⊥}  A \overline{A^{⊥}}  A  \overline{A}  A^{⊥}
A ⊓ A^{⊥}  A ⊔ A^{⊥}  A ⊓ A^{⊥}  A ⊔ A^{⊥}

Let Q_{3} be

\frac{\overline{A}}{A ⊓ A^{⊥}} \frac{\overline{A} \overline{A^{⊥}}}{A ⊔ A^{⊥}}

Then there is no quasi-embedding of Q_{3} in S nor between Q_{1}, Q_{2} and Q_{3}. Define Slicing(S) to be the set of all quasi-embeddings ι : Q → S preserving conclusions. We let

Fam(S) = {Q : for some ι in Slicing(S), ι : Q → S}.

Details for the noncommutative case are left to the reader.

3.4. Proof Networks for MALL and NCMALL.

Given a proof structure S for MALL or NCMALL, let F = Fam(S). Define an equivalence relation R on ⋃ F by letting A′ R A′′ if and only if there are ι′, ι′′ in Slicing(S) such that ι′(A′) = ι′′(A′′). If A = ι′(A′), we let [A] be the corresponding equivalence class. of formula occurrences. If A′ ∈ Q ∩ [A], then A′ is unique, and in this case we sometimes write A^{Q} for A′.

For any Q ∈ F the definition of empire of a formula occurrence is as in section 4. Let F = Fam(S) as before. The empire e[A] of an equivalence class [A] is a set of equivalence classes, defined as follows: [B]∈e[A] in F if and only if for every Q∈F such that [B] ∩ Q ≠ ∅, we have [A] ∩ Q ≠ ∅ and B^{Q}∈e(A^{Q}) in Q.

In this context the box condition is as follows. Given S with flagging function φ, let and F = Fam(S). Slicing Box Condition: (1) for every D, D′ ∈ S, if D and D′ are flagged with the same formula, then [D]♢[D′] in F;

(2) every ι ∈ Slicing(S is an embedding.

A family F = Fam(S) is a proof network if every Q ∈ F satisfies the vicious circle and connectedness condition and F satisfies the slicing box condition.

3.4.1. Proposition. Let S be a proof structure for MALL or NCMALL. Let F be Fam(S).

(i) If \frac{X_{0}}{Y} [ or \frac{X_{0} X_{1}}{Y} ] is a ∘-link in S different from a ⊓ or Contraction link, then for

each Q ∈ F either [X_{0}] ∩ Q = [X_{1}] ∩ Q = ∅ = [Y] ∩ Q or \frac{X_{0}^{Q}}{Y^{Q}} [ or \frac{X_{0}^{Q} X_{1}^{Q}}{Y^{Q}} ].

(ii) Conversely, every link in Q different from a ⊓ link can be written as \frac{X^{Q}}{Y^{Q}} or \frac{X_{0}^{Q} X_{1}^{Q}}{Y^{Q}} in correspondence with some link of the same type in S. (iii) For every link \frac{X_{0} X_{1}}{X_{0}⊓X_{1}} in S, for every Q ∈ F and for some i = 0, 1, either [X_{i}] ∩ Q

= ∅ = [Y] ∩ Q or \frac{X_{i}^{Q}}{(X_{0}⊓X_{1})^{Q}}. If Z_{0} ⪯ X_{0} and Z_{1} ⪯ X_{1}, then [Z_{0}] ∩ [Z_{1}] = ∅.

(iv) Conversely, every ⊓ link in Q can be written as \frac{X_{i}^{Q}}{(X_{0}⊓X_{1})^{Q}} in correspondence with some link \frac{X_{0} X_{1}}{X_{0}⊓X_{1}} in S. Suppose F satisfies the box condition.

(v) For every axiom \overline{X_{1}, …, X_{n}} ∈ S and every Q ∈ F, either [X_{i}] ∩ Q = ∅, for all i ≤ n, or \overline{X_{1}^{Q}, …, X_{n}^{Q}} is an axiom of Q.

(vi) Conversely, every axiom of Q can be written as \overline{X_{1}^{Q}, …, X_{n}^{Q}} in correspondence with some axiom \overline{X_{1}, …, X_{n}} of S. (vii) For every Contraction link \frac{X Y}{Z} in S, [X] ∪ [Y] = [Z] and for every Z_{0} ⪯ X and Z_{1} ⪯ Y, [Z_{0}] ∩ [Z_{1}] = ∅.

3.4.2. Equivalence Theorem. Let S be a proof structure for propositional MALL or NCMALL.

(i) If Fam(S) satisfies the box condition, then B ∈ e(A) in S if and only if [B] ∈ e[A] in Fam(S), for all A, B; (ii) S is a proof net if and only if Fam(S) is a proof network. Proof. (i) Using the proposition above, given a computation for B ∈ e(A) in S we obtain family of computations of B^{Q} ∈ e(A^{Q}) for each B^{Q} in [B], and conversely. (ii) If S is a proof net, then it is generated inductively and so is F, i.e., each Q in F can be generated inductively. By theorem 2.2.1. (extended to quasi structures), each Q in F satisfies the vicious circle and connectedness conditions. Also in the inductive generation of F each axiom of Q ∈ F is defined as a copy of an axiom of S and the box condition for F follows from the connectedness condition.

Conversely, if F is a proof network, then by part (i) we immediately obtain that the vicious circle and connectedness conditions hold for S. To show that the official box condition (condition (4), section 3.1) also holds for S, consider that condition (4)(i) is immediate from the slicing box condition for F and part (i). Next notice that for every \frac{X′ X′′}{X′⊓X′′} in S there are Q′ and Q′′ in F such that [X′] ∩ Q′ ≠ ∅ ≠ [X′′] ∩ Q′′ and [X′′] ∩ Q′ = ∅ = [X′] ∩ Q′′. Therefore condition (4)(ii) is immediate, again by part (i). To prove condition (4)(iii), consider two distinct ⊓ links in S, with conclusions X = X_{0} ⊓ X_{1} and Y = Y_{0} ⊓ Y_{1} and write X ◁ Y if X ⪯ Z, where Z is a formula flagged with Y_{i}, for i = 0 or 1.

On one hand, suppose X ◁ Y, say X ≺ Z♢Y_{0}, and consider a Q ∈ F such that [X_{i}] ∩ Q ≠ ∅. Then X_{i}^{Q} ∈ e(Z^{Q}) and X_{i}^{Q} ∈ e(Y_{0}^{Q}) (using the slicing box condition) and moreover [X_{1−i}] ∩ Q = ∅. This proves [X_{i}] ∈ e[Y_{0}] and [Y_{0}] ∉ e[X_{1−i}]. Excanging X_{i} and X_{1−i} and applying part (i), we obtain X_{0} Y_{i} and X_{1} Y_{i} in S.

On the other hand, if neither X ◁Y nor Y ◁X, then for each i, j = 1, 2 we can certainly find Q_{1} and Q_{2} in F such that

[X_{i}] ∩ Q_{1} = ∅ ≠ [Y_{j}] ∩ Q_{1}

and

[X_{i}] ∩ Q_{2} ≠ ∅ = [Y_{j}] ∩ Q_{2}

by construction of F. Hence in both cases we cannot have X_{i}♢Y_{j}.

Remark. Thus we have the following decision procedure for proof structures for propositional MALL: given S, test the multiplicative conditions for every Q ∈ Fam(S); next test the slicing box condition, and in particular, consider whether every quasi-embedding Slicing(S) is an embedding.

3.5. Slices.

In section 6, pp. 93-97 of Girard slices are defined for the whole system of linear logic, including exponentials. In particular, a slice for MALL is like a proof structure for MLL^{−}, with the addition of 1 axioms, unary ⊓ and ⊕, ⋀ and ⋁ links and of sets of formula occurrences that are not conclusions of any link and do not belong to any axiom.

In MALL maps ∗, ⋆ and • have been constructed

Sequent Derivations ⟶^{∗} Proof Nets ⟶^{⋆} Proof Networks ⟶^{•} Sets of Slices

that identify equivalent proofs. Notice that such a ∗ is unique in MLL^{−}, ⋆ is unique in MALL^{−} and • is unique in MALL.

It would be desirable to give sets S of slices an independent logical meaning, as much as possible. To do this, one must express in some way the restriction on S as a whole which is given by the ⊓ boxes, and the additional connections within each slice which is created by the ⊥ boxes. Assuming this to be done, the problem of irrelevance created by the slicing of ⊤ boxes is easily solved if we assume that each slice satisfies the relevance condition on conjunctions (cf. section 2.3.). This amounts to the requirement that we check logical correctedness only after garbage collection, i.e., that S is the slicing of a proof structure which is normal with respect to the following reduction.

• Zero Commutation. A proof structure S is transformed into a proof structure S′ by replacing a configuration of the form

e(C)
⊤, X_{1}, …, X_{m}, B  C Y_{1}, …, Y_{n}
B ⊗ C

where Y_{1}, …, Y_{n} are all the doors of e(C), with the configuration

\overline{⊤, X_{1}, …, X_{m}, B ⊗ C, Y_{1}, …, Y_{n}}.

Notice that in a ⊤ box, an occurrence of ⊤ is marked as principal. Clearly, one effect of Zero Commutation on proof structures is to erase axiom link and markings on occurrences of ⊤. Define the path P of a proof structure S for MALL to be the set of axiom links different from a ⊤ axiom and of marked occurrences of ⊤ boxes (cf. section 2.3.). The following is clear: Proposition. Let S and S′ be proof structures for MALL, where S′ results from S by an application of Zero Commutation. If the path P of S is non-empty and S satisfies the vicious circle condition, then so does S′. The above notions can be easily transfered to slices. Moreover, in a slice the notion of empire of a formula can be relativized to the given path P: in the case of a link \frac{X_{0} X_{1}}{X_{0}⊔X_{1}} where X_{i} is irrelevant we let X_{0} ⊔ X_{1} ∈ e_{P}(A) if and only if X_{1−i} ∈ e_{P}(A). Therefore, if a slice satisfies the relevance condition on conjunctions, then the multiplicative consistency conditions are the vicious circle, connectedness conditions, relativized to the path P and, moreover, the requirement that P is non-empty. Details are left to the reader.

3.6. Strong Normalization Theorem.

The Strong Normalization Theorem for the system of proof nets (with boxes) for full second order linear logic is proved in Girard , Section 4, pp.60-78. The reader is referred to that paper for a definition of all the contraction rules (definitions 4.1.- 4.18.) and for a definition of contractions for slices (definition 6.4.). It is also remarked there that the Church-Rosser Property holds for proof nets only in the fragment MLL^{−}, but that it does hold for sets of slices in the full system.

As an illustration, we consider the case of propositional MALL^{−}, the additive fragment without propositional constants.

A Contraction for proof structures transforms S into S′ by one of the replacements indicated below.

• Axiom Contraction: A configuration of the form

A^{⊥}, A  A^{⊥}

is replaced by

A^{⊥}.

• Times Contraction: A configuration of the form

\begin{matrix}A & B & B^{⊥} & A^{⊥} \\ A⊗B & B^{⊥} ⊔ A^{⊥} \end{matrix}

is replaced by

\begin{aligned}& B & B^{⊥} \\ A & & & A^{⊥} \end{aligned}

• With Contraction: A configuration of the form

S_{0}  S_{1}
Γ A_{0}  Γ A_{1}  A_{i}^{⊥}
Γ  A_{0} ⊓ A_{1}  A_{0}^{⊥} ⊕ A_{1}^{⊥}

is replaced by

\begin{aligned}& S_{i} \\ Γ & & \underline{A_{i} A_{i}⊥} \end{aligned}

• With Commutation: A configuration of the form

S_{0}  S_{1}
A_{0} Γ C  A_{1} Γ C  e(D)
A_{0} ⊓ A_{1} Γ  C  D  Δ
C ⊗ D

is replaced by

S_{0} e(D) S_{1} e(D)
A_{0} Γ C D Δ  A_{1} ΓC D Δ
C ⊗ D  C ⊗ D
A_{0} ⊓ A_{1}  Γ  C ⊗ D  Δ

A Contraction for Quasi Structures is defined like for proof structures in the case of an Axiom contraction or Times contraction. There are no commutations.

• With Contraction: If a Quasi Structure Q contains a configuration of the form

\begin{matrix}A_{i} & A_{i}^{⊥} \\ A_{0} ⊓ A_{1} & A_{0}^{⊥} ⊕ A_{1}^{⊥} \end{matrix}

then Q′ is obtained from Q by replacing that configuration by

\underline{A_{i} A_{i}^{⊥}}.

A Quasi Structure Q containing a configuration

\begin{matrix}A_{i} & A_{1−i}^{⊥} \\ A_{0} ⊓ A_{1} & A_{0}^{⊥} ⊕ A_{1}^{⊥} \end{matrix}

is deleted (replaced by the empty set of formula occurrences).

3.6.1. Reduction Lemma. If S is a proof net for MALL^{−} or NCMALL^{−} and S′ results from S by application of one of the above contractions, then S′ is a proof net and ⋃ Fam (S′) contains less links than ⋃ Fam (S); if S′ results from S by commutation, then Fam (S′) = Fam (S). Proof. In the case of an Axiom or Times reduction, to prove that the vicious circle condition is preserved by a reduction it is convenient to argue as follows: suppose some Q′ ∈ Fam(S′) contains a cyclic chain and show that there is a Q ∈ Fam(S) that contains a cyclic chain. Further details can be found in Bellin . 3.6.2. Strong Normalization Theorem. In MALL^{−} or NCMALL^{−} every reduction sequence starting from S terminates, and Fam(S) reduces to a unique F.

4. Part III. Permutability of Inferences in the Sequent Calculus for Linear Logic.

As an application, we give a classification of permutability of inferences in linear sequent calculus. We do not define standard terminology: principal formula, active formulas, ancestors of a formula, etc.

The table below is to be interpreted as follows. Let I_{1}, I_{2} be inferences such that:

(i) I_{2} occurs immediately after I_{1}; (ii) the principal formula of I_{1} is not active in I_{2} (iii) I_{1} and I_{2} are of the type indicated in the horizontal and vertical entries, respectively, then I_{2} can always be permuted above I_{1}, unless explicitly indicated.

I_{1}:  ⊗  ⊔  ⊓  ⊕  !  Der  Weak  Contr  Cut

I_{2}:

⊗  no
⊔  no  no  no
⊓  no  no  no  no  no  no  no
⊕  no
!  no  no  no  no  no  no  no

Der

Weak

Contr  no  no
Cut  no

Remarks. (i) The fact that Cut can be permuted above any inference other than a ! rule is part of the proof of the Cut elimination theorem. In the case

!/Cut :

. . . . . . .  ⊢ ?(C^{⊥}),?Γ, A
I_{3}  I_{1}
⊢ Δ,!C  ⊢ ?(C^{⊥}),?Γ,!A
I_{2}

⊢ Δ,?Γ,!A

a permutation of I_{1} and I_{2} is permissible only if Δ has the form ?Λ, in particular, if I_{3} is itself a ! rule. (ii) A Cut I_{1} cannot be permuted below another inference I_{2} in the following case:

Cut /⊔ :
⊢ B, Δ, C^{⊥}  ⊢ C, Γ, A
I_{1}
⊢ B, Δ, Γ, A
I_{2}
⊢ A ⊔ B, Δ, Γ

A similar case arises for the pair Cut / Contraction. Cut can be permuted below a ! rule only if the Cut formula C is of the form ?D:

Cut /! :

⊢ ?Δ, C^{⊥}  ⊢ C,?Γ, A
I_{1}

⊢ ?Δ,?Γ, A

I_{2}

⊢ ?Δ,?Γ,!A

(iii) A permutation of Cut below a ⊓ rule is permissible only if I_{3} is also a Cut with premises ⊢ Δ, C and ⊢ C^{⊥}, Δ, A:

Cut/⊓ :
. . . . . . . .  ⊢ Δ, C^{⊥}  ⊢ C, Γ, B
I_{3}  I_{1}
⊢ Δ, Γ, A  ⊢ Δ, Γ, B
I_{2}
⊢ Δ, Γ, A ⊓ B

(iv) Because of the restrictions on the side formulas of the ! rule, in a derivation there cannot be a sequence of consecutive inferences I_{1}, I_{2} as above, where I_{2} is a ! rule and where I_{1} is one of the ⊗, ⊔, ⊓, ⊕, ! rules.

(v) The following sequents provide counterexamples to the permutability of the indicated inferences: Cut-free proofs of the following sequents must end with a pair of logical inferences in the fixed ordering.

!/⊗  ⊢ P^{⊥}, P ⊗?(Q^{⊥}),!Q

!/⊔  ⊢ ?(P^{⊥}) ⊔?(P^{⊥}),!P

!/⊓  ⊢ (?(P^{⊥})) ⊓ ⊤,!P

!/⊕  ⊢ (?(P^{⊥})) ⊕ Q,!P

⊕/⊓  ⊢ P^{⊥} ⊕ Q^{⊥}, P ⊓ Q

Der /⊓  ⊢ ?(P^{⊥}),!P ⊓ P

Weak /⊓  ⊢ ?(P^{⊥}), P ⊓ 1

Contr /⊓  ⊢ ?(P^{⊥}), P ⊓ (P ⊗ P)

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

⊗/ Contr  ⊢ ?(P^{⊥}), P ⊗ P

⊗/⊓  ⊢ S^{⊥} ⊕ T^{⊥}, (T ⊗ S^{⊥}) ⊕ R, S ⊗ [P^{⊥} ⊕ (R^{⊥} ⊗ Q^{⊥})], P ⊓ Q

With respect to the last counterexample, notice that the permutation of I_{1} with I_{2} is impossible in the following case

⊗/⊓ :
. . . . . . . . . . . . . . . .  ⊢ Δ, C  ⊢ D, Γ, B
I_{3}  I_{1}
⊢ Δ, C ⊗ D, Γ, A  ⊢ Δ, C ⊗ D, Γ, B
I_{2}
⊢ Δ, C ⊗ D, Γ, A ⊓ B

unless I_{3} is itself a ⊗ rule with premises ⊢ Δ, C and ⊢ D, Γ, A. Now let

Δ = S^{⊥} ⊕ T^{⊥}, C = S

and let

D = [P^{⊥} ⊕ (R^{⊥} ⊗ Q^{⊥})],  Γ = (T ⊗ S^{⊥}) ⊕ R,  B = Q

and notice that

⊬ (T ⊗ S^{⊥}) ⊕ R, [P^{⊥} ⊕ (R^{⊥} ⊗ Q^{⊥})], P.

Since the ! rule cannot be permuted above or below the ⊗, ⊔, ⊓ and ⊕ rules, the most interesting cases of a Permutability Theorem for linear logic can be stated simply for the fragment without ! rule.

For such a fragment we can define a notion of proof net as before and the links for ? require no modification in the definition of empire.

We define inductively what it means for an inference R in a deduction to introduce a formula-occurrence X: either X is the principal formula of R or X is a side formula and R introduces the immediate ancestor of X.

For simplicity, we consider only derivations in which every application of the ⊥ rule occurs above any other rule of inference. Let ∗ be the mapping sending each derivation to the corresponding proof net, and let ⋆ send each proof net to the corresponding proof network. We write D^{∗} = S, S^{⋆} = F. For each formula occurrence A in a derivation D, A^{∗} is a formula occurrence in the proof net D^{∗} and A^{∗⋆} is a class of formulas in the proof network D^{∗⋆}. Also, given a D such that D^{∗} = S and B in S, we write B^{−∗} for the set of formula occurrences X in D such that X^{∗} = B and similarly we write (e(B))^{−∗} for the inverse image of e(B) in D. 4.1. Permutability Theorem. Let D be any derivation of Γ in propositional linear logic. For every formula occurrence A in D there exists a derivation D′ with an inference R_{+} introducing an occurrence A′ of the same formula as A and with the following properties.

(0) D′ is obtained from D by permuting the order of the inferences.

(1) Suppose A is introduced in D by either the ⊗ rule or the ⊔ rule or by a Contraction with active formulas A_{1} and A_{2}; then R_{+} is an inference of the same kind and

(i) D^{∗} = (D′)^{∗};

(ii) in D′, (e(A_{1}^{∗})∪e(A_{2}^{∗}))^{−∗} is the set of formula occurrences that are introduced above R_{+}.

(2) Suppose A is introduced in D either by the ⊕ rule or by Weakening or Dereliction; then R_{+} is an inference of the same kind and

(i) D^{∗} = (D′)^{∗};

(ii) in D′, (e(A^{∗}))^{−∗} is the set of formula occurrences that are introduced above R_{+}.

(3) Suppose A is introduced in D by the ⊓ rule; then R_{+} is an inference of the same kind and

(i) D^{∗⋆} = (D′)^{∗⋆};

(ii) (e(A^{∗}))^{⋆} = (e(A′^{∗}))^{⋆} and in D′, (e(A′^{∗}))^{−∗} is the set of formula occurrences that are introduced above R_{+}. Proof. (1) Let R be the inference of D introducing A (we may suppose A is the principal formula of R) and consider the link

\frac{B_{1} B_{2}}{B}

in S = D^{∗}, where B = A^{∗}, etc. Let k be the number of formula occurrences Z^{∗} in S that belong to e(B) but such that Z is introduced below R. By induction on e(B) (see section 2.1), we reduce k by permuting the inferences of D. The cases of clauses (i) − (iii) in the definition of empire are trivial. Clause (iv): for a fixed i = 1, 2, X^{∗} ∈ e(B_{i}) and X ≠ B_{i} implies (X⊗Y)^{∗} ∈ e(B_{i}). By induction hypothesis we may assume that X is introduced above R. If R′ introduces the principal formula X⊗Y and occurs below R, there is a passive formula X′ in every sequent between R and R′ such that (X′)^{∗} = X^{∗}. By the table above, we can certainly permute R′ with the inference R′′ immediately above it. In this way it, we do not increase the number of formulas Z^{∗} in e(B_{i}) such that Z is introduced below R. After a finite number of steps, the inference introducing X⊗Y is permuted above R and we have reduced k.

Clause (v): X^{∗} ∈ e(B_{i}), Y^{∗} ∈ e(B_{i}) and X^{∗} ≠ B_{i} ≠ Y^{∗} imply (X ⊔ Y)^{∗} ∈ e(B_{i}). If R′ introduces the principal formula X ⊔ Y, then by the table above the only problematic case is when the inference immediately above R′ is a ⊗ rule. By induction hypothesis we assume that both X and Y are introduced above R. It follows that for each application R^{⊗} of the ⊗-rule between R and R′ both X and Y have ancestors only in one of the upper sequents of R^{⊗}. But in this case it is certainly possible to permute R′ with R^{⊗} too. The cases of clause (v) that deal with the conclusion of a ⊓ link or of a Contraction link flagged with a ⊓ link do not apply here. Indeed, if R′ introduces the principal formula X ⊓ Y and R occurs above R′, then B_{i}^{∗} ∈ e(X^{∗}) or B_{i}^{∗} ∈ e(Y^{∗}) and by the Box Lemma, section 3.1, e(B_{i}) ⊂ e(X^{∗}) or e(B_{i}) ⊂ e(Y^{∗}), hence (X ⊓ Y)^{∗} ∉ e(B_{i}). Finally, it is easy to see that if D_{1} comes from D_{0} by a permutation of inferences as before, then D_{0}^{∗} = D_{1}^{∗}. This concludes part (1). Parts (2) is similar. In part (3) we must expand the size of the with-box by with-commutation, but this does not enlarge the empire of A. Details are omitted.

5. Conclusion.

What has been achieved?

(I) We have provided a unified treatment of multiplicative and additive linear logic, essentially based on the notion of empire. We have already stressed the significance of the empire of a formula as a subnet in a proof net. The vicious circle, connectedness, box and parameters conditions depend on the possibility of a simple subdivision (tiling) of a structure and correspond to natural properties of proofs in linear logic.

(II) The slicing of a proof structure with boxes has the Church Rosser property as most obvious motivation. In the case of proof networks, the result from our slicing (the quasi structures) still maintain enough connections, so that the test of the multiplicative condition for correctness can still be done on them.

It may be asked whether proof networks are adequate per se to represent proofs, or only in connection with proof nets, as the outcome of the process of slicing. One could informally describe a proof network as a family of quasi structures satisfying certain properties. (a) All quasi structures in the family satisfy the conditions for consistency and relevance. In addition, (b) all quasi structures in the family are identified at the conclusions. It must be possible to chose the points of identification in such a way that the can be grouped in patterns of the form C_{1},…, C_{n}, A ⊓ B. (c) Putting the same flag on all the points of the same group, the set of substructures occurring above flagged points must constitute two subnetworks. To express these conditions precisely is complicated enough; the alternative route, the embedding of the family in a proof structure seems more elegant.

The importance of avoiding bricolage in the theory of slicing is related to our understanding of the distinction between 0 and ⊥: practically useful applications of this distinction would certainly encourage further attention to the matter.

It is not our intention to advertise proof networks as the ultimate representation of provability for the systems in question. Ultimately, the significance of formalisms has to be proved in applications. If slicing represents ‘the absolute limit for a parallelization of the syntax, i.e., the removal of all boxes but !-ones’ (Girard , p.94), then its value ought to be tested in the field of parallelism.

References. S. Abramsky : Computational interpretations of Linear Logic, manuscript, Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen’s Gate, London SW7 2BZ, England. P. Andrews : Theorem proving via general mating, J. ACM 28 (1981) pp. 193-214. A. Asperti : A Logic for Concurrency, Technical Report, Dipartimento di Informatica, Università di Pisa, 1987. G. Bellin : Mechanizing Proof Theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information, PhD thesis, Stanford Computer Science Department Technical Report STAN-CS-90-1319. G. Bellin : Ramsey Interpreted: A Parametric Version of Ramsey Theorem, Logic and Computation, Contemporary Mathematics 106, AMS, 1990, pp. 17-37. G. Bellin and J. Ketonen : A Decision Procedure Revisited: Notes on Direct Logic, Linear Logic and its Implementation, forthcoming in Theoretical Computer Science. W. Bibel : On Matrices with Connections, Journal ACM, October 1981, vol. 28, 4, pp. 633-645. C. T. Brown : Relating Petri Nets to Formulae of Linear Logic, Technical Report ECS LFCS 89-87, Univ. of Edinburgh, June 1989. V. Danos and L. Regnier : The structure of Multiplicatives, Archive for Mathematical Logic, 26, pp.181-203, 1989. S. Feferman : Inductively Presented Systems and the Formalization of Meta Mathematics, in Logic Colloquium ’80 (van Dalen and others eds.), North Holland, pp. 95-128. R. O. Gandy, : Proof of Strong Normalization, in “To H.B.Curry: Essays on Combinatory Logic, Lambda calculus and Formalism”, Hindley and Seldin eds., Academic Press, 1980. J. Y. Girard : linear logic and Parallelism, proceeding of the School on semantics of parallelism, held at IAC, CNR, Roma, september 1986. J. Y. Girard : Linear Logic, Theoretical Computer Science, 50 (1987), pp. 1-102. J. Y. Girard : Quantifiers in Linear Logic, Proceedings of the SILFS conference held in Cesena, January 1987. J. Y. Girard : Towards a Geometry of Interaction, in “Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference held June 14-20, 1987 in Boulder, Colorado, J. W. Gray and A. Scedrov editors, Contemporary Mathematics 92, American Mathematical Society, 1989.

J. Y. Girard : Quantifiers in linear logic II, Preprint, Équipe de Logique. Université Paris VII. Tour 45-55.5^{eme} étage. 2, Place Jussieu. 75251 Paris, France. V. Gehlot and C. A. Gunter : Normal process representatives, in Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990. J. Ketonen and R. Weyhrauch : A decidable fragment of predicate calculus, Theoretical Computer Science 32 (1984) 297-307. N. Marti-Oliet and J. Meseguer : From Petri Nets to Linear Logic. in Springer LNCS 389, ed. by D.H.Pitt et al., 1989, pp.313-340. G. Pottinger : Normalization as Homomorphic Image of Cut-Elimination, Annals of Mathematical Logic, 12, 1977, pp. 323-357. D. Prawitz : Natural deduction. A proof-theoretic stydy, Almquist and Wiksell, Stockholm, 1965. D. Prawitz : A Proof Procedure with Matrix Reduction, Lecture Notes in Mathematics 125, Springer, Berlin, 1970, pp. 207-213. D. Prawitz : Ideas and Results in Proof Theory, in Proceedings of the Second Scandinavian Logic Symposium, ed. Fenstad, North-Holland, 1971. U. Solitro : La logica lineare come sistema di tipi per un calcolo non funzionale, Tesi di Dottorato, 1990, Dipartimento di Scienze dell’Informazione, via Moretto da Brescia, I-20133 Milano. A. Ungar : Normalization and Cut-Elimination in First-Order Logic, PhD Thesis, Department of Philosophy, Stanford 1986. L. A. Wallen : Automated Deduction in Nonclassical Logics, MIT Press, 1989. J. I. Zucker : The Correspondence between Cit-Elimination and Normalization, Annals of Mathematical Logic, 7, 1974, pp. 1-56.