Introduction to Linear Logic

Torben Braüner

December 1996

Abstract:

The main concern of this report is to give an introduction to Linear Logic. For pedagogical purposes we shall also have a look at Classical Logic as well as Intuitionistic Logic. Linear Logic was introduced by J.-Y. Girard in 1987 and it has attracted much attention from computer scientists, as it is a logical way of coping with resources and resource control. The focus of this technical report will be on proof-theory and computational interpretation of proofs, that is, we will focus on the question of how to interpret proofs as programs and reduction (cut-elimination) as evaluation. We first introduce Classical Logic. This is the fundamental idea of the proofs-as-programs paradigm. Cut-elimination for Classical Logic is highly non-deterministic; it is shown how this can be remedied either by moving to Intuitionistic Logic or to Linear Logic. In the case on Linear Logic we consider Intuitionistic Linear Logic as well as Classical Linear Logic. Furthermore, we take a look at the Girard Translation translating Intuitionistic Logic into Intuitionistic Linear Logic. Also, we give a brief introduction to some concrete models of Intuitionistic Linear Logic. No proofs will be given except that a proof of cut-elimination for the multiplicative fragment of Classical Linear Logic is included in an appendix

Contents

1

Classical and Intuitionistic Logic

1.1

Classical Logic

1.2

Intuitionistic Logic

1.3

The -Calculus

1.4

The Curry-Howard Isomorphism

2

Linear Logic

2.1

Classical Linear Logic

2.2

Intuitionistic Linear Logic

2.3

A Digression - Russell's Paradox and Linear Logic

2.4

The Linear -Calculus

2.5

The Curry-Howard Isomorphism

2.6

The Girard Translation

2.7

Concrete Models

A

Logics

A.1

Classical Logic

A.2

Intuitionistic Logic

A.3

Classical Linear Logic

A.4

Intuitionistic Linear Logic

B

Cut-Elimination for Classical Linear Logic

B.1

B.2

Putting the Proof Together

Available as PostScript, PDF, DVI.