The Disjunction and Numerical Existence Properties for Intuitionistic Analysis
Philip Scowcroft · Birkhäuser Boston eBooks · 1993
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).