This page is about my research activity in mathematical logic.
-
Constructive strong regularity and the extension property of a compactification.
Annals of Pure and Applied Logic, to appear.
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.
-
Abstract inductive and co-inductive definitions.
Journal of Symbolic Logic, 83, No. 2 (2018), pp. 598-616.
In [G. Curi, On Tarski's fixed point theorem. Proc. Amer. Math. Soc., 143
(2015), pp. 4439-4455], a notion of abstract inductive definition is formulated to extend
Aczel's theory of inductive definitions to the setting of complete lattices. In this paper,
after discussing a further extension of the theory to structures of much larger size than
complete lattices, as the class of all sets or the class of ordinals, a similar generalization is
carried out for the theory of co-inductive definitions on a set. As a corollary, a constructive
version of the general form of Tarski's fixed point theorem is derived.
- On Tarski's fixed point theorem.
Proc. Amer. Math. Soc., 143 (2015), pp. 4439-4455.
A concept of abstract inductive definition on a complete lattice is formulated and studied.
As an application, a constructive version of Tarski's fixed point theorem is obtained.
- (With M. Rathjen) Formal Baire space in
constructive set theory.
In: Logic, Construction,
Computation. Papers in honor of Helmut Schwichtenberg's 70th
birthday. Ontos Verlag, Frankfurt (2012), pp. 123-135.
It is shown that the constructive set theory CZF does not prove that the
covering system for formal Baire space defines a formal space. The
same holds for CZF augmented by constructively acceptable choice
principles. Formal Baire space gives thus an example of an imaginary
locale (in the sense of [G. Curi, "Topological inductive
definitions", APAL, 163 (2012), pp. 1471-1483.]) that is not a formal space in
CZF.
A corollary of this result is that CZF does not prove that the Brouwer
(or constructive) Ordinals form a set. A further consequence is that
the category IFSp of inductively generated formal spaces, which is
complete in CZF + REA, is not complete in CZF alone, according at
least to the received constructions.
- Topological inductive definitions.
Finalists' articles of the Kurt Gödel Centenary Research Prize Fellowships 2010.
Annals of Pure and Applied Logic, 163 (2012), pp. 1471-1483.
In intuitionistic generalized predicative systems as constructive set theory, or constructive type theory,
two categories have been proposed to play the role of the category of locales: the category FSp of formal spaces, and its full subcategory IFSp of inductively generated formal spaces.
Considered in impredicative systems as the intuitionistic set theory IZF, FSp and IFSp are both equivalent to the category of locales. In the mentioned predicative systems, however, FSp fails to be closed under basic constructions such as that of finite products; on the other hand, IFSp is complete (in particular has all products), but does not contain several naturally occurring classes of formal spaces, and completeness only holds under the assumption of strong principles for the existence of inductively defined sets.
In this paper, working in the context of constructive set theory, the category ImLoc of imaginary locales is introduced. ImLoc is complete already over weak formulations of constructive set theory, contains FSp and IFSp as full subcategories, and, as FSp and IFSp, is equivalent to the category of locales in IZF.
The notion of imaginary locale can in particular be used to systematically develop the theory of locales in systems that are proof-theoretically considerably weaker than those usually adopted to this aim.
Applications of the concept of imaginary locale to a proof of a point-free version of Tychonoff embedding theorem, and to set-representation theorems, are then presented.
- On the existence of Stone-Čech compactification.
Journal of Symbolic Logic, 75, No. 4 (Dec. 2010), pp. 1137-1146.
Two well-known achievements of locale theory are the intuitionistic and choice-free constructions of (point-free versions of) Stone-Čech compactification and of Gleason covers (see e.g. [P. T. Johnstone, "The points of pointless topology", Bull. Am. Math. Soc. 8 1, 41--53 (1983)]). Here, 'intuitionistic' means 'valid in any topos', i.e., derivable in higher-order Heyting arithmetic HHA. In [4] we proved that, albeit intuitionistic in this sense, the existence of the Gleason cover of a compact regular locale cannot be derived in constructive set theory CZF and type theory CTT, as in several, even impredicative, extensions of these systems.
In this paper we show that, in its generality, the localic Stone-Čech compactification theorem fails to hold constructively in the same sense. By contrast with Gleason covers, however, Stone-Čech compactification does exist for a wide class of locales: in [7] a necessary and sufficient condition was found for the Stone-Čech compactification of a locale X to exist in CTT, and in the formal system CZF+uREA+DC. The collection of locales satisfying this condition includes the locally compact locales, in particular the positive integers with discrete topology, and the point-free real line. In this paper we give a (self-contained) proof that, on the other hand, the existence of Stone-Čech compactification of a non-degenerate Boolean locale X is independent of the axioms of CZF (in a topos, the Stone-Čech compactification of a Boolean locale X is given by the locale of ideals of X).
This fact follows by a result of independent interest, namely the proof that the class Hom(X,Y) of continuous mappings from a compact regular locale X to a regular and set-presented locale Y is a set in CZF. In particular this result implies that the full subcategory used to represent constructively the category of compact Hausdorff spaces, i.e. the category of compact and regular locales, is locally small in CZF. A further consequence of this result is that the above-mentioned characterization of the locales of which the Stone-Čech compactification exists continues to hold over the standard system CZF plus REA, thus in particular without any recourse to a choice principle.
- On some peculiar aspects of the constructive theory of point-free spaces.
Mathematical Logic Quarterly, 56, No. 4, 1 (2010) pp. 375-387.
This paper presents several independence results concerning the topos-valid and the intuitionistic (generalised) predicative theory of locales/formal spaces. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined. The main results concern the following two aspects of the theory of locales:
i. considered in any topos, the category of locales is complete and cocomplete. By contrast, the existence of binary products of arbitrary formal spaces already seems to require the use of strongly impredicative principles, that are not available in generalised predicative settings such as constructive set theory CZF, or type theory CTT. In particular to remedy this deficiency, the concept of inductively generated formal space was introduced: inductively generated formal spaces define a full subcategory IFSp of the category of formal spaces, in which limits and colimits do exist. In this paper we show that, albeit satisfactory in this sense, the restriction to the category IFSp is a severe one, as several classes of formal spaces of interest are thus ruled out;
ii. in contrast with what happens with topological spaces, the Gleason cover of a compact regular formal space X - i.e., a minimal surjection γX→X, with γX compact, regular, and extremally disconnected - can be constructed in any topos (Johnstone). In this paper we show that CZF, CTT cannot prove that a non-trivial formal space is compact and extremally disconnected, so that for no non-trivial compact regular formal space X, the Gleason cover of X can be constructed in these systems.
- (With P. Aczel) On the T1 axiom and other separation properties in constructive point-free and point-set topology.
Annals of Pure and Applied Logic, 161
(2010) pp. 560-569.
In this note a T1 formal space (T1 set generated locale) is a formal space whose points are closed as subspaces. Any regular formal space is T1. We introduce the more general notion of T1* formal space, and prove that the class of points of a weakly set-presentable T1* formal space is a set in the constructive set theory CZF. The same also holds in constructive type theory. We then formulate separation properties Ti* for (class-sized) constructive topological spaces (ct-spaces), strengthening separation properties discussed elsewhere. Finally we relate the Ti* properties for ct-spaces with corresponding properties of formal spaces.
-
Remarks on the Stone-Čech and Alexandroff compactifications of locales.
Journal of Pure and Applied Algebra, 212, 5 (2008) pp. 1134-1144.
Generalizing a classical result of Smirnov for topological spaces, B. Banaschewski proved that there is an order isomorphism between compactifications of a frame (locale) and the strong inclusions on that frame. Considering, more generally, strong inclusions on distributive pseudocomplemented lattices allows new aspects of locale (and space) compactifications to emerge. Given a subpseudocomplemented lattice P of a frame L and a strong inclusion on P, the 'round ideal completion' of P is a compact regular frame enjoying a unique factorization property for certain continuous mappings from L into compact regular locales. Every compactification can be obtained in this way, from a subpseudocomplemented lattice P and a strong inclusion on P, both inductively defined. It follows that every compactification satisfies a natural extension property for certain classes of continuous mappings. This property reduces to the usual one of Stone-Čech compactification when the chosen subpseudocomplemented lattice P of L and strong inclusion on P are sufficiently large. One need not take the whole frame (Banaschewski-Mulvey's construction of Stone-Čech compactification). An inductively constructed subpseudocomplemented lattice K of L suffices. Remarkably, it suffices for all compactifications: every compactification of L can be obtained as the frame of round ideals over K for an inductively defined strong inclusion on K. Alexandroff compactification is also re-obtained in this vein, as the completion of the least inductively defined subpseudocomplemented lattice extending a base of L, endowed with the least (inductively defined) strong inclusion containing the way-below relation.
-
Exact approximations to Stone-Čech compactification.
Annals of Pure and Applied Logic, 146, 2-3 (2007) pp. 103-123.
Many fundamental results, as the theorems of Tychonoff and Hahn-Banach, are equivalent (in classical ZF) to some form of choice principle. A well-known advantage of replacing topological spaces with locales, or formal spaces, is that topos-valid (choice-free) versions of these results become provable. Generally speaking, this remains true even if one replaces topoi with constructive (intuitionistic and predicative) settings such as Type Theory or Constructive Set Theory. This paper deals with the rather extreme case of Stone-Čech compactification ß. The formal spaces/ locales X for which ß(X) exists constructively are characterized. This involves discussing the 'size' of hom-sets in the category Loc of locales/formal spaces (constructively Loc is not locally small). In particular, the full subcategory of locally compact regular locales is proved to be locally small. It is also shown how Stone-Čech compactification can itself be used to prove that certain hom-sets are small.
-
On the collection of points of a formal space.
Annals of Pure and Applied Logic 137, 1-3, 2006, pp. 126-146.
(Circulated as a draft since June 2001, with the title "Compact Hausdorff spaces are Data Types").
The concept of set available to constructive mathematics is considerably more restrictive than the classical or topos-theoretic ones. Many important constructions yield classes that in the mathematical practice are implicitly proved small by relying on strong comprehension principles. These classes may be hard to be presented as sets constructively, and often they can not. In this paper (every collection of objects that can be regarded as) the class of points of a locally compact regular (=locally compact Hausdorff) formal space is proved to form a set in every foundation adequate to constructive mathematics in the sense of Feferman (in particular therefore in type theory and constructive set theory). The skeleton of a constructive theory of uniform locales/ formal spaces, based on the notion of elementary diameter, is also introduced and used to derive generalizations and a more perspicuous version of the mentioned set-representation.
- Constructive metrisability in point-free topology.
Theoretical Computer Science 305 (2003), no. 1-3, 85-109.
Previous work on locales (mainly by Isbell, Pultr, and Banaschewski) has treated metrisability only classically. This paper presents a constructive theory of metrisability based on the notion of elementary diameter. Beside the constructive features, the resulting concept of metric locale (metric formal space) is easier to handle with respect to the existing ones. In particular, metric formal spaces in the sense of this paper may be regarded as providing presentations for Pultr's metric locales. By exploiting the notion of elementary diameter one may formulate quantitatively - in the form of the 'measurably inside' relation - the idea that a given neighbourhood is 'finer than', or is a 'better approximation than', another neighbourhood. This relation is then used to express metrisability. The way-below, well and really inside relations, used in the point-free formulation of local compactness, regularity and complete regularity, respectively, may similarly be regarded as expressions of a concept of 'finer than'. These intuitive similarities can be made formal: in particular, a constructive proof of Urysohn metrization theorem is obtained by constructing a diameter that 'transforms' the really inside relation into the measurably inside relation. This machinery is finally applied to prove that the class of points of a locally compact metrisable locale is a set constructively.
- The points of (locally) compact regular formal topologies.
In: Reuniting the Antipodes: Constructive and Nonstandard Views of the Continuum.
Synthese Library (Vol. 306, pp.39-54). Kluwer Academic Publishers, Dordrecht etc., 2001. Eds. U. Berger, H. Osswald and P. Schuster.
The points of a compact regular locale L are characterized as the maximal regular subsets of any given fixed base of L (i.e. of any formal space representing L). The concept of maximality involved is formulated elementary and yields a first-order characterization of the points of such a locale. A similar result also holds for locally compact regular L. An application of these characterizations is presented in "On the collection of points of a formal space".