19 found
Order:
  1.  45
    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 (4 more)  
     
    Export citation  
     
    Bookmark   35 citations  
  2.  8
    On the Relation Between Various Negative Translations.Gilda Ferreira & Paulo Oliva - 2012 - In Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation. De Gruyter. pp. 227-258.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   7 citations  
  3.  35
    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  
     
    Bookmark   3 citations  
  4.  48
    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 (5 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  5.  34
    (1 other version)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 (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  6.  67
    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 (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  7.  65
    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 (over system T) 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 (explicitly controlled) iterated products of selection function and quantifiers, it follows that this iterated product of selection functions is T‐equivalent to the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  8.  37
    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 (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  9.  49
    The Peirce Translation.Martín Escardó & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (6):681-692.
  10.  21
    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  
     
    Bookmark   1 citation  
  11.  44
    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  
     
    Export citation  
     
    Bookmark   2 citations  
  12.  33
    Bar recursion and products of selection functions.Martín Escardó & Paulo Oliva - 2015 - Journal of Symbolic Logic 80 (1):1-28.
    We show how two iterated products of selection functions can both be used in conjunction with systemTto interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over systemTto Spector’s bar recursion, whereas the other isT-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of ‘skewed’ selection functions. Iterations of the dependent binary products are also considered but (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  13.  42
    A parametrised functional interpretation of Heyting arithmetic.Bruno Dinis & Paulo Oliva - 2021 - Annals of Pure and Applied Logic 172 (4):102940.
  14.  30
    Double Negation Semantics for Generalisations of Heyting Algebras.Rob Arthan & Paulo Oliva - 2020 - Studia Logica 109 (2):341-365.
    This paper presents an algebraic framework for investigating proposed translations of classical logic into intuitionistic logic, such as the four negative translations introduced by Kolmogorov, Gödel, Gentzen and Glivenko. We view these asvariant semanticsand present a semantic formulation of Troelstra’s syntactic criteria for a satisfactory negative translation. We consider how each of the above-mentioned translation schemes behaves on two generalisations of Heyting algebras: bounded pocrims and bounded hoops. When a translation fails for a particular class of algebras, we demonstrate that (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  15.  49
    On bounded functional interpretations.Gilda Ferreira & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (8):1030-1049.
  16.  27
    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  
     
    Export citation  
     
    Bookmark   1 citation  
  17.  69
    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 (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  18.  16
    On the Herbrand functional interpretation.Paulo Oliva & Chuangjie Xu - 2020 - Mathematical Logic Quarterly 66 (1):91-98.
    We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of “sets of functionals” in the interpretation of implication and universal quantification. This is done by presenting an alternative formulation of the Herbrand functional interpretation, which we show to be equivalent to the original presentation. As a result of this investigation we also strengthen the monotonicity property of the original presentation, and prove a monotonicity property for our alternative definition.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  19.  33
    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  
     
    Bookmark