Universidade de Lisboa Repositório da Universidade de Lisboa

Repositório da Universidade de Lisboa >
Faculdade de Ciências (FC) >
FC - Teses de Doutoramento >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10451/1626

Title: Proof-theoretical studies on the bounded functional interpretation
Authors: Engrácia, Patrícia, 1980-
Advisor: Ferreira, Fernando, 1958-
Keywords: Álgebra
Teses de doutoramento
Issue Date: 2009
Abstract: 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.
Description: 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
Appears in Collections:FC - Teses de Doutoramento

Files in This Item:

File Description SizeFormat
19133_ulsd_re467_Proof.pdf815.07 kBAdobe PDFView/Open
FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpaceOrkut
Formato BibTex mendeley Endnote Logotipo do DeGóis 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.


  © Universidade de Lisboa / SIBUL
Alameda da Universidade | Cidade Universitária | 1649-004 Lisboa | Portugal
Tel. +351 217967624 | Fax +351 217933624 | repositorio@reitoria.ul.pt - Feedback - Statistics
  Estamos no RCAAP Governo Português separator Ministério da Educação e Ciência   Fundação para a Ciência e a Tecnologia

Financiado por: