Switch to: References

Add citations

You must login to add citations.
  1. Extensional realizability.Jaap van Oosten - 1997 - Annals of Pure and Applied Logic 84 (3):317-349.
    Two straightforward “extensionalisations” of Kleene's realizability are considered; denoted re and e. It is shown that these realizabilities are not equivalent. While the re-notion is a subset of Kleene's realizability, the e-notion is not. The problem of an axiomatization of e-realizability is attacked and one arrives at an axiomatization over a conservative extension of arithmetic, in a language with variables for finite sets. A derived rule for arithmetic is obtained by the use of a q-variant of e-realizability; this rule subsumes (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • On Goodman Realizability.Emanuele Frittaion - 2019 - Notre Dame Journal of Formal Logic 60 (3):523-550.
    Goodman’s theorem states that HAω+AC+RDC is conservative over HA. The same result applies to the extensional case, that is, E-HAω+AC+RDC is also conservative over HA. This is due to Beeson. In this article, we modified the Goodman realizability and provide a new proof of the extensional case.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • About Goodmanʼs Theorem.Thierry Coquand - 2013 - Annals of Pure and Applied Logic 164 (4):437-442.
    We present a proof of Goodmanʼs Theorem, which is a variation of the proof of Renaldel de Lavalette [9]. This proof uses in an essential way possibly divergent computations for proving a result which mentions systems involving only terminating computations. Our proof is carried out in a constructive metalanguage. This involves implicitly a covering relation over arbitrary posets in formal topology, which occurs in forcing in set theory in a classical framework, but can also be defined constructively.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations