Intersection Logic in sequent calculus style
Simona Ronchi Della Rocca

Alexis Saurin

Dipartimento di Informatica
Universita di Torino
IT-10149 Torino, Italy
ronchi@di.unito.it

Laboratoire CNRS PPS & INRIA pi.r2
Paris, France
alexis.saurin@pps.jussieu.fr

Yiorgos Stavrinos

Anastasia Veneti

Graduate Program in Logic and Algorithms (MPLA)
Department of Mathematics
University of Athens
GR-15784 Zografou, Greece
g.stavrinos@math.ntua.gr
tassiana98@gmail.com

1

Introduction

The intersection type assignment system IT (shown in Figure 1) is a deductive system that assigns formulae (built from the intuitionistic implication → and the intersection ∩) as types to the untyped λ -calculus.
It has been defined by Coppo and Dezani [6], in order to increase the typability power of the simple type
assignment system. In fact, IT has a strong typability power, since it gives types to all the strongly
normalizing terms [17, 11]. Intersection types, supported by a universal type and a suitable pre-order
relation, has been used for describing the λ -calculus semantics in different domains (e.g. Scott domains
[3, 7], coherence spaces [14]), allowing to characterize interesting semantical notions like solvability and
normalizability, both in call-by-name and call-by-value settings [18].
Differently from other well known type assignments for λ -calculus, like for example the simple or
the second order one, IT has not been designed as decoration of a logical system, following the so called
Curry-Howard isomorphism, relating in particular types with logical formulae. In fact, despite to the fact
that it looks like a decoration of the implicative and additive fragment of the intuitionistic logic, this is
not true. Indeed, while the connective → has the same behaviour of the intuitionistic implication, the
intersection ∩ does not correspond to the intuitionistic conjunction, as Hindley pointed out in [10], since
the rule introducing it has the meta-theoretical condition that the two proofs of the premises be decorated
by the same term, and this constraint is no more explicit when terms are erased.
It is natural to ask if there is a logic with a natural correspondence with intersection types. Some
attempts have been made, which will be briefly recalled in Section 7. Our work follow the line started
from [19] and [15, 16], where the authors defined Intersection Logic IL and Intersection Synchronous
Logic ISL, respectively. ISL is a deductive system in natural deduction style proving molecules which
are finite multisets of atoms which, in turn, are pairs of a context and a formula. The notion of molecule
allows to distinguish between two sets of connectives, global and local, depending on whether they
are introduced and eliminated in parallel on all atoms of a molecule or not. Note that global and local
connectives are called asynchronous and synchronous, respectively, in [15, 16]. In particular, two kinds
of conjunction are present: the global one corresponding to intuitionistic conjunction and the local one
corresponding to intersection. Then, the intersection type assignment system is obtained by decorating
ISL with λ -terms in the Curry-Howard style. Roughly speaking, a molecule can be mapped into a set of
E. Pimentel, B. Venneri and J. Wells (Eds.): Workshop on
Intersection Types and Related Systems 2010 (ITRS 2010).
EPTCS 45, 2011, pp. 16–30, doi:10.4204/EPTCS.45.2

c S. Ronchi Della Rocca, A. Saurin, et al.

S. Ronchi Della Rocca, A. Saurin, et al.

17

Γ, x : σ ⊢IT x : σ

(A)

Γ ⊢IT M : σ Γ ⊢IT M : τ
(∩I)
Γ ⊢IT M : σ ∩ τ

Γ ⊢IT M : σL ∩ σR
(∩Ek )k = L, R
Γ ⊢IT M : σk

Γ, x : σ ⊢IT M : τ
(→ I)
Γ ⊢IT λ x.M : σ → τ

Γ ⊢IT M : σ → τ Γ ⊢IT N : τ
(→ E)
Γ ⊢IT MN : τ

Figure 1: The intersection type assignment system IT.
intuitionistic proofs which are isomorphic, in the sense that some rules are applied in parallel to all the
elements in the set. The isomorphism is obtained by collapsing the two conjunctions.
ISL put into evidence the fact that the usual intuitionistic conjunction can be splitted into two different connectives, with a different behaviour, and the intersection corresponds to one of it. So we think that
ISL is a logic that can be interesting in itself, and so we would like to explore it from a proof-theoretical
point of view. To this aim, we present here a sequent calculus formulation of it, that we call ISC, and
we prove that it enjoys the property of cut elimination. The proof is not trivial, since the play between
global and local connectives is complicated and new structural rules are needed.
Stavrinos and Veneti [21, 23] further enhanced IL and ISL with a new connective: the logical counterpart of the union operator on types [2]. It turns out that union is a different kind of disjunction. In
the extensions of IL and ISL presented in [21], though, the status of union is not so clear; in particular,
union is not an explicitly local version of intuitionistic disjunction, since its elimination rule involves
a global side-effect. So, the pair union-disjunction does not enjoy the nice characterization of the pair
intersection-conjunction, which are the local and global versions, respectively, of the same connective.
Moving to a sequent calculus exposition [23] allows for a very nice and symmetric presentation of both
intersection and union, which are now the local versions of intuitionistic conjunction and disjunction,
respectively. Our next step will be to do a proof theoretical investigation of this new calculus.
The paper is organized as follows. In Section 2 the system ISL is recalled, and its sequent calculus
version ISC is presented. In Section 3 the relation between ISC and Intuitionistic Sequent Calculus LJ
is shown. Section 4 contains a brief survey of the cut-elimination procedure in LJ. In Section 5 the cut
elimination steps of ISC are defined, and in Section 6 the cut-elimination algorithm is given. Moreover
Section 7 contains a brief survey of the other approaches to the problem of a logical foundation of
intersection types.

2

The system ISC

In this section the system ISL presented in [15, 16] is recalled. Moreover, an equivalent sequent calculus
version is given.
Definition 2.1 (ISL)

i) Formulas are generated by the grammar

σ ::= a | σ → σ | σ &σ | σ ∩ σ
where a belongs to a countable set of propositional variables. Formulas are ranged over by small
greek letters.

Intersection Logic in sequent calculus style

18

[(σi ; σi ) | i ∈ I]

(Ax)

[(Γi1 , τi , σi , Γi2 ; ρi ) | i ∈ I]

[(Γi ; τi ) | i ∈ I]
(W)
[(Γi , σi ; τi ) | i ∈ I]
[(Γi , σi ; τi ) | i ∈ I]
(→I)
[(Γi ; σi → τi ) | i ∈ I]

[(Γi1 , σi , τi , Γi2 ; ρi ) | i ∈ I]

(X)

[(Γi ; σi → τi ) | i ∈ I] [(Γi ; σi ) | i ∈ I]
(→E)
[(Γi ; τi ) | i ∈ I]

[(Γi ; σi ) | i ∈ I] [(Γi ; τi ) | i ∈ I]
(&I)
[(Γi ; σi &τi ) | i ∈ I]
M ∪ [(Γ; σ ), (Γ; τ )]
(∩I)
M ∪ [(Γ; σ ∩ τ )]

M ∪ N (P)
M

[(Γi ; σiL &σiR ) | i ∈ I]
[(Γi ; σik ) | i ∈ I]

(&Ek ), k = L, R

M ∪ [(Γ; σL ∩ σR )]
(∩Ek ), k = L, R
M ∪ [(Γ; σk )]

Figure 2: The system ISL
ii) Contexts are finite sequences of formulas, ranged over by Γ, ∆, E, Z. The cardinality |Γ| of a
context Γ is the number of formulas in Γ.
iii) Atoms (Γ; σ ) are pairs of a context and a formula, ranged over by A , B.
iv) Molecules [(α1i , . . . αmi ; αi ) | 1 6 i 6 n] or [(α1i , . . . αmi ; αi ) | i ∈ I] or [(α1i , . . . αmi ; αi )]i are finite
multisets of atoms such that all atoms have the same context cardinality. Molecules are ranged
over by M , N .
v) ISL is a logical system proving molecules in natural deduction style. Its rules are displayed in
Figure 2. We write ⊢ISL M when there is a deduction proving the molecule M , and π : M when
we want to denote a particular derivation π proving M .
Some comments are in order. Rule (P) is derivable and it is useful for the normalization procedure.
The connectives →, & are global, in the sense that they are both introduced and eliminated in all the atoms
of a molecule by a unique rule, while the connective ∩ is local, since it is introduced and eliminated in
just one atom of a molecule.
The following theorem recall the correspondence between ISL and IT, proved in [16]. In the text of
the theorem, we use the notation (Γ)s for denoting a decoration of the context Γ through a sequence s
of different variables. More precisely, if Γ = α1 , ..., αn and s = x1 , ..., xn , (Γ)s is the set of assignments
{x1 : α1 , ..., xn : αn }.
Theorem 2.2 (ISL and IT)
i) Let ⊢ISL [(Γ1 ; α1 ), . . . , (Γm ; αm )], where αi and all formulae in Γi do
not contain the connective &. Then for every s, there is M such that (Γi )s ⊢IT M : αi .
ii) If (Γi )x1 ,...,xn ⊢IT M : αi (i ∈ I), then ⊢ISL [(Γi ; αi ) | i ∈ I].
Now we will define an equivalent formulation in sequent calculus style.
Definition 2.3 ISC is a logical system proving molecules in sequent calculus style. Its rules are displayed in Figure 3. We write ⊢ISC M when there is a derivation proving molecule M and π : M when
we want to denote a particular derivation π proving M .
Notice that the connectives →, & are dealt with rules having a multiplicative behaviour of contexts,
but the structural rules ensure an equivalent additive presentation. The connective ∩, though, need to

S. Ronchi Della Rocca, A. Saurin, et al.

19

Identity Rules: both global

[(αi ; αi )|i ∈ I]

(Ax)

[(Γi ; αi )|i ∈ I] [(∆i , αi ; βi )|i ∈ I]
(cut)
[(Γi , ∆i ; βi )|i ∈ I]

Structural Rules: (W), (X), (C) are global and (Fus), (P) are local
[(Γi ; βi )|i ∈ I]
(W)
[(Γi , αi ; βi )|i ∈ I]

[(Γi , βi , αi , ∆i ; γi )|i ∈ I]
(X)
[(Γi , αi , βi , ∆i ; γi )|i ∈ I]

[(Γ; β )] ∪ M
(Fus)
[(Γ; β ), (Γ; β )] ∪ M

[(Γi , αi , αi ; βi )|i ∈ I]
(C)
[(Γi , αi ; βi )|i ∈ I]

M ∪ N (P)
M

Logical Rules: →, & are global and ∩ is local
[(Γi ; αi )|i ∈ I] [(∆i , βi ; γi )|i ∈ I]
(→L)
[(Γi , ∆i , αi → βi ; γi )|i ∈ I]
[(Γi , αiL , αiR ; βi )|i ∈ I]
[(Γi , αiL &αiR ; βi )|i ∈ I]

(& L)

[(Γi , αi ; βi )|i ∈ I]
(→R)
[(Γi ; αi → βi )|i ∈ I]

[(Γi ; αi )|i ∈ I] [(∆i ; βi )|i ∈ I]
(& R)
[(Γi , ∆i ; αi &βi )|i ∈ I]

[(Γ, αk ; β )] ∪ M
(∩ Lk ), k = L, R
[(Γ, αL ∩ αR ; β )] ∪ M

[(Γ; α ), (Γ; β )] ∪ M
(∩ R)
[(Γ; α ∩ β )] ∪ M

Figure 3: The system ISC

Intersection Logic in sequent calculus style

20

have an additive presentation. By abuse of notation, we will call global the rules dealing with → and
& and local the rules dealing with ∩. The rules (P) and (Fus) are derivable; they will be useful in the
cut-elimination procedure.
Lemma 2.4 Let π :⊢ISC M . There is a function clean, such that clean(π ) is a derivation proving M
which does not contain applications of the rules (P) and (Fus).
Proof It is easy to check that both (P) and (Fus) commute upwards with any rule preceding them and
that they disappear when following an axiom rule. For instance:

D
[(Γ; α ), (Γ; β )] ∪ M
(∩ R)
[(Γ; α ∩ β )] ∪ M
(Fus)
[(Γ; α ∩ β ), (Γ; α ∩ β )] ∪ M

−→

D
[(Γ; α ), (Γ; β )] ∪ M
(Fus)
[(Γ; α ), (Γ; β ), (Γ; β )] ∪ M
(Fus)
[(Γ; α ), (Γ; β ), (Γ; α ), (Γ; β )] ∪ M
(∩ R)
[(Γ; α ), (Γ; β ), (Γ; α ∩ β )] ∪ M
(∩ R)
[(Γ; α ∩ β ), (Γ; α ∩ β )] ∪ M

(Ax)

[(β ; β )] ∪ [(αi ; αi )|i ∈ I]
[(β ; β ), (β ; β )] ∪ [(αi ; αi )|i ∈ I]

(Fus)

−→

[(β ; β ), (β ; β )] ∪ [(αi ; αi )|i ∈ I]

(Ax)

and
[(αi ; αi )|i ∈ I] ∪ [(αi ; αi )|i ∈ J]
[(αi ; αi )|i ∈ I]

(Ax)
(P)

−→

[(αi ; αi )|i ∈ I]

(Ax)

We will call clean a derivation without applications of rules (P) and (Fus).
Theorem 2.5 ⊢ISL M if and only if ⊢ISC M
Proof
(only if). By induction on the natural deduction style derivation. Rules (Ax), (W), (X) are the same in
both styles. Rule (P) is derivable in both styles (see previous lemma and Theorem 11 in [15]). In case
of the global rules, the proof is quite similar to the standard proof of the equivalence between natural
deduction and sequent calculus for intuitionistic case, just putting similar cases in parallel. So we will
show just the case of implication as example, and then the case for local conjunction elimination (the
introduction is the same in both the systems).
Case (→E):
(Ax)

[(Γi ; αi )]i
[(βi ; βi )]i
(→L)
[(Γi , αi → βi ; βi )]i
[(Γi ; αi → βi )]i
(cut)
[(Γi , Γi ; βi )]i
(XC)
[(Γi ; βi )]i

where the dashed line named (XC) denotes a sequence of applications of rules (X) and (C).
Case (∩Ek ):
(Ax)

[(γi ; γi )]i , (αk ; αk )
[(γi ; γi )]i , (αL ∩ αR ; αk )
[(Γi ; γi )]i , (Γ ; αL ∩ αR )
[(Γi ; γi )]i , (Γ ; αk )

(∩Lk )
(cut)

S. Ronchi Della Rocca, A. Saurin, et al.

21

(if).
By induction on the sequent calculus style derivation.
We will show just the case of implication, local conjunction elimination and cut.
Case (→L): Let Zi = Γi , ∆i , αi → βi . Then:
(Ax)

[(αi → βi ; αi → βi )]i
[(Γi ; αi )]i
[(∆i , βi ; γi )]i
(WX)
(WX)
[(Zi , βi ; γi )]i
[(Zi ; αi → βi )]i
[(Zi ; αi )]i
(→I)
[(Zi ; βi → γi )]i
[(Zi ; βi )]i
(→E)
;
[(Γi , ∆i , αi → βi γi )]i
{z
}
|

(W)
(→E)

Zi

Case (∩Lk ): Let Γi = Γ′i , θi and Ei = Γ′i , θi , θi = Γi , θi . Then:
(Ax)

[(θi ; θi )]i , (αL ∩ αR ; αL ∩ αR )
[(Γi ; γi )]i , (Γ, αk ; β )
(WX)
(WX)
[(Ei ; γi )]i , (Γ, αL ∩ αR , αk ; β )
[(Γi ; θi )]i , (Γ, αL ∩ αR ; αL ∩ αR )
(→I)
(∩Ek )
[(Γi ; θi → γi )]i , (Γ, αL ∩ αR ; αk → β )
[(Γi ; θi )]i , (Γ, αL ∩ αR ; αk )
(→E)
[(Γi ; γi )]i , (Γ, αL ∩ αR ; β )

Case (cut):
[(∆i , αi ; βi )]i
(WX)
[(Γi , ∆i , αi ; βi )]i
[(Γi ; αi )]i
(→I)
[(Γi , ∆i ; αi → βi )]i
[(Γi , ∆i ; αi )]i
[(Γi , ∆i ; βi )]i

3

(W)
(→E)

ISC and LJ

A derivation in ISC corresponds to a set of derivations in Intuitionistic Sequent Calculus (LJ), where the
two conjunctions collapse into ∧.
Definition 3.1 Given a ISC derivation π , we define the set π̃ = (πi )i∈I of LJ derivations by induction on
the structure of π as follows:
• if π : [(αi ; αi ) | i ∈ I]

(Ax)

then π̃ = (πi )i∈I with πi : αi ⊢ αi

π 1 : [(Γi ; αi ) | i ∈ I] π 2 : [(∆i , αi ; βi ) | i ∈ I]
π : [(Γi , ∆i ; βi ) | i ∈ I]
• if
and π˜2 = (πi2 : ∆i , αi ⊢ βi )i∈I , then π̃ = (πi )i∈I

π ′ : [(Γi ; βi ) | i ∈ I]
• if π : [(Γi , αi ; βi ) | i ∈ I]

(W)

(cut)

(Ax)

with π˜1 = (πi1 : Γi ⊢ αi )i∈I

πi1 : Γi ⊢ αi πi2 : ∆i , αi ⊢ βi
with
πi : Γ i , ∆ i ⊢ βi

with π˜′ = (πi′ : Γi ⊢ βi )i∈I , then π̃ = (πi )i∈I

• π̃ is defined in the same way as above for (X), (C) and (→R).

(cut)

πi′ : Γi ⊢ βi
with πi : Γi , αi ⊢ βi

(W)

Intersection Logic in sequent calculus style

22

M ′ (R)
˜ π)
• if π : M
where (R) = (Fus), (P) then π̃ = clean(

π 1 : [(Γi ; αi ) | i ∈ I] π 2 : [(∆i , βi ; γi ) | i ∈ I]
• if
π : [(Γi , ∆i , αi → βi ; γi ) | i ∈ I]
and π˜2 = (πi2 : ∆i , βi ⊢ γi )i∈I , then π̃ = (πi )i∈I

π ′ : [(Γi , αi0 , αi1 ; βi ) | i ∈ I]
• if π : [(Γi , αi0 &αi1 ; βi ) | i ∈ I]

πi′ : Γi , αi0 , αi1 ⊢ βi
with πi : Γi , αi0 ∧ αi1 ⊢ βi

(& L)

and π˜2 =

(→L)

with π˜′ = (πi′ : Γi , αi0 , αi1 ⊢ βi )i∈I , then π̃ = (πi )i∈I

(∧L)

: ∆i ⊢ βi )i∈I , then π̃ = (πi )i∈I

(&R)

with π˜1 = (πi1 : Γi ⊢ αi )i∈I

πi1 : Γi ⊢ αi πi2 : ∆i ⊢ βi
with
πi : Γi , ∆i ⊢ αi ∧ βi

π ′ : [(Γ, α j ; β )] ∪ [(Γi ; γi ) | i ∈ I]
• if π : [(Γ, α0 ∩ α1 ; β )] ∪ [(Γi ; γi ) | i ∈ I]

then π̃ = {π⋆ } ∪ (πi′ )i∈I

with π˜1 = (πi1 : Γi ⊢ αi )i∈I

πi1 : Γi ⊢ αi πi2 : ∆i , βi ⊢ γi
πi : Γi , ∆i , αi → βi ⊢ γi
with

π 1 : [(Γi ; αi ) | i ∈ I] π 2 : [(∆i ; βi ) | i ∈ I]
π : [(Γi , ∆i ; αi &βi ) | i ∈ I]
• if
(πi2

(→L)

(∩L j )

(∧R)

with π̃ ′ = {π⋆′ : Γ, α j ⊢ β } ∪ (πi′ : Γi ⊢ γi )i∈I ,

π⋆′ : Γ, α j ⊢ β
(W), (X)
Γ, α0 , α1 ⊢ β
(∧L)
with π⋆ : Γ, α0 ∧ α1 ⊢ β

π ′ : [(Γ; α ), (Γ; β )] ∪ [(Γi ; γi ) | i ∈ I]
• if π : [(Γ; α ∩ β )] ∪ [(Γi ; γi ) | i ∈ I]
πα′ : Γ ⊢ α
then π̃ = {π⋆ } ∪ (πi′ )i∈I with

(∩R)

with π˜′ = {πα′ : Γ ⊢ α }∪{πβ′ : Γ ⊢ β }∪(πi′ : Γi ⊢ γi )i∈I ,

πβ′ : Γ ⊢ β

Γ, Γ ⊢ α ∧ β
π⋆ : Γ ⊢ α ∧ β

(∧R)

(X), (C)

Let us stress the fact that, by Definition 3.1, each πi in π̃ is a derivation in LJ. The translation from
ISC to LJ is almost standard, but for the rules (Fus), (P), where the result of Lemma 2.4 has been used.

4

Cut-elimination in LJ: a short survey

Analogously to LJ, ISC enjoys cut-elimination, i.e., the cut rule is admissible. In order to give a proof of
this fact the most natural idea is to mimic the cut elimination procedure of LJ, in a parallel way. We will
use Definition 3.1, which associates to every derivation in ISC a set of derivations in LJ. There are different versions of such a proof in the literature; we suggest the versions in [9, 22, 13]. Let us briefly recall it.

S. Ronchi Della Rocca, A. Saurin, et al.

23

The cut-elimination algorithm in LJ is based on a definition of some elementary cut-elimination
steps, each one depending on the premises of the cut-rule, and on a certain order of applications of such
steps. If the elementary steps are applied in the correct order, then the procedure eventually stops and the
result is a cut-free proof of the same sequent.
The principal problem for designing this algorithm is in defining the elementary step when the contraction rule is involved. In fact the natural way of defining the contraction step is the following:
∆, α , α ⊢ β
(C)
∆, α ⊢ β
Γ⊢α
(cut)
Γ, ∆ ⊢ β

Γ⊢α
→

Γ ⊢ α ∆, α , α ⊢ β
(cut)
Γ, ∆, α ⊢ β
(cut)
Γ, Γ, ∆ ⊢ β
(CX)
Γ, ∆ ⊢ β

where (CX) represents a suitable number of contraction and exchange rules. This step generates two cuts,
such that the last one appears of the same “size” and also of the same (or maybe greater) “height” as
the original one, according to any reasonable notions of size and height. A standard way to solve this
problem is to strenghen the cut rule, allowing it to eliminate at the same time more than one occurrences
of a formula, in the following way:
m

Γ⊢α

z }| {
∆, α , ..., α ⊢ β
Γ, ∆ ⊢ β

m≥1

(multicut)

It is easy to check that replacing the cut-rule with the multicut-rule produces an equivalent system.
Abusing the naming, in what follows we will use the name “cut” for multicut and we will call “LJ” the
system obtained by replacing cut by multicut.
Assuming, for simplicity, that Γ and ∆ do not contain any occurrence of α , the contraction step now
becomes:
∆, α , α ⊢ β
(C)
Γ⊢α
Γ ⊢ α ∆, α , α ⊢ β
∆, α ⊢ β
(cut)
(cut)
→
Γ, ∆ ⊢ β
Γ, ∆ ⊢ β
and the new cut-rule which has been generated has been moved up in the derivation with respect to the
original one. The cut rule can be eliminated and, in order to design the algorithm doing it, the following
measures are needed.
Definition 4.1

i) The size of a formula σ (denoted by |σ |) is the number of symbols in it;

ii) The height of a derivation is the number of rule applications in its derivation tree. Let h(π ) denote
the height of π ;
iii) The measure of a cut π , denoted by m(π ), is a pair (s, h), where s is the size of the formula
eliminated by it and h is the sums of the heights of its premises.
We consider measures ordered according to a restriction of lexicographic order, namely:
(s, h) < (s′ , h′ ) if either s < s′ and h ≤ h′ or s ≤ s′ and h < h′ .
Then the following lemma holds:

Intersection Logic in sequent calculus style

24

Lemma 4.2 Let π : Γ ⊢ σ be a derivation in LJ, with some cut rule applications. Let π ′ : Γ ⊢ σ be
the derivation obtained from π by applying an elementary cut-elimination step to a cut closest to the
axioms, let c. Then π ′ does not contain c anymore, and, if it contains some new cuts with respect to π ,
their measure are less than the measure of c. Moreover the measures of the cuts different from c do not
increase.
The cut elimination property can now be stated.
Theorem 4.3 Let π be a derivation in LJ. Then, there is a derivation π ′ proving the same judgement
which does not use the cut-rule.
Proof From our definition of measure, a topmost cut can be eliminated in a finite number of steps.
Since the number of cuts is finite, the property follows.

5

Cut-elimination in ISC: the elementary cut elimination steps

First of all we strenghten the cut-rule of ISC analogously to LJ, in the following way:
m

z }| {
[(Γi ; αi )|i ∈ I] [(∆i , αi , ..., αi ; βi )|i ∈ I]
[(Γi , ∆i ; βi )|i ∈ I]

(cut)

It is easy to check that we obtain an equivalent system, so we will abuse the notation, and call respectively
cut the new cut, and ISC the new system.
Then, we can divide the most significant occurrences of cut in ISC in two cases: the global and local
ones, depending on whether global or local connectives are introduced on cut formulas in the premises.
In the case of global cut-rules, the elementary cut elimination steps act as for LJ, but in parallel on
all the atoms of the involved molecules. As an example, let us show the case of the (&R), (&L) cut:
[(Zi , αi , βi ; γi )]i
[(Γi ; αi )]i
[(∆i ; βi )]i
(&R)
[(Γi , ∆i ; αi &βi )]i
[(Zi , αi &βi ; γi )]i
[(Γi , ∆i , ZI ; γi )]i

(& L)
(cut)

↓
[(Zi , αi , βi ; γi )]i
[(∆i ; βi )]i
[(∆i , Zi , αi ; γi )]i
[(Γi ; αi )]i
(cut)
[(Γi , ∆i , Zi ; γi )]i

(cut)

The definition of the local cut-elimination steps in IUSC poses some problems. Let us consider the
following example:
Let π1 and π2 be respectively the following derivations:
(Ax)

(Ax)

[(α ; α ), (α ; α ), (µ ; µ )]
[(α ; α ), (α ; α ), (µ ∩ ν ; µ ∩ ν )]
(→L)
[(α , α → α ; α ), (α , α → α ; α ), (µ , µ → (µ ∩ ν ); µ ∩ ν )]
(∩R)
π1 : [(α , α → α ; α ∩ α ), (µ , µ → (µ ∩ ν ); µ ∩ ν )]
(Ax)

[(α ∩ α ; α ∩ α ), (µ ; µ )]
π2 : [(α ∩ α ; α ∩ α ), (µ ∩ ν ; µ )]

(∩L)

S. Ronchi Della Rocca, A. Saurin, et al.
And let π be:

25

π1
π2
π : [(α , α → α ; α ∩ α ), (µ , µ → (µ ∩ ν ); µ )]

(cut)

Notice that the right and left introduction of the connective ∩ create an asymmetry because they are
applied on different atoms, so it looks quite impossible to perform a cut-elimination step. In fact, the
derivation π corresponds (modulo some structural rules) to the following derivation in ISL:
(Ax)

[(α → α ; α → α ), (α → α ; α → α ), (µ → (µ ∩ ν ); µ → (µ ∩ ν ))]
[(α ; α ), (α ; α ), (µ ; µ )]
[(α , α → α ; α ), (α , α → α ; α ), (µ , µ → (µ ∩ ν ); µ ∩ ν )]
(∩E)
[(α , α → α ; α ), (α , α → α ; α ), (µ , µ → (µ ∩ ν ); µ )]
(∩I)
[(α , α → α ; α ∩ α ), (µ , µ → (µ ∩ ν ); µ )]

(Ax)
(→E)

This derivation is in normal form according to the definition given in [15]; roughly speaking, a derivation
in ISL is in normal form if it does not contain an introduction of a connective immediately followed by
an elimination of the same connective, modulo some structural rules.
Since the problem is due to the presence of the local connective, in particular when the two premises
of a cut are the right and left introduction of ∩ on different atoms, the solution is to restrict the use of this
connective, in particular forbidding atoms where it is in principal position.
Definition 5.1

i) A formula is canonical if its principal connective is not ∩.

i) An ISC derivation is canonical if all the formulas introduced by axioms and (W) are canonical.
Lemma 5.2 Let π :⊢ISC M . Then, there is a canonical derivation π ′ :⊢ISC M .
Proof

By induction on π .

The following example illustrates the base-case.
Example 5.3 Consider the derivation:
[(σ ∩ τ ; σ ∩ τ )]

(Ax)

The corresponding canonical derivation can be obtained by introducing the molecule [(σ ; σ ), (τ ; τ )] by
an axiom and then by applying a sequence of two (∩L) rules followed by a (∩R) rule.
From now on, we will only consider canonical derivations to define the cut-elimination steps. Moreover we assume that the derivations are also clean. As said before, the global rules are completely
standard, since they act like in LJ, but in parallel on all the atoms of the involved molecules. Thus, we
will expose only some characteristic cases dealing with ∩. Note the use of the structural rules (P) and
(Fus).
Definition 5.4 A cut-elimination step in ISC is defined by cases. We assume do not have applications of
rules (P) and (Fus), and we show the most interesting structural and local cases.
Commutation steps:
• case of (∩R)

Intersection Logic in sequent calculus style

26

π ′ : [(∆0 , γ0 ; α0 ), (∆0 , γ0 ; β0 )] ∪ [(∆i , γi ; δi )]1≤i≤m
(∩R)
π : [(Γ0 ; γ0 )] ∪ [(Γi ; γi )]1≤i≤m
π ′′ : [(∆0 , γ0 ; α0 ∩ β0 )] ∪ [(∆i , γi ; δi )]1≤i≤m
(cut)
[(Γ0 , ∆0 ; α0 ∩ β0 )] ∪ [(Γi , ∆i ; δi )]1≤i≤m
↓
π : [(Γ0 ; γ0 )] ∪ [(Γi ; γi )]1≤i≤m
(Fus)
′′′
π : [(Γ0 ; γ0 ), (Γ0 ; γ0 )] ∪ [(Γi ; γi )]1≤i≤m
π ′ : [(∆0 , γ0 ; α0 ), (∆0 , γ0 ; β0 )] ∪ [(∆i , γi ; δi )]1≤i≤m
[(Γ0 , ∆0 ; α0 ), (Γ0 , ∆0 ; β0 )] ∪ [(Γi , ∆i ; δi )]1≤i≤m
(∩R)
[(Γ0 , ∆0 ; α0 ∩ β0 )] ∪ [(Γi , ∆i ; δi )]1≤i≤m

(cut)

Conversion steps:
• case of symmetric ∩ rule

π : [(Γ0 ; α0 ), (Γ0 ; β0 )] ∪ [(Γi ; αi )]1≤i≤m
π ′ : [(∆0 , α0 ; γ0 )] ∪ [(∆i , αi ; γi )]1≤i≤m
(∩R)
(∩L)
[(Γ0 ; α0 ∩ β0 )] ∪ [(Γi ; αi )]1≤i≤m
[(∆0 , α0 ∩ β0 ; γ0 )] ∪ [(∆i , αi ; γi )]1≤i≤m
(cut)
[(Γi , ∆i ; γi )]i
↓
π : [(Γ0 ; α0 ), (Γ0 ; β0 )] ∪ [(Γi ; αi )]1≤i≤m
(P)
[(Γ0 ; α0 )] ∪ [(Γi ; αi )]1≤i≤m
π ′ : [(∆0 , α0 ; γ0 )] ∪ [(∆i , αi ; γi )]1≤i≤m
(cut)
[(Γi , ∆i ; γi )]i
• case of asymmetric ∩ rule

π0′ : [(∆i , σi ; τi )]i ∪ [(∆, α ∩ β ; γ ), (∆′ , µ ; ρ )]
π0 : [(Γi ; σi )]i ∪ [(Γ; α ), (Γ; β ), (Γ′ ; µ ∩ ν )]
(∩R)
π : [(Γi ; σi )]i ∪ [(Γ; α ∩ β ), (Γ′ ; µ ∩ ν )]
π ′ : [(∆i , σi ; τi )]i ∪ [(∆, α ∩ β ; γ ), (∆′ , µ ∩ ν ; ρ )]
[(Γi , ∆i ; τi )]i ∪ [(Γ, ∆; γ ), (Γ′ , ∆′ ; ρ )]

(∩L)
(cut)

Since the derivation is canonical, the ∩ in the atom (Γ′ ; µ ∩ ν ) has been introduced by a (∩R) rule.
Substituting this (∩R) rule in π by (P) and removing the (∩L) rule from π ′ , we get:
[ . . . , (Γ′′ ; µ ), (Γ′′ ; ν )]
[ . . . , (Γ′′ ; µ ∩ ν )]
..
.

(∩R)

[(Γi ; σi )]i ∪ [(Γ; α ), (Γ; β ), (Γ′ ; µ ∩ ν )]
π : [(Γi ; σi )]i ∪ [(Γ; α ∩ β ), (Γ′ ; µ ∩ ν )]

→
(∩R)

[ . . . , (Γ′′ ; µ ), (Γ′′ ; ν )]
[ . . . , (Γ′′ ; µ )]
..
.

(P)

[(Γi ; σi )]i ∪ [(Γ; α ), (Γ; β ), (Γ′ ; µ )]
πs : [(Γi ; σi )]i ∪ [(Γ; α ∩ β ), (Γ′ ; µ )]

πs : [(Γi ; σi )]i ∪ [(Γ; α ∩ β ), (Γ′ ; µ )]
π0′ : [(∆i , σi ; τi )]i ∪ [(∆, α ∩ β ; γ ), (∆′ , µ ; ρ )]
[(Γi , ∆i ; τi )]i ∪ [(Γ, ∆; γ ), (Γ′ , ∆′ ; ρ )]

(∩R)

(cut)

S. Ronchi Della Rocca, A. Saurin, et al.

27

Note that a canonical derivation remains canonical after a cut-elimination step, while a clean derivation can be transformed into a not clean one. Morever, note that all the elementary steps related to global
connectives and structural rules act locally. In fact they correspond to apply the standard cut elimination
steps of LJ in parallel in all the atoms of the considered molecule. But some cases dealing with the local
connective ∩ are not local. In particular, in the asymmetric case, the derivation can be modified in an
almost global way.

6

Cut-elimination in ISC: the algorithm

We are now ready to define the cut elimination algorithm for ISC. First we need to define a notion of
measure, for proving the termination of the algorithm.
Definition 6.1 Let π be a cut in ISC, with premises π1 and π2 . The measure of π , denoted by m(π ) is
the set {m(πi ) | πi ∈ π̃ }. m(π ) ≤ m(π ′ ) if and only if for every (s, h) ∈ m(π ) \ m(π ′ ) there is (s′ , h′ ) ∈
m(π ′ ) \ m(π ) such that (s, h) ≤ (s′ , h′ ).
An important lemma holds.
˜ π ) = {π ′ | i ∈ I}. Then
Lemma 6.2 Let π be a derivation in ISC, let π̃ = {πi | i ∈ I} and let clean(
i
′
h(πi ) = h(πi ), for all | i ∈ I.
Proof

By Lemma 2.4 and by the definition of π̃ .

Now we are able to design the cut-elimination algorithm.
Definition 6.3
i) Let π be a clean and canonical derivation in ISC, containing at least one cut rule.
Then step(π ) is the result of applying to π an elementary cut elimination step to a cut closest to
the premises.
ii) The algorithm A , which takes in input a clean and canonical proof π and produces as output a
cut-free proof π ′ , is defined as follows:
– A (π ) = i f π does not contain any cut then π else A (clean(step(π ))).
Lemma 6.4 A (π ) eventually stops.
Proof It would be necessary to check that every application of an elementary cut elimination step
makes either the cut disappearing, in case of an axiom cut, or replaces it by some cuts, with a less measure. In case of a cut involving structural rules, or global connectives, the check is easy, since the result
comes directly from Lemma 4.2, and by the definition of measure of a cut in ISC which is done in function of the measure of a cut in LJ (remember that the input proof is clean, so there are not occurrences
of (P) and of ((Fus))). So we will show only the cases of the elementary steps defined in Definition 5.4.
For readability, we will use the same terminology.
•. commutation step (∩R).
Let π̃ = {π0 : Γ0 ⊢ γ0 } ∪ {πi : Γi ⊢ γi | 1 ≤ i ≤ m}, π˜′ = {π01 : ∆0 , γ0 ⊢ α0 , π02 : ∆0 , γ0 ⊢ β0 } ∪ {πi′ :
π01 π02
(∩R)
∆i , γi ⊢ δi | 1 ≤ i ≤ m} and π˜′′ = {π0′ : ∆0 , γ0 ⊢ α0 ∩ β0
} ∪ {πi′ : ∆i , γi ⊢ δi | 1 ≤ i ≤ m}. Moreover
1
2
′
1
2
let h0 , h0 , h0 , hi , hi be respectively the heights of π0 , π0 , π0 , πi , πi′ .
The measure of the cut is : m = {(|γ0 |, h0 + h10 + h20 + 1)} ∪ {|γi |, hi + h′i ) | 1 ≤ i ≤ m}.

Intersection Logic in sequent calculus style

28

The measure of the new generated cut is: m′ = {(|γ0 |, h0 + h10 ), (|γ0 |, h0 + h20 )} ∪ {|γi |, hi + h′i ) | 1 ≤
i ≤ m}, and m′ < m, by Definition 6.1, remembering that π˜′′′ = clean(π˜′′′ ) and since the clean step does
not modify the height of π0 and πi , by Lemma 6.2.
• Conversion step: symmetric ∩ rule.
Let π̃ = {π01 : Γ0 ⊢ α0 , π02 : Γ0 ⊢ β0 } ∪ {πi : Γi ⊢ αi | 1 ≤ i ≤ m} and {π˜′ = π03 : ∆0 , α0 ⊢ γ0 } ∪ {πi′ :
∆i , αi ⊢ γi | 1 ≤ i ≤ m}. Moreover let h10 , h20 , h30 , hi , h′i be respectively the heights of π0 , π01 , π02 , π03 , πi , πi′ .
The measure of the cut is: m = {(|α0 ∩ β0 |, h10 + h20 + h30 + 2)} ∪ {(|αi |, hi + h′i ) | 1 ≤ i ≤ m}. The
measure of the new generared cut is: m′ = {(|α0 |, h10 + h30 )} ∪ {(|αi |, hi + h′i ) | 1 ≤ i ≤ m}. In computing
m′ , we used Lemma 6.2, which assures that the heigh of π01 has been not modified by the clean step.
• Conversion step: asymmetric ∩ rule
Let π˜0 = {π01 : Γ ⊢ α , π02 : Γ ⊢ β , π03 : Γ′ ⊢ µ ∩ ν } ∪ {πi : Γi ⊢ σi | i ∈ I} and {π˜0′ = π04 : ∆, α ∩ β ⊢
γ , π05 : ∆′ , µ ⊢ ρ } ∪ {πi′ : ∆i , σi ⊢ τi | i ∈ I}. Moreover let h10 , h20 , h30 , h40 , h50 , hi , h′i be respectively the heights
of π0 , π01 , π02 , π03 , π04 , π05 πi , πi′ .
The measure of the cut is: m = {(|α ∩ β |, h10 + h20 + h40 + 1)} ∪ {(|µ ∩ ν |, h30 + h50 + 1)} ∪ {(|σi |, hi +
′
hi )}. The measure of the new generared cut is: m′ = {(|α ∩ β |, h10 + h20 + h40 + 1)} ∪ {(|µ |, h30 + h50 − 1)} ∪
{(|σi |, hi + h′i )}, since, by Lemma 6.2, h(πs ) = h(π ).
So a topmost cut can be eliminated in a finite number of steps. Moreover Lemma 6.2 assures us that
the cleaning step does not increase the measure of any cut. Since the number of cuts is finite, the algorithm eventually stops.
Corollary 6.5 ISC enjoys the cut elimination property.

7

Intersection types from a logical point of view: an overview

The problem raised by Hindley, of looking for a logical system naturally connected to intersection
type assignment through the Curry-Howard isomorphism, has generated many different proposals. Very
roughly speaking, we could divide them in two categories, that we call the semantic approach and the
logical approach to the problem. The semantic approach is characterized by the fact that an extension of
the system we called IT in this paper has been considered. Namely intersection type assignment comes
with a subtyping relation, which formalizes the semantics of intersection as the meet in the continuous
function space. This subtyping relation is the essential tool in using intersection types for modelling
denotational semantics of λ -calculus, and so we call this approach semantic. The key idea here is to
avoid the rule introducing the intersection, which has not a logical explication. The first result in this
line is by Venneri [24], who designed an intersection type assignment system for Combinatory Logic, in
Hilbert style, where the introduction of intersection is replaced by an infinite set of axioms for the basic
combinators, built from their principal types. Then the subtyping rule plays the role of the intersection
introduction. In [8] this result has been enhanced, both by extending it to union types, and by giving
a logical interpretation of the subtyping relation, which turned out to correspond to the implication in
minimal relevant logic. The connection between intersection types and relevant implication has been
already noticed in [1].

S. Ronchi Della Rocca, A. Saurin, et al.

29

In the logical approach the system shown IT shown in Fig. 1 is taken into consideration, without any
subtyping relation. The aim is to design a true deductive system, such that its decoration coincide with
IT. In this line Capitani, Loreti and Venneri [5] propose a system of hypersequents, i.e., sequences of
formulae of LJ, where the distinction between global and local connectives has been already introduced.
The relation between this system and LJ cannot be formally stated, since the notion of empty formula
in an hypersequent is essential, while it has no correspondence in LJ. The relation between IT and LJ
has been clarified by Ronchi Della Rocca and Roversi, who designed IL [19], a deductive system where
formulae are tree of formulae of LJ, proved by isomorphic proofs. The result has been further enhanced
by Pimentel, Ronchi Della Rocca and Roversi [15, 16], who defined ISL and proved that the intersection
born from a splitting of the usual intuitionistic conjunction into two connectives, each one reflecting part
of its behaviour, local or global. The system ISL is extensively discussed in this paper.
A problem strongly related to the considered one is the design of a language, explicitly typed by
intersection types. Different proposals have been made. In [20], a language with this property has been
obtained as side effect of the logical approach, by a full decoration of the intersection logic IL. But
its syntax is difficult, since the syncronous behaviour of intersection types is reflected in the fact that a
term typed by an intersection type is a pair of terms which are identical, modulo type erasure. A similar
language has been proposed in [26]. All the other attempts have been made with the aim of avoiding
such a duplication of terms. Wells and Haack [25] build a language where the duplication becomes
dynamic, by enriching the syntax and by defining an operation of type selection both on terms and types.
Liquori and Ronchi Della Rocca [12] proposed a language which has an imperative flavour, since terms
are decorated by locations, which in their turn contain intersection of simply typed terms, describing the
corresponding type derivation. The last proposal is by Bono, Bettini and Venneri [4], and consists in
a language with parallel features, where parallel subterms share the same free variables, i.e., the same
resources. Since we can see a connection between the global behaviour of the arrow type and a parallel
behaviour of terms, we think it would be interesting to explore if there is a formal connection between
this language and ISL.

References
[1] F. Barbanera, S. Martini, Proof-functional connectives and realizability Archive for Mathematical Logic, 33,
189–211, 1994.
[2] F. Barbanera, M. Dezani-Ciancaglini, and U. de’Liguoro, Intersection and Union Types: Syntax and Semantics, Inform. and Comput., 119, pp. 202-230, 1995.
[3] H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini, A Filter Lambda Model and the Completeness of Type
Assignment, Journal of Symbolic Logic, 48(4), pp. 931-940, 1983.
[4] V. Bono, L. Bettini and B. Venneri, A Typed lambda calculus with Intersection Types, Theoretical Computer
Science, vol. 398 (1-3), pp. 95-113, 2008.
[5] B. Capitani, M. Loreti, B. Venneri, Hyperformulae, Parallel Deductions and Intersection Types Electr. Notes
Theor. Comput. Sci., vol. 50 (2), 2001.
[6] M. Coppo and M. Dezani-Ciancaglini, An extension of the basic functionality theory for the lambda-calculus,
Notre Dame J. Formal Logic, 21(4), pp. 685-693, 1980.
[7] Coppo M., Dezani-Ciancaglini M., Honsell F., and Longo G. “Extended Type Structures and Filter Lambda
Models”, Logic Colloquium ’82, pp.241-262, 1983.
[8] M. Dezani-Ciancaglini, S. Ghilezan, B. Venneri, Intersection Types as Logical Formulae, Notre Dame Journal
of Formal Logic, vol. 38 (2), pp. 246-269,1997 1994.

30

Intersection Logic in sequent calculus style

[9] J.-Y. Girard, Y. Lafont, and P. Taylor, Proofs and Types, Cambridge University Press, 1989.
[10] J.R. Hindley, Coppo-Dezani types do not correspond to propositional logic, Theoret. Comput. Sci., 28(1-2),
pp. 235-236, 1984.
[11] J.L.Krivine Lambda-calcul, types et modèles, Masson, 1990.
[12] L. Liquori, S. Ronchi Della Rocca, Intersection Types a la Church, Information and Computation, vol. 205
(9), pp. 1371-1386, 2007.
[13] A.R. Omondi, Proof Normalization I: Gentzen Hauptsatz, Victoria University of Wellington, Techn. Rep.CSTR 93-5, 1993.
[14] L. Paolini, M. Piccolo, S. Ronchi Della Rocca Logical Semantics for Stability, proc. MFPS 2009, LNCS,
249, pp. 429-449, 2009.
[15] E. Pimentel, S. Ronchi Della Rocca, and L. Roversi, Intersection Types: a Proof-Theoretical Approach,
ICALP’05 workshop, Proceedings of Structure and Deduction, pp. 189-204, 2005.
[16] E. Pimentel, S. Ronchi Della Rocca, and L. Roversi, Intersection Types from a proof-theoretic perspective,
Fund. Informaticae: Special Issue on Intersection Types and Related Systems, to appear.
[17] Pottinger, G. A type assignment for the strongly normalizable λ -terms. In To H. B. Curry: essays on
combinatory logic, lambda calculus and formalism, pages 561-577. Academic Press, London, 1980.
[18] S. Ronchi Della Rocca and L. Paolini, The Parametric λ -Calculus: a Metamodel for Computation, Text in
Theoretical Computer Science, Springer-Verlag, 2004.
[19] S. Ronchi Della Rocca and L. Roversi, Intersection Logic, Proceedings of CSL’01, LNCS 2142, pp. 414-428,
2001.
[20] S. Ronchi Della Rocca, Typed Intersection lambda calculus, Proc. of ITRS’02, ENTCS, vol 70, 2002.
[21] Y. Stavrinos and A. Veneti, Towards a logic for union types, Fund. Informaticae: Special Issue on Intersection Types and Related Systems, to appear.
[22] A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, 2000.
[23] A. Veneti and Y. Stavrinos, A Sequent Calculus for Intersection and Union Logic, CiE’08 Conference,
abstract in Local Proceedings of the 4th CiE Conference, p. 514, 2008.
[24] B. Venneri, Intersection Types as Logical Formulae, J.Log. Comput., vol. 4 (2), pp. 109-124, 1994.
[25] J.B. Wells, C. Haack, Branching Types, proc. of ESOP’02, LNCS, vol. 2305, pp. 115-132, 2002.
[26] J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak, A calculus with polymorphic and polyvariant flow types, J. Funct. Programming, 12(3), pp.183227, 2002.

