Constructive characterizations of bar subsets (Q866574)

This paper analyzes the notion of bar subsets for Cantor space, Baire space and, more generally, for an inductively generated formal topology. Presented formally, Baire space for instance is given by a generalized inductive definition which describes the covering relation between basic opens, where a basic open is given as a set of finite sequences of integers. This is an early example of generalized inductive definition, introduced by Brouwer (a little earlier example was provided by the definition of Borel sets). An arbitrary covering defines a well-founded tree. In the case of Cantor space, it defines a finite tree, without having to rely on a non-constructive compactness argument (König's lemma). These notions are neatly represented in Intuitionistic Type Theory, and in the case of an inductively generated formal topology can be seen as canonical examples of generalized inductive definitions.