Dissertação

On the herbrandised interpretation for nonstandard arithmetic EVALUATED

As interpretações funcionais são ferramentas úteis da teoria da demonstração. Depois de Gödel ter descrito a sua interpretação dialectica para a aritmética de Heyting, foram propostas muitas outras interpretações, cada uma com objectivos diferentes. Começamos por apresentar as interpretações de Gödel e Shoenfield. Propomos uma interpretação funcional para a aritmética de Heyting não standard, baseada em trabalho de Van den Berg, Briseid e Safarik. Esta interpretação permite a transformação de provas na aritmética não standard de teoremas internos em provas na aritmética standard desses mesmos teoremas. As testemunhas para afirmações existenciais externas das fórmulas interpretadoras são funções cujo output é uma lista finita. Sintacticamente, os termos que representam estas funções são chamados termos end-star. É possível definir uma pré-ordem nos termos end-star. A nossa interpretação é monótona nesta pré-ordem: se um dado termo end-star é uma testemunha para uma afirmação existencial, então qualquer termo "maior" também o é. Usando esta propriedade, provamos a correcção da nossa interpretação, e eliminamos princípios reconhecíveis da análise não standard. Também obtemos como corolário que a aritmética não standard é conservativa sobre a aritmética standard, bem como um teorema de extracção de termos. É possível provar um teorema de caracterização para a nossa interpretação. Como corolário, mostramos que o princípio da saturação contável não acrescenta força ao nosso sistema intuicionista não standard. Por fim, descrevemos brevemente a redutibilidade de Weihrauch e sugerimos uma aplicação da interpretação dialectica de Gödel para, em certas circunstâncias, decidir se uma fórmula-∀∃ se reduz-Weihrauch a outra.
Interpretações funcionais, aritmética não standard, redutibilidade de Weihrauch

Dezembro 12, 2016, 15:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Ulrich Kohlenbach

TU Darmstadt

Professor Catedratico

ORIENTADOR

Fernando Jorge Inocêncio Ferreira

Departamento de Matemática, Faculdade de Ciências, ULisboa

Professor Catedratico

ORIENTADOR

Carlos Manuel Costa Lourenço Caleiro

Departamento de Matemática (DM)

Professor Associado