The Disjunction and Numerical Existence Properties for Intuitionistic Analysis
- 165 Downloads
Let ℐ be the system of analysis studied in . ℐ’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.
- van Dalen, D. , The use of Kripke’s schema as a reduction principle. JSL 42, 238–240.Google Scholar
- Kleene, S.C. , Formalized recursive Junctionals and formalized realizability. Memoirs of the AMS, No. 89. American Mathematical Society, Providence.Google Scholar