Inductively generated formal topologies.
type: Item
instance of: scholarly article
title: Inductively generated formal topologies.
zbMATH Open document ID: 1070.03041
DOI: 10.1016/S0168-0072(03)00052-6
author: Thierry Coquand
author: Giovanni Sambin
author: Jan Smith
author: Silvio Valentini
published in: Annals of Pure and Applied Logic
publication date: 2003-11-25T00:00:00Z
review text: This paper introduces the very useful concept of inductively generated formal topology (without or with the positivity predicate) in a predicative framework. Formal topology was introduced by P. Martin-Löf and G. Sambin to provide a predicative representation of the concept of locale and open locale [see \textit{G. Sambin}, ``Intuitionistic formal spaces -- a first communication'', in: Mathematical Logic and its Applications, 187--204 (1987; Zbl 0703.03040), and ``Some points in formal topology'', Theor. Comput. Sci. 305, No. 1--3, 347--408 (2003; Zbl 1044.54001)]. The inductive generation in topology is a very important tool since it allows one to reason on topology by induction, that is, by using proof-theoretic methods, and it provides predicative examples of formal topologies. One of these remarkable examples is the inductive formal topology of real numbers. In the paper, the authors start with discussing that the axiomatic definition of formal topology in the cited papers by G. Sambin is not inductive predicatively. At the end they also provide a counterexample of a predicative formal topology that is not inductive by taking the Dedekind-MacNeille cover on the Boolean set. Another difference between generic formal topologies and inductive ones is that, while inductively generated formal topologies are easily seen to be closed predicatively under suitable constructions, such as the closure under binary products, for formal topology it is still not known (predicatively!).
Mathematics Subject Classification ID: 03F65
Mathematics Subject Classification ID: 06D22
Mathematics Subject Classification ID: 54A05
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 06F30
zbMATH DE Number: 2009283
zbMATH Keywords: Inductive definitions
zbMATH Keywords: Formal topology
zbMATH Keywords: Predicative systems
MaRDI profile type: Publication
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: A constructive proof of the Heine-Borel covering theorem for formal reals
cites work: An intuitionistic proof of Tychonoff's theorem
cites work: Q3481700
cites work: Inductive families
cites work: Q4150804
cites work: Q3322099
cites work: Q4225149
cites work: Q3965241
cites work: Q3322276
cites work: An extension of the Galois theory of Grothendieck
cites work: Q4944857
cites work: Continuous domains as formal spaces
cites work: Tychonoff's theorem in the framework of formal topologies
cites work: Q3999860
cites work: Q3481701
cites work: Q3832536
cites work: Q4247310
cites work: Constructive domain theory as a branch of intuitionistic pointfree topology
cites work: On the formal points of the formal topology of the binary tree
description: scientific article; zbMATH DE number 2009283