To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Inductively generated for… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Inductively generated formal topologies

Journal article
Authors Thierry Coquand
G. Sambin
Jan Smith
S. Valentini
Published in Annals of Pure and Applied Logic
Volume 124
Issue 1-3
Pages 71–106
ISSN 0168-0072
Publication year 2003
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Pages 71–106
Language en
Keywords inductive definitions, formal topology, predicative systems
Subject categories Computer and Information Science


Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in a predicative way by an inductive generation and thus their properties can be proved inductively. We show however that some natural complete Heyting algebra cannot be inductively defined.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?