Utilize este identificador para referenciar este registo: http://hdl.handle.net/10451/11769
Título: Unificação das interpretações funcionais: via lógica linear intuicionista
Autor: Reis, Sílvia da Conceição Alexandre
Orientador: Ferreira, Fernando, 1958-
Ferreira, Gilda Maria Saraiva Dias,1976-
Palavras-chave: Lógica intuicionista
Lógica linear intuicionista
Interpretações funcionais
Realizabilidade
Unificação de interpretações funcionais
Cálculo de sequentes
Teses de mestrado - 2014
Data de Defesa: 2014
Resumo: A presente dissertação em Lógica Matemática, enquadrada no âmbito da Teoria da Demonstração, centra-se no conceito de “interpretação funcional”. Em termos informais, uma interpretação funcional consiste numa interpretação (de fórmulas de um sistema para fórmulas de outro sistema), que pode ser encarada como uma correspondência entre fórmulas e jogos, e num teorema que, intuitivamente, faz corresponder provas a estratégias vencedoras. A terminologia “interpretação funcional” parece ser relativamente recente, mas o conceito (ou, no mínimo, exemplos concretos do mesmo) data pelo menos da década de 50. Com efeito, foi em 1958 que Gödel propôs a famosa interpretação Dialéctica, e apenas um ano mais tarde surge a Realizabilidade Modificada de Kreisel. É sobre estas duas interpretações funcionais, juntamente com a variante da Dialéctica mais tarde proposta por Diller e Nahm, que nos debruçamos ao longo deste texto. O nosso principal objectivo é demonstrar que é possível apresentar as três interpretações funcionais do parágrafo anterior como “variantes” de uma única interpretação funcional, parametrizada. Para tal, introduziremos e motivaremos o contexto da Lógica Linear, criada por J.–Y. Girard e apresentada pela primeira vez em [17]. Estaremos em particular interessados na Lógica Linear Intuicionista, uma vez que é nesta lógica que será feita a unificação. A unificação será obtida apresentando uma interpretação linear “básica”, que representará a parte comum à realizabilidade modificada, à Dialéctica e à variante de Diller–Nahm, juntamente com três instanciações de um parâmetro, que corresponderá ao que as diferencia.
We present a dissertation in Mathematical Logic, specifically within the framework of Proof Theory, centered on the concept of functional interpretation. Informally, a functional interpretation consists of an interpretation, which maps formulas of a system into formulas of another system and which can be thought of as a correspondence between formulas and games, and a theorem, which, intuitively, associates proofs with winning strategies. The terminology “functional interpretation” seems to be relatively recent, but the concept it represents (or, at least, specific examples of it) is known and studied since the fifties. It was indeed in 1958 that Gödel presented his famous Dialectica interpretation, and barely a year after that Kreisel introduced his Modified Realizability. These two functional interpretations, together with the Dialectica variant presented later by Diller and Nahm, will be the object of our study throughout the text. Our main goal will be to show that it is possible to present the three functional interpretations mentioned above as “variants” of one parametrized functional interpretation. In order to do so, we will motivate and introduce the context of Linear Logic, first introduced by J.–Y. Girard in [17]. We will be specifically interested in Intuitionistic Linear Logic, since the unification will be obtained within this context. The unification, as we will see, will be done by means of presenting a “basic” functional interpretation, representing the common part to modified realizability, Dialectica and Diller–Nahm’s variant, together with three instantiations of a parameter, corresponding to what differentiates these interpretations.
Descrição: Tese de mestrado em Matemática, apresentada à Universidade de Lisboa, através da Faculdade de Ciências, 2014
URI: http://hdl.handle.net/10451/11769
Aparece nas colecções:FC - Dissertações de Mestrado

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
ulfc109432_tm_Silvia_Reis.pdf1,09 MBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.