Categorical semantics of linear logic

Dissertação de mestrado em MatemáticaFazemos uma breve introdução à lógica intuicionista, ao cálculo- e à teoria de categorias com objetivo de demonstrar a profunda relação entre programas, provas e morfismos em categorias cartesianas fechadas: apresentamos o isomorfismo de Curry-Howard, mostramos que sistemas de dedução para um certo fragmento da lógica intuicionista podem ser vistos como categorias e definimos uma semântica categorial para o cálculo- tipificado. Introduzimos a lógica linear intuicionista e descrevemos as transformações para a eliminação do corte. Mostramos que, identificando as derivações da lógica linear intuicionista a menos das transformações para a eliminação do corte juntamente com algumas transformações simples, obtemos classes que se organizam-se espontaneamente como uma categorial monoidal. Após definirmos categorias-2 de categorias monoidais e uma série de conceitos categoriais relacionados, definimos, com todo o detalhe, uma semântica categorial para a lógica linear intuicionista. Por último, apresentamos três axiomatizações distintas para modelos da lógica linear e mostramos que espaços de coerência podem ser vistos como um destes modelos.We start with a brief introduction to intuitionistic logic, -calculus and category theory with the objective of illustrating the deep connection between programs, proofs and morphisms in closed cartesian categories. We elaborate on this by demonstrating the Curry-Howard isomorphism, showing that deduction systems for a given fragment of intuitionistic logic can be seen as categories and defining a categorical semantics for typed -calculus. We define intuitionistic linear logic and describe the transformations involved in cut elimination. We prove that, by identifying the intuitionistic linear logic derivations up to the transformations in cut elimination together with a few other simple transformations, we obtain classes that spontaneously organize themselves into a monoidal category. After defining 2-categories of monoidal categories and a series of related categorical concepts, we define, in full detail, a categorical semantics for intuitionistic linear logic. Lastly, we present three distinct axiomatizations for models of linear logic and show that coherence spaces are one such model