The Noble Art of Linear Decorating [PhD Thesis]

Description

Linear logic (Girard,1987) sprouts from the remarkable observation that a certain semantical decomposition of intuitionistic type constructors corresponds on a syntactical level to the banning of structural rules of weakening and contraction from the formulation of intuitionistic'logic as a sequent calculus, followed by their resurrection in modalized form. It then is a small, but important, step to apply this latter, purely formal, manipulation to sequent calculi also for classical logic, and marvel at the consequences. Soon following its introduction, linear logic became the topic of a quickly growing number of research- and survey-papers, and inspired workers in proof theory, category theory, complexity theory, theoretical and not-so-theoretical computer science, all eager to explore the possible, impossible, the more, as well as the less, probable, implications and applications. As a result, in much less than a decade, the field has become so extensive, that, in the present context, we will not even try to give a comprehensive overview. The optic of this thesis, then, is a fairly modest one: linear sequent calculus appears as a refinement of the known calculi for both intuitionistic and classical logic. It therefore can be considered a tool to investigate, as if through a microscope, behaviour and properties of intuitionistic and classical sequent derivations. It is on a such proof theoretical study that we will embark.