To appear in Theoretical Computer Science

Experiments in Linear Natural Deduction

Simone Martini^{∗} Andrea Masini ^{†}

February 1, 1996

Abstract

We investigate several fragments of multiplicative linear logic, in a natural deduction setting and with the aim of a better understanding of the par connective. We study, first, a pre-tensorial calculus, which is strengthened then in the standard tensorial fragment. The addition of a further pre-tensorial connective yields (a natural deduction version of) Full Intuitionistic Linear Logic. A further strengthening of the rules leads to the full classical multiplicative logic. Some proof-theoretical properties of the systems are investigated.

1. Introduction

This study emerges as an attempt to better understand the “par” connective of linear logic, in its logical and computational content, from a computer science perspective. In the context of functional programming, the Curry-Howard isomorphism—relating natural deduction intuitionistic proofs and their normalization process to programs and their execution—is a leading idea. Proofs are effective transformations of several inputs (assumptions) into one output (conclusion), as it is apparent from the correspondence between implication and function space, and from the categorical interpretation of the intuitionistic natural deduction.

In this perspective there is no real problem with linear logic (e.g. [Gir95, Tro95, BBdPH93]) but for par, which has not received any attention from a natural deduction (i.e. input-output) perspective. The reason seems to stay in the apparent impossibility to formulate a suitable introduction–elimination pair, when sticking to single conclusion systems. The problem obviously does not arise either in sequent calculus or in proof-nets, which are intrinsically multi-conclusion calculi. Note, moreover, that even in an intuitionistic setting (traditionally single-conclusion), the Full Intuitionistic Linear Logic (FILL) of [dPH93], which is an input-output interpretation, is formulated as a multi-conclusion sequent calculus.

Semantically speaking, a par is a monoidal tensor. Thus, our strategy of investigation has been to isolate a simple ambience (the pure implicative fragment) and to enrich it stepwise, starting from the weakest possible connective (i.e. a covariant bifunctor; Section 2.). The strengthening of this connective into an intuitionistic par allowed interesting reflections on the logical power of this “intuitionistic” system (Section 3.). Indeed, from the simple formulation of the calculus and the logical equivalence with FILL, we see that this intuitionistic par is a restricted tensor (Section 3.2.), leaving still open the problem of finding a convincing intuitionistic interpretation for par. It is not too surprising that in the classical case the par is amenable to a better treatment (Sections 4. and 5.), resulting in a natural deduction system enjoying both proof-theoretical (explicit introduction-elimination rules for par) and computational (normalization) good properties.

∗Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze, 206, I-33100 Udine, Italy. E-mail:martini@dimi.uniud.it. Partially supported by EC HCM Project CHRX-CT93-0046 Lambda Calcul Typé and CNR-GNSAGA.

†Dipartimento di Informatica, Università di Pisa, Corso Italia, 40, I-56125 Pisa, Italy. Email:masini@di.unipi.it. Partially supported by a grant of MURST 40%, “Modelli della Computazione e dei Linguaggi di Programmazione” and ESPRIT BRA 8130 LOMAPS.

2. Pre-tensorial Linear Logic

All the systems we study in this paper are built on top of the implicational fragment of linear logic, formulated in natural deduction style according to the following definition.

Definition 2.1. The pure implicative natural deduction system of linear logic (N-ill) is given by the following axioms and rules:

A

[B] ; \begin{matrix}· \\ · \\ · \end{matrix} ; A ; ⊸ I ; B ⊸ A  B B ⊸ A ; ⊸ E ; A

Here, and in the following, [B] means that exactly one occurrence of the formula B is discharged; as usual, other assumptions may be present. We write Γ ⊢ A, where Γ is a multiset of formulas, if there is a deduction of A whose open assumptions (each corresponding to a leaf) are exactly the formulas of Γ.

Additional systems will be obtained adding to N-ill connectives and rules. We will use the notation LL_{list-of-rules}^{list-of-connectives} to denote the natural linear deduction system obtained by adding to N-ill the new connectives in the “list-of-connectives” equipped with the rules in the “listof-rules”.

We study, first, the simple system obtained by adding a binary connective •, with, as only rule, the following replacement rule (•R):

A • B  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C  [B] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D
•R
C • D

A • B is the “major premise” of the rule, while C and D are its “minor premises”.

We call the resulting system, LL_{•R}^{•}, pre-tensorial linear logic (or PtLL). It is a very simple system, with good proof-theoretical properties (see Section 2.1.), but very limited on the logical side. Indeed, from a categorical point of view, • is simply a bi-functor, without any “intrinsic” property. In particular:

Proposition 2.2. The • is not commutative and is not associative.

And, moreover, its rule is too weak to characterize completely the connective:

Proposition 2.3. Let ∘ be another connective with the same rule of •. Then

LL_{∘R,•R}^{∘,•} ⊬ A ∘ B ⊸ A • B

It is a situation common to all “intensional” connectives, like the modalities, when their proof theory is formulated in the standard way.

2.1. Reductions and properties

We may equip system PtLL with a reduction relation on proofs, adding to the usual β reductions for ⊸ the following • reduction.

\begin{matrix}{A • B  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C  [B] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D \atop C • D} & [C] ; \begin{matrix}· \\ · \\ · \end{matrix} ; E & [D] ; \begin{matrix}· \\ · \\ · \end{matrix} ; F \\ E • F \end{matrix}  ▷  {A • B  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; (C) ; \begin{matrix}· \\ · \\ · \end{matrix} ; E  [B] ; \begin{matrix}· \\ · \\ · \end{matrix} ; (D) ; \begin{matrix}· \\ · \\ · \end{matrix} ; F \atop E • F}

It is no surprise that under the reduction relation defined by this rule, PtLL enjoys good properties.

Theorem 2.4. PtLL is strongly normalizing.

Proof. Define the size s(π) of a deduction π whose last rule has premise π_{1} (respecively, premises π_{1}, π_{2}, π_{3}) as s(π_{1}) + 1 (s(π_{1}) + s(π_{2}) + s(π_{3}) + 1). Due to the linearity of the calculus, the size of the deduction strictly decreases in any reduction step.

Q.E.D.

In spite of the impurity of rule •R (its premises behave as in an elimination rule, while its conclusion behaves as in an introduction rule), PtLL enjoys also the subformula principle. We are not interested in the study of the subformula principle “per se”, but it is interesting in order to have a full understanding of the •R rule. The usual notion of track has to be extended, in order to handle the non-standard behavior of rule •R.

Definition 2.5. A track of a derivation is a sequence of formulas A_{0}, …, A_{n} such that:

(i) A_{0} is an assumption not discharged by an application of •R;

(ii) A_{i}, for i < n, is not the minor premise of ⊸ E and either:

1. A_{i} is not the major premise of •R and A_{i+1} is directly below A_{i};

2. A_{i} is the major premise of •R and A_{i+1} is an assumption discharged at that rule; (iii) A_{n} is either the minor premise of a ⊸ E, or the conclusion of the deduction.

In the following theorem, whose proof is routine ([Pra65]), note the double role played by the •R rule: its major premise belongs to the E-part, while its minor premises belong to the I-part (or is the minimum formula).

Theorem 2.6. Let D be a normal derivation and let π = A_{0}, …, A_{n} be a track in D. Then there is a formula A_{i} which separates two (possibly empty) parts of π (called the E-part and the I-part) such that:

i for each A_{j} of the E-part: j < i, A_{j} is the major premise of an elimination rule or of •R, and A_{j+1} is a subformula of A_{j};

ii A_{i}, for i ≠ n, is a premise of an introduction rule, or a minor premise of a •R rule;

iii for each A_{j} of the I-part: i < j, A_{j} is either a premise of an introduction rule, or a minor premise of a •R rule, and A_{j} is a subformula of A_{j+1}.

Proof. Suppose false the thesis; then the proof is not normal. Argue by cases. A_{j} cannot be the premise of an introduction rule and A_{j+1} the major premise of an elimination, for normality; A_{j} cannot be the premise of an introduction rule and A_{j+1} the major premise of •R, for the main connective of A_{j+1} is not •; A_{j} cannot be the minor premise of •R and A_{j+1} the major premise of an elimination, for the main connective of A_{j+1} is not ⊸; A_{j} cannot be the minor premise of •R and A_{j+1} the major premise of •R, for normality.

Q.E.D.

Theorem 2.7. LL_{•R}^{•} enjoys the subformula principle.

Proof. By induction on the order of a track (a track is of order 0 iff its last formula is the conclusion of the deduction, and is of order p + 1 if its conclusion is the minor premise of a ⊸ elimination), show that any formula appearing in a track is subformula of the conclusion or of one undischarged hypothesis.

Q.E.D.

2.2. Toward tensorial linear logic

Theorem 2.6 suggests a way to strengthen PtLL, separating in two different rules the introduction and the elimination behavior of •R. Since a minor premise belongs to the I-part and is followed in a track by the conclusion of the rule, a suitable introduction rule is obtained simply, by taking as its premises the minor premises of •R and as conclusion the conclusion of the •R, namely:

\begin{aligned}\begin{matrix}· \\ · \\ · \end{matrix} ; C & & \begin{matrix}· \\ · \\ · \end{matrix} ; D \\ & & & •I \\ & C • D \end{aligned}

Analogously, since the major premise of •R belongs to the E-part and is followed in a track by one of the discharged assumptions, we may obtain an elimination rule by taking as its major premise the major premise of •R, as discharged hypotheses the discharged hypotheses of •R, and as conclusion a “new” formula:

A • B  [A][B] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C
•E
C

Now, in these two rules we immediately recognise those for the linear connective ⊗. The logic LL_{•I,•E}^{•} coincides therefore with the tensorial fragment of LL, without the constant 1. We will then use ⊗ for the connective • equipped with these two rules. It is obvious that the rule •R is derived in LL_{•I,•E}^{•}.

3. Linear Intuitionism?

3.1. Good news

Having obtained the tensorial logic LL_{⊗I,⊗E}^{⊗}, we may now exploit the observation we made on the intensionality of a connective defined by the only rule •R and look what happens to the tensorial logic based on ⊗ when we add a further (pre-)tensor connective •. We are thus interested in the system LL_{⊗I,⊗E,•R}^{⊗,•}. The two connectives interact in a nice form, since

LL_{⊗I,⊗E,•R}^{⊗,•} ⊢ B ⊗ (A • D) ⊸ (B ⊗ A) • D

This important weak distributivity property is at the heart of the interpretation of linear logic into categories. Cockett and Seely [CS92] show how it is necessary in order to model the cut rule in classical linear logic; DePaiva and Hyland [dPH93] build over it an interesting system for an intuitionistic fragment of linear logic. Standard formulations of intuitionistic linear logic (e.g. [GL87]) stem from the usual syntactic restriction (at most one formula to the right) of the two-sided sequent formulation of the classical version. Since the right rule for par does not make sense under this restriction, par has been banned from the intuitionistic fragment. Starting from the semantic intuition of a category with two monoidal operations connected by weak distributivity, DePaiva and Hyland realized that an (intuitionistic) system with par was possible, in a multi-conclusion setting and (for ensuring cut-elimination) with term annotations. They prove the calculus (FILL: Full Intuitionistic Linear Logic) complete with respect to full multiplicative categories (i.e. symmetric monoidal closed categories which are weakly distributive), which are the “natural” models of FILL. What are, then, the relations between FILL and our LL_{⊗I,⊗E,•R}^{⊗,•}, with • playing the role of intuitionistic par? To answer the question, let us first add to our system rules for the constants 1 and ⊥, plus rules for commutativity and associativity of •. As usual, we will write A^{⊥} for A ⊸ ⊥. The simplest rules for the constants are the naive ones:

A ; ⊥I ; A • ⊥  A • ⊥ ; ⊥E ; A

\begin{aligned}& 1I \\ 1 \end{aligned}  A 1 ; 1E ; A

Commutativity and associativity are simply obtained by^{1}

\begin{matrix}· \\ · \\ · \end{matrix} ; B • C ; \overline{comm} ; C • B

\begin{matrix}· \\ · \\ · \end{matrix} ; A • (B • C) ; a1 ; (A • B) • C  \begin{matrix}· \\ · \\ · \end{matrix} ; (A • B) • C ; a2 ; A • (B • C)

Let N-FILL (= LL_{⊗I,⊗E,•R,comm,a1,a2,⊥I,⊥E,1I,1E}^{⊗,•,1,⊥}) be the resulting system.

Theorem 3.1. Γ ⊢_{N−F ILL} A iff Γ ⊢_{F ILL} A.

Proof. (⇒) Easy, since all the rules of N-FILL are clearly valid in FILL. (⇐) For a syntactic proof of this fact one needs first to decorate N-FILL proofs with terms and, then, to prove that each FILL term can be permuted in a suitable way to obtain an N-FILL term. The crucial point of this process is the treatment of the restriction on the right rule for ⊸. This syntactic proof, however, is long and tedious. We sketch, instead, an economical semantical proof. Note, first, that N-FILL contains all the ingredients to build a full multiplicative category, say NF. In order NF to be such a category, of course, one needs to add suitable quotients of arrows, for unicity and coherence, but these will not identify objects. Since FILL is complete for weakly distributive categories, any proof Γ ⊢_{F ILL} A corresponds to an arrow in NF, that is to a (quotient of proofs) Γ ⊢_{N−F ILL} A.

Q.E.D.

3.2. Bad news

Unfortunately, as far as provability is concerned, N-FILL is not big improvement over pure tensorial logic. Define the following “collapsing” map ()^{∗}:

\begin{aligned}(⊥)^{∗} & = & 1 \\ (A • B)^{∗} & = & (A)^{∗} ⊗ (B)^{∗} \\ (A ⊗ B)^{∗} & = & (A)^{∗} ⊗ (B)^{∗} \\ (A ⊸ B)^{∗} & = & (A)^{∗} ⊸ (B)^{∗} \end{aligned}

Theorem 3.2. If π is a proof of Γ ⊢_{N−F ILL} A, then we can construct a proof π^{∗} of (Γ)^{∗} ⊢_{N−F ILL} (A)^{∗}.

Proof. Easy induction on the lenght of π and by cases on its last rule. The only “interesting” cases are those involving the • connective: we will show only the one in which the last rule is •, as it shows how the bifunctorial rules must be replaced by a pair of ⊗I − ⊗E rules:

Γ ; \begin{matrix}· \\ · \\ · \end{matrix} π_{1} ; A • B  [A], Δ ; \begin{matrix}· \\ · \\ · \end{matrix} π_{2} ; C  [B], Σ ; \begin{matrix}· \\ · \\ · \end{matrix} π_{3} ; D
•
C • D

1Proof theoretical purist: wait...!

Figure 1: Logical laws of “and”-“or”,“tensor”-“par”

By induction hypothesis and by using the ⊗I and ⊗E rules we have:

(Γ)^{∗} ; \begin{matrix}· \\ · \\ · \end{matrix} π_{1}^{∗} ; (A)^{∗} ⊗ (B)^{∗}  \begin{aligned}[(A)^{∗}], (Δ)^{∗} ; \begin{matrix}· \\ · \\ · \end{matrix} π_{2}^{∗} ; (C)^{∗} & [(B)^{∗}], (Σ)^{∗} ; \begin{matrix}· \\ · \\ · \end{matrix} π_{3}^{∗} ; (D)^{∗} \\ & ⊗I \\ (C)^{∗} ⊗ (D)^{∗} \end{aligned}
⊗E
(C)^{∗} ⊗ (D)^{∗}

Q.E.D.

The opposite implication obviously does not hold. For F = ((A•B) ⊸ C) ⊸ (A ⊸ (B ⊸ C)), ⊢ (F)^{∗}, but it is easy to show, in view of the the cut-elimination theorem for FILL, that ⊬ F.

The logical laws on ⊸, •, ⊥ are thus a subset (modulo renaming) of the laws on ⊸, ⊗, 1, a situation hardly satisfactory. Consider, indeed, what happens for the (non linear) connectives “and”, “or”. When we go from their classical formulation to the intuitionistic one, we preserve a clean-cut separation between them—they still have a common set of logical laws, but none of them is a subset of the other. In the linear case, instead, Theorem 3.2 tells us that the intuitionistic par is a restricted version of the tensor ⊗.

The moral we draw from this section is that, despite the deep semantical motivation and the proof-theoretical interest of a system like FILL (whose cut-elimination depends in an essential way from the term annotations), it is difficult to call intuitionistic a connective that is only a restricted tensor. The only fact that in this fragment A℘A^{⊥} it is not provable, seems too a limited reason. Due to the intensionality of its par, its status is somehow similar to that of many temporal logics, where different logics are characterized by connectives with increasing power.

4. Toward Classical Linear Logic

If the natural deduction formulation shows that intuitionistic par is debatable, can we gain something passing to classical par? Let us look at ways to extend the pre-tensorial rule

A℘B  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C  [B] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D
℘R
C℘D

in order to have a classical ℘. Since in MLL one can prove A℘A^{⊥} (where, with a little abuse of language, in the case of A = 1, A^{⊥} may denote not only 1 ⊸ ⊥, but also ⊥), let us start adding to LL_{℘R,⊗I,⊗E,1I,1E}^{℘,⊗,1} the axiom

\begin{aligned}& ℘-ax \\ A℘A^{⊥} \end{aligned}

From this and rule ℘R, we obtain the figure

\begin{aligned}& ℘-ax \\ A℘A^{⊥} \end{aligned}  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C  [A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D
℘
C℘D

which can be formulated as introduction rule:

[A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C  [A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D
℘I
C℘D

This (and its symmetric) is the “official” introduction rule for ℘, which trivially allows the proof of A℘A^{⊥}. Let us start again this euristic game. In MLL, ⊥ is the identity of ℘. In particular, we need a way of obtaining a proof of B, given a proof of B℘⊥ ^{2}. Assume then given the rule

{⊥℘B \atop B}

and combine it with ℘R to form the figure:

A℘B  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥  [B] ; {⊥℘B \atop B}

[1] B ; \overline{1E} ; B [⊥]

2The reverse deduction is easily proved by

℘I B℘⊥

Once again, this inference can be formulated as an elimination rule:

A℘B  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥
℘E
B

This (and its symmetric) is the “official” elimination rule for ℘. Observe it is not independent from the others connectives: its premises contain, besides ℘, also ⊥.

5. Classical MLL

After the discussion of the last section, let N-mll be the system obtained by adding to LL_{⊗I,⊗E,1I,1E}^{⊗,1} the following rules:

• Introduction rules:

\begin{aligned}[A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C & & [A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D \\ & & ℘I^{1} \\ & C℘D \end{aligned}  \begin{aligned}[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C & & [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D \\ & & & ℘I^{2} \\ & C℘D \end{aligned}

where in the case of A = 1, A^{⊥} may be either 1 ⊸ ⊥ or ⊥.

• Elimination rules:

A℘B  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥ ; ℘E^{1} ; B  B℘A  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥ ; ℘E^{1} ; B

Proposition 5.1. The ℘R pre-tensorial rule is derivable in N-mll.

Proof.

[C]  A℘B  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C  [C^{⊥}] ; ⊸ E ; ⊥ ; ℘E ; B ; \begin{matrix}· \\ · \\ · \end{matrix} ; D
℘I
C℘D

Q.E.D.

The following proposition shows how the splitting of the pre-tensorial rule allows to recover commutativity and associativity.

Proposition 5.2. The ℘ connective of N-mll is commutative and associative.

Proof.

{{[A]  \begin{matrix}{A℘(B℘C) {[A] [A^{⊥}] \atop ⊥} \atop B℘C} & {[C] [C^{⊥}] \atop ⊥} \\ B \end{matrix} \atop A℘B}  [C] \atop (A℘B)℘C}

Q.E.D.

Theorem 5.3.

Γ ⊢_{N−mll} A ⇔ Γ ⊢_{MLL} A

Proof. (⇒) All the N-MLL rules are sound in MLL. (⇐) From Theorem 3.1 and the discussion of the previous section, if Γ ⊢_{F ILL} A, then Γ ⊢_{N−mll} A. On the other hand, it is an easy exercise to show that FILL + A℘A^{⊥} = MLL. Since ⊢_{N−mll} A℘A^{⊥}, we conclude.

Q.E.D.

5.1. On the ℘ introduction rule

One of the novelties of our approach is the ℘ introduction rule which, in the discharging of a “negated” formula, bears similarities with reductio ad absurdum rule (RAA) of classical logic. It is easy to see how RAA is “implemented” in N-mll:

{{[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥ [A] \atop ⊥℘A} [⊥] \atop A}

Note RAA is obtained with a restricted instance of ℘I, where the “non negated” discharged formula is an assumption. In fact, such a restriction preserves the logical power of N-mll.

Proposition 5.4. There is an effective transformation of a N-mll proof π in another N-mll proof π′, s.t. in π′ each occurrence of the rule ℘I is bound to the following “formats”:

{[A] [A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B \atop A℘B}  {[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B [A] \atop A℘B}

Proof. (sketch) Replace each occurrence

\begin{aligned}[A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C & & [A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D \\ & C℘D \end{aligned}

of ℘I in π, with the figure

{{{[A] {[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; D [D^{⊥}] \atop ⊥} \atop A℘⊥} [⊥] \atop A} ; \begin{matrix}· \\ · \\ · \end{matrix} ; C [D] \atop C℘D}

Q.E.D.

Hence, from the point of view of the pure provability power, the ℘I rules may be replaced with the new rules

[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B ; A℘B  [A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B ; B℘A

which correspond to the definition of ⊸ in terms of ℘.

6. Reductions

Before defining the N-mll reduction, we introduce a new proof figure that we call “absorption”.

\begin{matrix}[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥ & & [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C \\ & & & ℘I^{1} \\ & ⊥℘C \end{matrix} [⊥]

℘E^{1}
C

Such a figure cannot be reduced in N-mll. This is consistent with the linearity of the calculus, in particular with the constraint that all the open hypotheses of a deduction be “concrete” leaves of the proof tree. This form of implicit weakening (the other undischarged assumptions of the deduction of ⊥ from A^{⊥} are present, though not necessary for the derivation of C) is coessential to a formalization of linear proofs as proof trees.

We will write an absorption as

[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥  [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C
A
C

Remark We have in fact four absorption figures, one for each combination of ℘I^{1}, ℘I^{2} with ℘E^{1}, ℘E^{2}.

6.1. β reductions

We have the usual β redexes originated by ⊸, ⊗, 1 plus the new ℘ redexes. A ℘ redex is a sequence ℘I − ℘E that does not belong to an absorption figure. We have four kind of redexes, one for each combination of ℘I^{1}, ℘I^{2} with ℘E^{1}, ℘E^{2}; we will give a specific case, the other are analogous.

\begin{aligned}\begin{aligned}[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B & & [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C \\ & & & ℘I^{2} \\ & B℘C \end{aligned} & [B] ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥ \\ & & ℘E^{1} \\ C \end{aligned}  ▷  \begin{aligned}[A^{⊥}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B ; \begin{matrix}· \\ · \\ · \end{matrix} ; ⊥ & & [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C \\ & & & A \\ & C \end{aligned}

B℘C is the principal formula of the redex.

6.2. Commutative reductions

The usual commutative contractions for ⊗ and 1, formed by a ⊗E (1E) followed by an elimination rule.

6.3. Normalization

Let us denote with → the compatible closure of ▷, and with ↠ the transitive and reflexive closure of →. The “degree” of a redex is the usual structural complexity of its principal formula. It is immediate to prove that:

Proposition 6.1. The contractions previously defined are correct in N-mll.

Now we can formulate the normalization theorem:

Theorem 6.2. The reduction relation ↠ is normalizing.

Proof. Completely standard (see [TvD88]). We outline here the main idea. Define the degree, d(D), of a deduction D as the maximum of the degrees of the redexes in D. Set now μ(D) = (d(D), m), where m is the sum of the lenghts of redexes of degree d(D). By induction on μ(D) (under the lexicographic ordering) we prove that, selected a redex of maximal degree in D, we can reduce μ(D).

Q.E.D.

7. Conclusions

We have proposed some new natural deduction systems for various versions of the par connective. These systems show that, contrary to most folklore, the classical natural deduction methods can indeed cope with par.

Besides this genuine proof-theoretical interest, we are persuaded that a deeper insight into a system can be gained only by looking at it from many different perspectives, each revealing properties that others hide. A good example of this situation is the relation bewteen optimal lambda-reduction and linear logic, which becomes apparent only in the proof-net formulation and can be only reconstucted a posteriori in the sequent calculus approach.

Without being too optimistic, we believe the proposed systems may point out new computational interpretation, with a particular emphasis on concurrency. The shape of the classical introduction rule, in fact, may be seen as the definition of a concurrent composition operator with a syncronous communication (represented by the symultaneous discharging of the two dual premises).

References

[BBdPH93] N. Benton, G. Bierman, V. de Paiva, and J.M.E. Hyland. Linear λ-calculus and categorical models revisited. In E. Börger et al., editors, Computer Science Logic 1992, volume 702 of Lectures Notes in Computer Science, pages 61–84. Springer-Verlag, 1993. San Miniato, September 1992.

[CS92] Robin Cockett and Robert Seely. Weakly distributive categories. In Conference on Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 47–69. AMS, June 1992.

[dPH93] Valeria de Paiva and Martin Hyland. Full intuitionistic linear logic. Annals of Pure and Applied Logic, 64:273–291, 1993. (Extended Abstract).

[Gir95] Jean-Yves Girard. Linear logic, syntax and semantics. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Note Series, pages 1–42. Cambridge University Press, 1995.

[GL87] Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In TAP-SOFT ’87, Volume 2, number 250 in Lecture Notes in Computer Science, pages 52–66. Springer-Verlag, 1987.

[Pra65] Dag Prawitz. Natural Deduction. Acta Universitatis Stockholmiensis, Stockholm Studies in Philosophy 3. Almqvist & Wiksell, Stockholm, 1965.

[Tro95] Anne S. Troelstra. Natural deduction for intuitionistic linear logic. Annals of Pure and Applied Logic, 73:79–108, 1995.

[TvD88] Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics, volume II. North-Holland, 1988.