Formal Baire Space in Constructive Set Theory
Giovanni Curi, Michael Rathjen · 2012
Constructive topology is generally based on the notion of locale, or formal space (see [10, 9, 8], and [22, pg. 378], for an explanation of why this is the case). Algebraically, locales are particular kinds of lattices that, like other familiar algebraic structures, can be presented using the method of generators and relations, cf. e.g. [23]. Equivalently, they may be described using covering systems [9, 13]. Set-theoretically, ‘generators and relations’ and covering systems can be regarded as inductive definitions. Classical or intuitionistic fully impredicative systems, such as intuitionistic Zermelo-Fraenkel set theory, IZF [2], or the intuitionistic theory of a topos [11], are sufficiently strong to ensure that such inductive definitions do give rise to a locale or formal space. This continues to hold in (generalized) predicative systems as for example the constructive set theory CZF augmented by the weak regular extension axiom wREA (where the covering systems give rise to so-called inductively generated formal spaces, [1]). However, albeit being much weaker than classical set theory ZF, the system CZF + wREA is considerably stronger than CZF. As it turns out, CZF + wREA is a subsystem of classical set theory ZF plus the axiom of choice AC, but not of ZF alone (cf. [17]). Naturally, this lends itself to the question of what can be proved in the absence of wREA. In this note we show that working in CZF alone, a covering system may fail to define a formal space already in a familiar case. It is easy to see that CZF can prove that, e.g., the covering systems used to present formal Cantor space C, and the formal real line R, do define formal spaces; this is essentially because the associated inductive definition is a finitary one for C, and can be