A carregar...
Publicação
Unificação das interpretações funcionais: via lógica linear intuicionista
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 1.07 MB | Adobe PDF |
Resumo(s)
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.
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
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