2-CATEGORY AND PROOF THEORY / 2-CATEGORIA E TEORIA DA PROVA

AUTOR(ES)
DATA DE PUBLICAÇÃO

2009

RESUMO

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.

ASSUNTO(S)

deducao natural natural deduction

Documentos Relacionados