Harvey Friedman's request on the FoM-forum for an overview of current intuitionistic foundations revived the following question, which I have been meaning to ask for five years. (I'm no expert on realizability, which is why I ask the question, here and on FoM).
Is the following reasoning valid, and does it constitute (some form of) constructive proof of Brouwer's Bar Induction and Continuous Choice axioms?:
In 1969, Kleene proved that the formal system FIM = M +BI_D + AC_11 is equiconsistent with its classically valid subsystem M + BI_D. Here M is a two-sorted model containing natural-number and Baire-space-sequence variables, countable choice and function comprehension, BI_D denotes decidable bar induction (classically valid), and AC_11 is Brouwer's continuous choice axiom for Baire space (classically false). Number variables are usually indicated with $x,y,...$, sequence variables with $\alpha,\beta,...$.
Kleene proved more: if FIM proves an existential theorem $\exists\alpha [P(\alpha)]$, then we can constructively find a recursive sequence $\beta$ such that FIM proves $P(\beta)$.
These results have usually been cited to show that Brouwer's axioms are far less mystical than many people working in classical mathematics believe(d).
But I have been pondering the opposite direction. Does not M give a rather faithful model for BISH? Therefore, if we take a BISH theorem, it should be provable in M (excepting Gödelian stuff of course).
Suppose an M-provable BISH-theorem yields: there is a certain bar on Baire space. Then this theorem holds in FIM as well, meaning we can actually find an inductive recursive bar satisfying the theorem. In other words, if we prove in M that there is a bar on Cantor space, then FIM-realizability proves that this bar contains a finite bar. Constructive proof of the fan theorem FT.
Suppose the BISH-theorem yields: $\forall\alpha\exists\beta [A(\alpha, \beta)]$. Then similarly, FIM-realizability proves that there is a continuous recursive function $f$ on Baire space, such that FIM proves: $\forall\alpha[A(\alpha,f(\alpha))]$. Constructive proof of AC_11.
Perhaps I'm mistaken, and someone can give a BISH theorem which cannot be phrased in M. Or perhaps I'm mistaken in my interpretation of Kleene's results.
All comments welcome, and sorry if I got it wrong [still: in that case correcting me will perhaps benefit many others as well...].
