Switch to: Citations

Add references

You must login to add references.
  1. A constructive approach to nonstandard analysis.Erik Palmgren - 1995 - Annals of Pure and Applied Logic 73 (3):297-325.
    In the present paper we introduce a constructive theory of nonstandard arithmetic in higher types. The theory is intended as a framework for developing elementary nonstandard analysis constructively. More specifically, the theory introduced is a conservative extension of HAω + AC. A predicate for distinguishing standard objects is added as in Nelson's internal set theory. Weak transfer and idealisation principles are proved from the axioms. Finally, the use of the theory is illustrated by extending Bishop's constructive analysis with infinitesimals.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • A model for intuitionistic non-standard arithmetic.Ieke Moerdijk - 1995 - Annals of Pure and Applied Logic 73 (1):37-51.
    This paper provides an explicit description of a model for intuitionistic non-standard arithmetic, which can be formalized in a constructive metatheory without the axiom of choice.
    Download  
     
    Export citation  
     
    Bookmark   21 citations  
  • The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
    In this note we show that Friedman's syntactic translation for intuitionistic logical systems can be carried over to Martin-Löf's type theory, inlcuding universes provided some restrictions are made. Using this translation we show that the theory is closed under a higher type version of Markov's rule.
    Download  
     
    Export citation  
     
    Bookmark   1 citation