Realizing Brouwer's sequences (Q1923574)

In this paper, the author, who assumes familiarity with FIM [\textit{S. C. Kleene} and the author, The foundations of intuitionistic mathematics (1965; Zbl 0133.24601)], puts forward a new interpretation, that generalizes to higher-type Kleene's functional realizability (FIM). Three formal systems, \(S_1\), \(S_2\), and \(S^*\), each extending the previous one, are introduced, all expressed in an extension \(L^*\) of the language \(L\) of FIM, that contains a constant functor (function of one variable) primitive the name for a particular ``lawless'' sequence \(\omega\). This novelty allows the expression in \(L^*\) of the property of a choice sequence to be lawless by means of the formula \[ LS(\alpha): \exists z \biggl(\text{Seq} (z) \wedge \alpha \in z \wedge \forall i \bigl(i \geq lh(z) \to \alpha (i) = \omega (i) \bigr) \biggr) . \] \((U,R)\)-realizability, with \(U\) standing for Kleene's ``universal spread'' of FIM, and with \(R\) standing for the set of total recursive functions, is introduced to code continuous functions, and it is shown that all theorems in \(S^*\) (whence all in \(S_2\) and \(S_1)\) are \((U,R)\)-realizable. The only nonconstructive argument is used in the proof that the only axiom scheme that was added to \(S_2\) to get \(S^*\), namely CONT!, is \((U,R)\)-realizable. \(S_2\) (in fact, already \(S_1\) together with one of the principles for lawless sequences LS4) is an exclusively intuitionistic formal system, for it becomes inconsistent once \(\neg \neg A\to A\) is added to it. The lawless axioms for \(S_2\) are sufficiently strong to reject even the Ščedrov-Vesley [\textit{A. Ščedrov} and the author, Arch. Math. Logik Grundlagenforsch. 23, 153-160 (1983; Zbl 0533.03033)] weak version of Markov's principle.