Abstract

In maths, a hypothesis can be used as many times as needed: if A is true, and A => B is true, then B is true, but A is still true after that. Things are different in real life. For example, if A is to spend £1 on apples, and B is to get them, then you lose £1 in the process and you cannot do it again.

Linear logic is a refinement of intuitionistic and classical logic, which takes this into account by forbidding the duplication and disposal of some hypotheses. This is interesting on the proof- theoretical side, but it is also very relevant to computer science, where we need to reason about the consumption of resources (e.g. time, memory). Linear logic has therefore been very influential in the study of programming languages, leading in particular to game semantics, and to a range of denotational semantics for languages with probabilistic or quantum features.

I will introduce the syntax of linear logic, which involves two new connectives for AND , two for OR, and a unary operator ”!” indicating which hypotheses we are allowed to duplicate or discard. If I have time, I will mention some well-known models of linear logic, and present a categorical axiomatisation of these models.

Covering:

• The connectives of linear logic and their meaning
• The linear sequent calculus
• Some models of linear logic
• Categorical semantics

I will only assume a basic understanding of

• Classical and intuitionistic logics
• Sequent calculus and Curry-Howard correspondence
• Category theory