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.
dezembro 12, 2016, 15:0
Publicação
Obra sujeita a Direitos de Autor
Orientação
ORIENTADOR
Fernando Jorge Inocêncio Ferreira
Departamento de Matemática, Faculdade de Ciências, ULisboa
Professor Catedratico
