Dissertação
Bar recursion with abstract types// a study on the bounded functional interpretation EVALUATED
As interpretações funcionais são uma ferramenta importante em teoria da demonstração. Estudamos duas extensões à interpretação funcional limitada de Ferreira e Oliva, no contexto da lógica clássica, que contribuem para a sua aplicabilidade em estudos de proof mining. A primeira extensão introduz definições por bar recursão, uma forma de recursão transfinita em árvores bem fundadas. Com esta adição, a interpretação funcional limitada pode ser usada para analisar demonstrações que envolvam o princípio das escolhas dependentes e o princípio da compreensão numérica. A segunda extensão diz respeito à inclusão de um tipo abstrato, isto é, à inclusão de um tipo base adicional. Este tipo pode representar um anel, ou um espaço métrico, por exemplo. Como consequência, a interpretação funcional limitada pode ser usada para a análise de demonstrações sobre estruturas matemáticas arbitrárias sem que estas tenham que ser codificadas. O objetivo é estudar a extensão da interpretação funcional limitada simultaneamente com bar recursão e com um tipo abstrato. Verificamos em detalhe, na presença de um tipo abstrato, a dedução do princípio das escolhas dependentes a partir de bar indução, o princípio de demonstração associado à bar recursão. Numa aplicação, mostramos que a interpretação funcional limitada estendida completa automaticamente os espaços métricos.
dezembro 21, 2021, 9:30
Publicação
Obra sujeita a Direitos de Autor
Orientação
