 While \(\mathbf{HA}\) is a proper part of classical arithmetic, the intuitionistic attitude toward mathematical objects results in a theory of real numbers (cf. sections 3.4–3.7 of the entry on  intuitionism in the philosophy of mathematics)  diverging from the classical. Kleene’s function-realizability interpretation, developed to prove the consistency of his formalization \(\mathbf{FIM}\) of the intuitionistic theory of sequences (“intuitionistic analysis”), changes the interpretation of arithmetical formulas; for example, \(\neg \neg \forall x (A(x) \vee \neg A(x))\) is function-realizable for every arithmetical formula \(A(x).\) In the language of analysis, Markov’s Principle and the negative translation of the countable axiom of choice are among the many non-intuitionistic principles which are function-realizable (by classical arguments) and hence consistent with \(\mathbf{FIM};\) cf. Kleene [1965], Vesley [1972] and Moschovakis [2003].