The Disjunction and Numerical Existence Properties for Intuitionistic Analysis

  • Philip Scowcroft
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 12)


Let ℐ be the system of analysis studied in [13]. ℐ’s language is two-sorted — with number variables x, y, z, … and choice-sequence variables α, β, γ, … — and has a constant for zero, symbols for certain primitive-recursive functions, an identity predicate in the number sort, and notation for γ-abstraction. Starting from two-sorted intuitionistic logic, ℐ adds axioms for Heyting arithmetic (HA), recursion equations for the primitive-recursive functions, certain “postulates concerning functions” [7, p. 14], and four axiom schemata described below: relativized dependent choice (RDC), monotone bar induction (BI M), weak continuity for numbers (WC-N), and Kripke’s schema (KS).


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    van Dalen, D. [1977], The use of Kripke’s schema as a reduction principle. JSL 42, 238–240.Google Scholar
  2. [2]
    Grayson, R.J. [1979], Heyting-valued models for intuitionistic set theory. In: M.P. Fourman, C.J. Mulvey, D.S. Scott, eds., Applications of Sheaves. Lecture Notes in Mathematics 753, 402–414. Springer-Verlag, Berlin.CrossRefGoogle Scholar
  3. [3]
    Grayson, R.J. [1982], Constructive well-orderings. Z. math. Logik Grundlag. Math. 28, 495–504.MathSciNetzbMATHCrossRefGoogle Scholar
  4. [4]
    Kleene, S.C. [1952], Introduction to Metamathematics. Van Nostrand Co., New York.zbMATHGoogle Scholar
  5. [5]
    Kleene, S.C. [1962], Disjunction and existence under implication in elementary intuitionistic formalisms. JSL 27, 11–18.MathSciNetGoogle Scholar
  6. [6]
    Kleene, S.C. [1969], Formalized recursive Junctionals and formalized realizability. Memoirs of the AMS, No. 89. American Mathematical Society, Providence.Google Scholar
  7. [7]
    Kleene, S.C. and R.E. Vesley [1965], The Foundations of Intuitionistic Mathematics. North-Holland Publishing Co., Amsterdam.zbMATHGoogle Scholar
  8. [8]
    Krol, M.D. [1977], Disjunctive and existential properties of intuitionistic analysis with Kripke’s scheme. Soviet Math. Dokl. 18, 755–758.zbMATHGoogle Scholar
  9. [9]
    Krol, M.D. [1978], Distinct variants of Kripke’s schema in intuitionistic analysis. Soviet Math. Dokl. 19, 474–477.zbMATHGoogle Scholar
  10. [10]
    Krol, M.D. [1978], A topological model for intuitionistic analysis with Kripke’s scheme. Z. math. Logik Grundlag. Math. 24, 427–436.MathSciNetzbMATHCrossRefGoogle Scholar
  11. [11]
    Moschovakis, J.R. [1967], Disjunction and existence in formalized intuitionistic analysis. In: J.N. Crossley, ed., Sets, models, and recursion theory. North-Holland Publishing Co., Amsterdam, 309–331.CrossRefGoogle Scholar
  12. [12]
    Scedrov, A. [1981], Consistency and independence results in intuitionistic set theory. In: F. Richman, ed., Constructive Mathematics. Lecture Notes in Mathematics 873, 54–86. Springer-Verlag, Berlin.CrossRefGoogle Scholar
  13. [13]
    Scowcroft, P. [1990], A new model for intuitionistic analysis. Ann. Pure Appl. Logic 47, 145–165.MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 1993

Authors and Affiliations

  • Philip Scowcroft
    • 1
  1. 1.Department of MathematicsWesleyan UniversityMiddletownUSA

Personalised recommendations