Switch to: References

Add citations

You must login to add citations.
  1. Some axioms for constructive analysis.Joan Rand Moschovakis & Garyfallia Vafeiadou - 2012 - Archive for Mathematical Logic 51 (5-6):443-459.
    This note explores the common core of constructive, intuitionistic, recursive and classical analysis from an axiomatic standpoint. In addition to clarifying the relation between Kleene’s and Troelstra’s minimal formal theories of numbers and number-theoretic sequences, we propose some modified choice principles and other function existence axioms which may be of use in reverse constructive analysis. Specifically, we consider the function comprehension principles assumed by the two minimal theories EL and M, introduce an axiom schema CFd asserting that every decidable property (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Essay Review.M. Detlefsen - 1988 - History and Philosophy of Logic 9 (1):93-105.
    S. SHAPIRO (ed.), Intensional Mathematics (Studies in Logic and the Foundations of Mathematics, vol. 11 3). Amsterdam: North-Holland, 1985. v + 230 pp. $38.50/100Df.
    Download  
     
    Export citation  
     
    Bookmark  
  • Models of intuitionistic set theory in subtoposes of nested realizability toposes.Samuele Maschio & Thomas Streicher - 2015 - Annals of Pure and Applied Logic 166 (6):729-739.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Unavoidable sequences in constructive analysis.Joan Rand Moschovakis - 2010 - Mathematical Logic Quarterly 56 (2):205-215.
    Five recursively axiomatizable theories extending Kleene's intuitionistic theory FIM of numbers and numbertheoretic sequences are introduced and shown to be consistent, by a modified relative realizability interpretation which verifies that every sequence classically defined by a Π11 formula is unavoidable and that no sequence can fail to be classically Δ11. The analytical form of Markov's Principle fails under the interpretation. The notion of strongly inadmissible rule of inference is introduced, with examples.
    Download  
     
    Export citation  
     
    Bookmark  
  • Intuitionistic analysis at the end of time.Joan Rand Moschovakis - 2017 - Bulletin of Symbolic Logic 23 (3):279-295.
    Kripke recently suggested viewing the intuitionistic continuum as an expansion in time of a definite classical continuum. We prove the classical consistency of a three-sorted intuitionistic formal system IC, simultaneously extending Kleene’s intuitionistic analysis I and a negative copy C° of the classically correct part of I, with an “end of time” axiom ET asserting that no choice sequence can be guaranteed not to be pointwise equal to a definite sequence. “Not every sequence is pointwise equal to a definite sequence” (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Analyzing realizability by Troelstra's methods.Joan Rand Moschovakis - 2002 - Annals of Pure and Applied Logic 114 (1-3):203-225.
    Realizabilities are powerful tools for establishing consistency and independence results for theories based on intuitionistic logic. Troelstra discovered principles ECT 0 and GC 1 which precisely characterize formal number and function realizability for intuitionistic arithmetic and analysis, respectively. Building on Troelstra's results and using his methods, we introduce the notions of Church domain and domain of continuity in order to demonstrate the optimality of “almost negativity” in ECT 0 and GC 1 ; strengthen “double negation shift” DNS 0 to DNS (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Relative and modified relative realizability.Lars Birkedal & Jaap van Oosten - 2002 - Annals of Pure and Applied Logic 118 (1-2):115-132.
    The classical forms of both modified realizability and relative realizability are naturally described in terms of the Sierpinski topos. The paper puts these two observations together and explains abstractly the existence of the geometric morphisms and logical functors connecting the various toposes at issue. This is done by advancing the theory of triposes over internal partial combinatory algebras and by employing a novel notion of elementary map.
    Download  
     
    Export citation  
     
    Bookmark   4 citations