Please use this identifier to cite or link to this item:
Title: Proof-theoretical studies on the bounded functional interpretation
Author: Engrácia, Patrícia, 1980-
Advisor: Ferreira, Fernando, 1958-
Keywords: Álgebra
Teses de doutoramento
Defense 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
Appears in Collections:FC - Teses de Doutoramento

Files in This Item:
File Description SizeFormat 
19133_ulsd_re467_Proof.pdf815,07 kBAdobe PDFView/Open

FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

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