Order:
Disambiguations
Paulo Oliva [17]P. Oliva [1]Pedro Riquelme Oliva [1]Pilar Herráiz Oliva [1]
  1.  2
    Bounded Functional Interpretation.Fernando Ferreira & Paulo Oliva - 2005 - Annals of Pure and Applied Logic 135 (1):73-112.
    We present a new functional interpretation, based on a novel assignment of formulas. In contrast with Gödel’s functional “Dialectica” interpretation, the new interpretation does not care for precise witnesses of existential statements, but only for bounds for them. New principles are supported by our interpretation, including the FAN theorem, weak König’s lemma and the lesser limited principle of omniscience. Conspicuous among these principles are also refutations of some laws of classical logic. Notwithstanding, we end up discussing some applications of the (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   21 citations  
  2.  27
    On Spector's Bar Recursion.Paulo Oliva & Thomas Powell - 2012 - Mathematical Logic Quarterly 58 (4-5):356-265.
    We show that Spector's “restricted” form of bar recursion is sufficient to define Spector's search functional. This new result is then used to show that Spector's restricted form of bar recursion is in fact as general as the supposedly more general form of bar recursion. Given that these two forms of bar recursion correspond to the iterated products of selection function and quantifiers, it follows that this iterated product of selection functions is T-equivalent to the corresponding iterated product of quantifiers.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  3.  7
    Unifying Functional Interpretations.Paulo Oliva - 2006 - Notre Dame Journal of Formal Logic 47 (2):263-290.
    This article presents a parametrized functional interpretation. Depending on the choice of two parameters one obtains well-known functional interpretations such as Gödel's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kohlenbach's monotone interpretations, Kreisel's modified realizability, and Stein's family of functional interpretations. A functional interpretation consists of a formula interpretation and a soundness proof. I show that all these interpretations differ only on two design choices: first, on the number of counterexamples for A which became witnesses for ¬A when defining (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  4.  3
    Proof Mining in L1-Approximation.Ulrich Kohlenbach & Paulo Oliva - 2003 - Annals of Pure and Applied Logic 121 (1):1-38.
    In this paper, we present another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation developed in Kohlenbach , Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheney's simplification 189) of Jackson's original proof 320) of the uniqueness of the best L1-approximation of continuous functions fC[0,1] by polynomials pPn of degree n. Cheney's (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  5.  37
    An Analysis of Gödel's Dialectica Interpretation Via Linear Logic.Paulo Oliva - 2008 - Dialectica 62 (2):269–290.
    This article presents an analysis of Gödel's dialectica interpretation via a refinement of intuitionistic logic known as linear logic. Linear logic comes naturally into the picture once one observes that the structural rule of contraction is the main cause of the lack of symmetry in Gödel's interpretation. We use the fact that the dialectica interpretation of intuitionistic logic can be viewed as a composition of Girard's embedding of intuitionistic logic into linear logic followed by de Paiva's dialectica interpretation of linear (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  6. Bar Recursion and Products of Selection Functions.Martín Escardó & Paulo Oliva - 2015 - Journal of Symbolic Logic 80 (1):1-28.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  7.  1
    Bounded Functional Interpretation and Feasible Analysis.Fernando Ferreira & Paulo Oliva - 2007 - Annals of Pure and Applied Logic 145 (2):115-129.
    In this article we study applications of the bounded functional interpretation to theories of feasible arithmetic and analysis. The main results show that the novel interpretation is sound for considerable generalizations of weak König’s Lemma, even in the presence of very weak induction. Moreover, when this is combined with Cook and Urquhart’s variant of the functional interpretation, one obtains effective versions of conservation results regarding weak König’s Lemma which have been so far only obtained non-constructively.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  8.  18
    The Peirce Translation.Martín Escardó & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (6):681-692.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  9.  13
    Confined Modified Realizability.Gilda Ferreira & Paulo Oliva - 2010 - Mathematical Logic Quarterly 56 (1):13-28.
    We present a refinement ofthe bounded modified realizability which provides both upper and lower bounds for witnesses. Our interpretation is based on a generalisation of Howard/Bezem's notion of strong majorizability. We show how the bounded modified realizability coincides with our interpretation in the case when least elements exist . The new interpretation, however, permits the extraction of more accurate bounds, and provides an ideal setting for dealing directly with data types whose natural ordering is not well-founded.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  10.  4
    A Direct Proof of Schwichtenberg’s Bar Recursion Closure Theorem.Paulo Oliva & Silvia Steila - 2018 - Journal of Symbolic Logic 83 (1):70-83.
    Schwichtenberg showed that the System T definable functionals are closed under a rule-like version Spector’s bar recursion of lowest type levels 0 and 1. More precisely, if the functional Y which controls the stopping condition of Spector’s bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg’s original proof, however, relies on a detour through Tait’s infinitary terms and the correspondence between ordinal recursion for α < ε₀ and primitive recursion over (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  11.  10
    On the Computational Complexity of Best L1-Approximation.Paulo Oliva - 2002 - Mathematical Logic Quarterly 48 (S1):66-77.
    It is well known that for a given continuous function f : [0, 1] → ℝ and a number n there exists a unique polynomial pn ∈ Pn which best L1-approximates f. We establish the first upper bound on the complexity of the sequence n∈ ℕ, assuming f is polynomial-time computable. Our complexity analysis makes essential use of the modulus of uniqueness for L1-approximation presented in [13].
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  12.  9
    Bar Recursion Over Finite Partial Functions.Paulo Oliva & Thomas Powell - 2017 - Annals of Pure and Applied Logic 168 (5):887-921.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  13.  16
    On Bounded Functional Interpretations.Gilda Ferreira & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (8):1030-1049.
  14.  3
    The Herbrand Functional Interpretation of the Double Negation Shift.Martín Escardó & Paulo Oliva - 2017 - Journal of Symbolic Logic 82 (2):590-607.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  15.  5
    Proof Interpretations with Truth.Jaime Gaspar & Paulo Oliva - 2010 - Mathematical Logic Quarterly 56 (6):591-610.
    This article systematically investigates so-called “truth variants” of several functional interpretations. We start by showing a close relation between two variants of modified realizability, namely modified realizability with truth and q-modified realizability. Both variants are shown tobe derived from a single “functional interpretation with truth” of intuitionistic linear logic. This analysis suggests that several functional interpretations have truth and q-variants. These variants, however, require a more involved modification than the ones previously considered. Following this lead we present truth and q-variants (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  16.  1
    An Analysis of Gödel's Dialectica Interpretation Via Linear Logic.Paulo Oliva - 2008 - Dialectica 62 (2):269-290.
    This article presents an analysis of Gödel's dialectica interpretation via a refinement of intuitionistic logic known as linear logic. Linear logic comes naturally into the picture once one observes that the structural rule of contraction is the main cause of the lack of symmetry in Gödel's interpretation. We use the fact that the dialectica interpretation of intuitionistic logic can be viewed as a composition of Girard's embedding of intuitionistic logic into linear logic followed by de Paiva's dialectica interpretation of linear (...)
    No categories
    Direct download  
     
    Export citation  
     
    My bibliography  
  17.  2
    Proof Mining in< I> L_< Sub> 1-Approximation.Ulrich Kohlenbach & Paulo Oliva - 2003 - Annals of Pure and Applied Logic 121 (1):1-38.
  18. Belegradek, O., Verbovskiy, V. And Wagner, FO, Coset.J. Y. Halpern, B. M. Kapron, V. S. Harizanov, U. Kohlenbach, P. Oliva, F. Lucas, B. Luttik, P. Matet & M. Pourmahdian - 2003 - Annals of Pure and Applied Logic 121:287.
     
    Export citation  
     
    My bibliography  
  19. Kellie Robertson. Nature Speaks: Medieval Literature and Aristotelian Philosophy. X + 439 Pp., Figs., Bibl., Index. Philadelphia: University of Pennsylvania Press, 2017. $69.95. [REVIEW]Pilar Herráiz Oliva - 2018 - Isis 109 (2):380-381.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography