More on real algebra in Scott's model
type: Item
instance of: scholarly article
title: More on real algebra in Scott's model
zbMATH Open document ID: 0594.03042
DOI: 10.1016/0168-0072(86)90023-0
author: Philip Scowcroft
published in: Annals of Pure and Applied Logic
publication date: 1986-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F65
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03C90
zbMATH DE Number: 3954907
zbMATH Keywords: intuitionism
zbMATH Keywords: decision procedure
zbMATH Keywords: Dana Scott's topological model for intuitionistic analysis
zbMATH Keywords: primitive-recursive algorithm
MaRDI profile type: Publication
full work available at URL: 0168-0072(86)90023-0
OpenAlex ID: W2017280465
cites work: Q5835082
cites work: Q4079589
cites work: Q5593817
cites work: The real-algebraic structure of Scott's model of intuitionistic analysis
cites work: A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
description: scientific article; zbMATH DE number 3954907