[FOM] Did Kleene give a constructive proof of Brouwer's axioms?

[Frank Waaldijk]

Harvey Friedman's request for an overview of current intuitionistic
foundations revived the following question, which I have been meaning to
ask for five years. If I'm not mistaken (but I'm no expert on
realizability, which is why I ask the question):

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 E\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 is finite. Constructive proof of the fan theorem FT.

Suppose the BISH-theorem yields: For all \alpha there is \beta [A(\alpha,
\beta)]. Then similarly, FIM-realizability proves that there is a
continuous recursive function f on Baire space, such that FIM proves: for
all \alpha [A(\alpha, f(\alpha). Constructive proof of AC_11.

The question now becomes: what is the difficulty for BISH to accept Bar
Induction and continuous choice 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...].

Best regards,
Frank Waaldijk

http://www.fwaaldijk.nl/mathematics.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20161222/e0cce06e/attachment.html>