Constructive strong regularity and the extension property of a compactification

In contexts in which the principle of dependent choice may not be available, as toposes or Constructive Set Theory, standard locale theoretic results related to complete regularity may fail to hold. To resolve this difficulty, B. Banaschewski and A. Pultr introduced strongly regular locales. Unfortunately, Banaschewski and Pultr's notion relies on non-constructive set existence principles that hinder its use in Constructive Set Theory. In this article, a fully constructive formulation of strong regularity for locales is introduced by replacing non-constructive set existence with coinductive set definitions, and exploiting the Relation Reflection Scheme. As an application, every strongly regular locale L is proved to have a compact regular compactification. The construction of this compactification is then used to derive the main result of this article: a characterization of locale compactifications (and thus, classically, of the compactifications of a space) in terms of their ability of extending continuous functions with compact regular codomains. Finally, an open problem related to the existence of the compact regular reflection of a locale is presented.     

A note on Bar Induction in Constructive Set Theory

Bar Induction occupies a central place in Brouwerian mathematics. This note is concerned with the strength of Bar Induction on the basis of Constructive Zermelo‐Fraenkel Set Theory, CZF. It is shown that CZF augmented by decidable Bar Induction proves the 1‐consistency of CZF. This answers a question of P. Aczel who used Bar Induction to give a proof of the Lusin Separation Theorem in the constructive set theory CZF. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The Vector Space Kinna‐Wagner Principle is Equivalent to the Axiom of Choice

We show that the axiom of choice AC is equivalent to the Vector Space Kinna‐Wagner Principle, i.e., the assertion: “For every family 𝒱= {V_i : i ∈ k} of non trivial vector spaces there is a family ℱ = {F_i : i ∈ k} such that for each i ∈ k, F_i is a non empty independent subset of V_i”. We also show that the statement “every vector space over ℚ has a basis” implies that every infinite well ordered set of pairs has an infinite subset with a choice set, a fact which is known not to be a consequence of the axiom of multiple choice MC.