The real-algebraic structure of Scott's model of intuitionistic analysis
type: Item
instance of: scholarly article
title: The real-algebraic structure of Scott's model of intuitionistic analysis
zbMATH Open document ID: 0566.03034
DOI: 10.1016/0168-0072(84)90030-7
author: Philip Scowcroft
published in: Annals of Pure and Applied Logic
publication date: 1984-01-01T00:00:00Z
review text: 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 wit…
Mathematics Subject Classification ID: 03F65
zbMATH DE Number: 3902645
zbMATH Keywords: intuitionistic continuum
zbMATH Keywords: continuous functions
zbMATH Keywords: real-closed fields
zbMATH Keywords: good M-point
MaRDI profile type: Publication
full work available at URL: 0168-0072(84)90030-7
OpenAlex ID: W2056848940
cites work: Principles of continuous choice and continuity of functions in formal systems for constructive mathematics
cites work: Q5573965
cites work: Q3901492
cites work: Q4079605
cites work: Q3963137
cites work: Q5596338
cites work: The first order properties of products of algebraic systems
cites work: Q3863865
cites work: Q5835082
cites work: Q3855166
cites work: Proofs of non-deducibility in intuitionistic functional calculus
cites work: Q5734410
cites work: Q5593817
cites work: Q5614645
cites work: Elementary intuitionistic theories
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
description: scientific article; zbMATH DE number 3902645