A classical view of the intuitionistic continuum (Q1923572)

The author presents a classical consistency proof of a strong formal system \(S\) extending the FIM [\textit{S. C. Kleene} and \textit{R. E. Vesley}, The foundations of intuitionistic mathematics (1965; Zbl 0133.24601)] formal system for second-order number theory (or ``analysis''), expressed in a language with two kinds of second-order variables, one for lawlike and the other for arbitrary choice sequences. It is further shown that \(S\) can be extended to \(S^+\), whose lawlike part is classical analysis, so that ``the intuitionistic continuum appears as a proper extension of the classical continuum'' (p. 10). The author also provides a final simplification to the definition of lawlessness (relative to a class \(R\) of ``lawlike'' functions) that she had introduced in J. Symb. Logic 52, 68-88 (1987; Zbl 0637.03058) and simplified in J. Symb. Logic 59, 813-829 (1994), and proves the equivalence of the newly defined concept (as a choice sequence \(\alpha\) such that for each predictor (any function that maps sequence numbers to sequence numbers) \(\pi \in R\), there is some \(x \in \omega\) such that \(\pi\) correctly predicts \(\alpha\) at \(x\), i.e. \(\alpha \in \overline \alpha (x)* \pi (\overline \alpha (x)))\) with the older versions. The main contributions of the paper, which assumes familiarity with the formal system and notations of FIM, as well as their place in the existing body of intuitionistic literature, are spelled out in an informal language in the introduction.