A new model for intuitionistic analysis (Q750439)

In the topological model for intuitionistic analysis of \textit{J. R. Moschovakis} [Compos. Math. 26, 261-275 (1973; Zbl 0279.02018)], the schema of relativized dependent choice, monotone bar induction, Kripke's schema, and the restriction of Brouwer's principle for numbers to predicates without free choice-sequence parameters hold. The unrestricted principle of Brouwer does not hold. Therefore the model does not reflect completely intuitionistic analysis. For instance \(\forall x[\forall y((y>0\Rightarrow x>0)\vee (y\leq 0\Rightarrow x>0))\Rightarrow x>0]\) holds intuitionisticly for reals but not in the model. \textit{M. D. Krol'} [Math. Notes 19, 503-504 (1976); translation from Mat. Zametki 19, 859-862 (1976; Zbl 0355.02025)] showed that the unrestricted Brouwer's principle fails in a topological model over T if there is a choice-sequence \(\xi\) and an element t of the topological \(T_ 1\)-space T such that the truth value of \(\exists x {\dot \xi}(x)=0\) is \(T\setminus \{t\}\), \({\dot \xi}\) being the constant for \(\xi\). \textit{M. D. Krol'} overcomes this difficulty in another paper [Z. Math. Logik Grundlagen Math. 24, 427-436 (1978; Zbl 0418.03039)] by restricting the universe of choice-sequences such that it contains no element \(\xi\) such that the truth value \(T\setminus \{t\}\) is associated to \(\exists x {\dot \xi}(x)=0\). In the paper under review the author obtains the unrestricted Brouwer's principle by avoiding truth values like \(T\setminus \{t\}\). In Lect. Notes Math. 753, 302-401 (1979; Zbl 0415.03053), \textit{M. Fourman} and \textit{D. Scott} showed that the complements of the perfect open sets of a sober \(T_ 1\)-space T constitute a complete Heyting algebra, i.e. are suitable as truth values for intuitionistic logic. These complements are not of the kind to be aoivded. The author develops a model of the theory of choice-sequences including restricted dependent choice, monotone bar induction, the schema WC-N of weak continuity for numbers and Kripke's schema by associating complements of the perfect open sets of the Baire space \(^{\omega}\omega\) to the formulas of this theory, and shows that the truth value of every theorem is \(^{\omega}\omega\). Since \textit{W. A. Howard} and \textit{G. Kreisel} [J. Symb. Logic 31, 325-358 (1966; Zbl 0156.008)] showed that the principles mentioned entail the unrestricted Brouwer's principle, the model has the desired properties. It is certainly an interesting and convincing alternative to Krol's model. Analogies and differences of both models are not yet finally investigated.