Constructive characterizations of bar subsets

DOI10.1016/J.APAL.2006.10.003MaRDI QIDQ866574zbMATH OpenOpenAlexFDO

Publication date 14 February 2007

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2006.10.003

bar induction bar theorem constructive mathematics constructive ordinals formal topology generalized inductive definitions type theory

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Frames, locales (06D22) Topological spaces and generalizations (closure spaces, etc.) (54A05)

Review text

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.

Recommendations

Cites work

Cited in

(10)

This page was built for publication: Constructive characterizations of bar subsets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q866574)