The real-algebraic structure of Scott's model of intuitionistic analysis (Q1059071)

Background. Let \({\mathcal R}\) be Scott's classical model for the intuitionistic continuum whose elements are the continuous functions \(\xi\) : \(T\to {\mathbb{R}}\) (T being a specific topological subspace of the Baire space \(\omega^{\omega})\). The following properties of the model have become part of the folklore: \((1)\quad \{r\in Q:\quad t\in \| \xi <r\| \}\) is an upper cut of the rationals, \((2)\quad \| \xi <\eta \| =\{t\in T:\quad \xi (t)<\eta (t)\}\) and \((3)\quad \| \xi =\eta \| =int\{t\in T:\quad \xi (t)=\eta (t)\}.\) Brouwer's theorem that well defined functions are uniformly continuous on closed bounded intervals is one of the intuitionistic principles that hold in the second order extension of \({\mathcal R}\). Another principle that holds is the following weak form of choice: \[ \forall x\exists !y A(x,y)\to \exists !f \forall x A(x,f(x)), \] where x,y range over \({\mathcal R}\) and f ranges over the subclass of \({\mathcal R}^{{\mathcal R}}\) which serves as the universe of functions. This schema, in combination with Brouwer's theorem, shows that for any sentence \(\forall x\exists !y A(x,y)\) true in \({\mathcal R}\), one can replace y by a Skolem function f continuous in the model. Using another result of Scott one obtains that if A(x,y) is in the language of real- closed fields then the function f can be realized by a continuous \(g: {\mathbb{R}}\to {\mathbb{R}}\). Those observations can then be used to obtain classically true sentences of real-closed fields of the form \(\forall x\exists !y A(x,y)\) which fail in the model (because the y does not vary continuously with x). The problem. The schema \(\forall x\exists y A(x,y)\to \exists f\forall x A(x,y)\) fails in the model. Consequently Brouwer's theorem cannot be used to decide whether y can be made to depend continuously on x for sentences \(\forall x\exists y A(x,y)\) in the language of real-closed fields which are true in the model. The solution. The author gives an algorithm which with every predicate M(x,y) in the language of real-closed fields (\(\vec x=<x_ 1,...,x_ m>\) and \(\vec y=<y_ 1,...,y_ n>)\) effectively associates another predicate G(\(\vec x,\vec y)\) \(\{\) read; (\(\vec x,\vec y)\) is a good M- point\(\}\) such that: if for all continuous functions \(\vec f:^{\omega}\omega \to {\mathbb{R}}^ m\) and \(\vec g:^{\omega}\omega \to {\mathbb{R}}^ n\), \(\| M(\vec f,\vec g)\| =int\{p\in T:\quad M(\vec f(p),\vec g(p))\},\) then: \(\forall \vec x\exists \vec y M(\vec x,\vec y)\) is true in Scott's model, if and only if \(\forall x\exists y G(x,y)\) is true. Applications. Results of Fourman give that there are many, syntactically described classes of formulas obeying the above condition on the M. Furthermore, since G is effectively obtained from M, the decidability of the classical first-order theory of real-closed fields yields a decision procedure for the truth in Scott's model of sentences in a fairly large class. Finally, using Collin's method for the elimination of quantifiers in the classical theory of real-closed fields the author is able to give examples in which the condition of ''good M-point'' is translated into more familiar mathematical terms.