Utilize este identificador para referenciar este registo: http://hdl.handle.net/10451/1626
Título: Proof-theoretical studies on the bounded functional interpretation
Autor: Engrácia, Patrícia, 1980-
Orientador: Ferreira, Fernando, 1958-
Palavras-chave: Álgebra
Teses de doutoramento
Data de Defesa: 2009
Resumo: This dissertation studies the bounded functional interpretation of Ferreira and Oliva. The work follows two different directions. We start by focusing on the generalization of the bounded functional interpretation to second-order arithmetic (a.k.a. analysis). This is accomplished via bar recursion, a well-founded form of recursion. We carry out explicitly the bounded functional interpretation of the (non-intuitionistic) law of the double negation shift with bar recursive functionals of finite type. As a consequence, we show that full numerical comprehension has bounded functional interpretation in the classical case. In the other direction, we extend the bounded functional interpretation with new base types, representing an abstract class of normed spaces. Some studies on the representation of the real numbers are carried out, as it is useful to have a representation which meshes well with the notion of majorizability. A majorizability theorem holds. We carry out the extension of the bounded functional interpretation to new base types and prove a soundness theorem with characteristic principles similar to the numerical case. We also extend the classical direct bounded functional interpretation of Peano arithmetic to new base types and prove the corresponding soundness theorem. The characteristic principles are also similar to the ones in the numerical case. In the classical setting, these prove that linear operators are automatically bounded and that Cauchy sequences (with a modulus of Cauchyness) of elements of the new base type do converge. Relying on the characteristic principles (and on a special form of choice), a logical version of the Baire category theorem of functional analysis is proved. As a consequence, we also prove logical versions of the Banach-Steinhaus and the open mapping theorems.
Descrição: Tese de doutoramento, Matemática (Álgebra Lógica e Fundamentos), 2009, Universidade de Lisboa, Faculdade de Ciências
URI: http://catalogo.ul.pt/F/?func=item-global&doc_library=ULB01&type=03&doc_number=000561723
http://hdl.handle.net/10451/1626
Aparece nas colecções:FC - Teses de Doutoramento

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
19133_ulsd_re467_Proof.pdf815,07 kBAdobe 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.