A new model for intuitionistic analysis
type: Item
instance of: scholarly article
title: A new model for intuitionistic analysis
zbMATH Open document ID: 0714.03051
DOI: 10.1016/0168-0072(90)90067-C
author: Philip Scowcroft
published in: Annals of Pure and Applied Logic
publication date: 1990-01-01T00:00:00Z
review text: 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 numbe…
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03C90
zbMATH DE Number: 4174926
zbMATH Keywords: topological model
zbMATH Keywords: intuitionistic analysis
zbMATH Keywords: unrestricted Brouwer's principle
zbMATH Keywords: model of the theory of choice-sequences
zbMATH Keywords: restricted dependent choice
zbMATH Keywords: monotone bar induction
zbMATH Keywords: weak continuity for numbers
zbMATH Keywords: Kripke's schema
reviewed by: Helmut Pfeiffer
MaRDI profile type: Publication
cites work: The use of Kripke's schema as a reduction principle
cites work: An interpretation of intuitionistic analysis
cites work: How to glue analysis models
cites work: Glueing of analysis models in an intuitionistic setting
cites work: Q3863865
cites work: Q3050433
cites work: Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
cites work: Q5343325
cites work: The topological models of intuitionistic analysis. One counterexample
cites work: Q4163218
cites work: Q4180345
cites work: A Topological Model for Intuitionistic Analysis with Kripke's Scheme
cites work: Q4404863
cites work: Q5593817
cites work: Q5614645
cites work: The real-algebraic structure of Scott's model of intuitionistic analysis
cites work: More on real algebra in Scott's model
Wikidata QID: Q128017591
Recommended article: Topological forcing semantics with settling
Recommended article: Undecidability of the real-algebraic structure of models of intuitionistic elementary analysis
Recommended article: Q4764119
Recommended article: A model of intuitionistic analysis in which \(\varnothing\)-definable discrete sets are subcountable
Recommended article: Undecidability of the Real-Algebraic Structure of Scott's Model
Recommended article: Freyd’s models for the independence of the axiom of choice
Recommended article: La logique des topos
Recommended article: Q4532197
description: scientific article; zbMATH DE number 4174926