Switch to: References

Add citations

You must login to add citations.
  1. Affine logic for constructive mathematics.Michael Shulman - 2022 - Bulletin of Symbolic Logic 28 (3):327-386.
    We show that numerous distinctive concepts of constructive mathematics arise automatically from an “antithesis” translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically “constructivize” classical definitions, handling the resulting bookkeeping automatically.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • The Limits of Computation.Andrew Powell - 2022 - Axiomathes 32 (6):991-1011.
    This article provides a survey of key papers that characterise computable functions, but also provides some novel insights as follows. It is argued that the power of algorithms is at least as strong as functions that can be proved to be totally computable in type-theoretic translations of subsystems of second-order Zermelo Fraenkel set theory. Moreover, it is claimed that typed systems of the lambda calculus give rise naturally to a functional interpretation of rich systems of types and to a hierarchy (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • On bounded functional interpretations.Gilda Ferreira & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (8):1030-1049.
    Download  
     
    Export citation  
     
    Bookmark  
  • Light dialectica revisited.Mircea-Dan Hernest & Trifon Trifonov - 2010 - Annals of Pure and Applied Logic 161 (11):1379-1389.
    We upgrade the light Dialectica interpretation [6] by adding two more light universal quantifiers, which are both semi-computational and semi-uniform and complement each other. An illustrative example is presented for the new light quantifiers and a new application is given for the older uniform quantifier. The realizability of new light negative formulations for the Axiom of Choice and for the Independence of Premises is explored in the new setting.
    Download  
     
    Export citation  
     
    Bookmark  
  • A parametrised functional interpretation of Heyting arithmetic.Bruno Dinis & Paulo Oliva - 2021 - Annals of Pure and Applied Logic 172 (4):102940.
    Download  
     
    Export citation  
     
    Bookmark