5
$\begingroup$

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...].

$\endgroup$
  • 1
    $\begingroup$ Will you clarify the question? I see only one sentence with a question mark, but it's phrased as a negative and describes a theory as a model, so that confuses me. $\endgroup$ – Matt F. Dec 22 '16 at 15:06
  • $\begingroup$ thank you Matt, that is helpful, I will edit to clarify. The question is: is my reasoning valid? But I will rephrase more clearly than that. $\endgroup$ – Frank'a Waaldijk Dec 22 '16 at 15:10
  • $\begingroup$ The intermingling of theory and model is part of the question, since within M we cannot of course deduce such things. But then we step up to FIM, and even further, outside of FIM, to deduce the existence of the inductive/continuous recursive realizers. I wonder what parts of BISH fall outside of M, and how important they are? $\endgroup$ – Frank'a Waaldijk Dec 22 '16 at 15:18
  • 1
    $\begingroup$ Thanks for that clarification. Now, if the main question is "does this count as a constructive proof?", why is it relevant if some other BISH theorem cannot be phrased in M? Or is that an independent question? $\endgroup$ – Matt F. Dec 22 '16 at 15:23
  • 1
    $\begingroup$ Coming in late, but the reason that I can't say anything about such questions is that I do not understand what's going on. You are asking whether every theorem of some under-specified system BISH can be phrased in some specified system FIM. What is BISH? I never saw it formalized anywhere, which is needed to make your question precise. Also, the answer is "obviously not" because Bishop uses powersets, quotients, and any number of devices, and you do not have those in FIM. So I think you need to make things more precuse, but once you do, there won't be much of a question left, will there? $\endgroup$ – Andrej Bauer May 14 '18 at 13:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.