More on real algebra in Scott's model (Q1076670): Difference between revisions

The present paper extends previous results of its author [ibid. 27, 275- 308 (1984; Zbl 0566.03034)] concerning real algebra inside Dana Scott's topological model for intuitionistic analysis. From real-algebraic predicates \(M(x_ 1,...,x_ m)\) and \(N(x_ 1,...,x_ m),y_ 1,...,y_ n)\), a primitive-recursive algorithm produces another such predicate G(\(\vec x,\vec y)\) with the property: if \(\| M(\vec f)\| =int\{p\in^{\omega}\omega:\) M(\(\vec f(p))\}\), \(\| N(f,g)\| =int\{p\in^{\omega}\omega:\) N(f(p),g(p))\(\}\) for all continuous \(\vec f:^{\omega}\omega \to {\mathbb{R}}^ m\) and \(\vec g:^{\omega}\omega \to {\mathbb{R}}^ n\), then \(\forall \vec x(M(\vec x)\to \exists \vec yN(\vec x,\vec y))\) holds in Scott's model just in case \(\forall \vec x(M(\vec x)\to \exists \vec yG(\vec x,\vec y))\) is classically true. The latter statement, classically stronger than the former, demands that one be able to choose \(\vec y's\), obeying N(\(\vec x,\vec y)\), which vary continuously with \(\vec x's\) obeying M: continuously, in the sense in which the roots of a polynomial vary continuously with its coefficients. Extensions of the basic result, and some discussion of specific examples to which the theorem applies, follow the description and justification of the algorithm. Since the writing of this paper its author has forged a strong link between the theory of Scott's model and constructive mathematics. In brief: sentences \(\forall \vec x(M(\vec x)\to \exists \vec yN(\vec x,\vec y))\) of the type mentioned above are provable with Bishop-style methods if true in Scott's model, and refutable in intuitionistic analysis otherwise. The extent to which Stengle's theorems are constructively valid - a problem mentioned briefly at the end of the present paper - has also been determined.