Switch to: References

Add citations

You must login to add citations.
  1. The FAN principle and weak König's lemma in herbrandized second-order arithmetic.Fernando Ferreira - 2020 - Annals of Pure and Applied Logic 171 (9):102843.
    We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are interpreted by finite sets of natural numbers.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • On bounded functional interpretations.Gilda Ferreira & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (8):1030-1049.
    Download  
     
    Export citation  
     
    Bookmark  
  • 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.
    Download  
     
    Export citation  
     
    Bookmark   2 citations