This paper introduces an extension 𝒜 of Kleene’s axiomatization
of Brouwer’s intuitionistic analysis, in which the classical arithmetical
and analytical hierarchies are faithfully represented as hierarchies of
the domains of continuity. A domain of continuity is a
relation R(α) on Baire space with the property that every
constructive partial functional defined on {α: R(α)} is
continuous there. The domains of continuity for 𝒜 coincide
with the stable relations (those equivalent in 𝒜
to their double negations), while every relation R(α) is
equivalent in 𝒜 to ∃ β A(α,β) for some
stable A(α,β) (which belongs to the classical analytical
hierarchy).
¶
The logic of 𝒜 is intuitionistic. The axioms of 𝒜
include countable comprehension, bar induction, Troelstra’s generalized
continuous choice, primitive recursive Markov’s Principle and a
classical axiom of dependent choices proposed by Krauss. Constructive
dependent choices, and constructive and classical countable choice, are
theorems. 𝒜 is maximal with respect to classical Kleene
function realizability, which establishes its consistency. The usual
disjunction and (recursive) existence properties ensure that 𝒜
preserves the constructive sense of “or” and “there exists.”