2-CATEGORY AND PROOF THEORY
CONSELHO NACIONAL DE DESENVOLVIMENTO CIENTÍFICO E TECNOLÓGICO === Dedução Natural para a lógica intuicionista tem sido relacionada à Teoria das Categorias através do que agora é conhecido por Lógica Categórica. Essa relação é fortemente baseada no isomorfismo de Curry-Howard entre Dedução Natural e...
| Main Author: | |
|---|---|
| Other Authors: | |
| Language: | English |
| Published: |
PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO
2009
|
| Online Access: | http://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=15181@1 http://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=15181@2 |
| Summary: | CONSELHO NACIONAL DE DESENVOLVIMENTO CIENTÍFICO E TECNOLÓGICO === Dedução Natural para a lógica intuicionista tem sido relacionada à Teoria das Categorias através do que agora é conhecido por Lógica Categórica. Essa relação é fortemente baseada no isomorfismo de Curry-Howard entre Dedução Natural e (lambda)-Cálculo Tipado. Esta dissertação descreve alguns aspectos dessa relação com o objetivo de propor uma visão 2-categórica da Lógica Categórica. Mostramos que mesmo numa visão 2-cateórica algumas desvantagens conhecidas na Teoria das Categorias continuam valendo. Concluímos essa dissertação discutindo as vantagens de uma visão 2-categórica a partir de premissas mais fracas. === Natural Deduction for intuitionistic logic has been related to Category Theory by what now is known as Categorical Logic. This relationship is strongly based on the Curry-Howard Isomorphism between Natural Deduction and typed (lambda)-Calculus. This dissertation describes some aspects of these relationship with the aim of proposing a 2-categorical view of categorical logic. We show that even under this 2-categorical view some of the drawbacks already known in ordinary Category Theory remain holding. We conclude this dissertation discussing the advantages of 2-categorical view under some weaker assumptions. |
|---|