Switch to: References

Citations of:

An intuitionistic proof of Tychonoff's theorem

Thierry Coquand

Journal of Symbolic Logic 57 (1):28-32 (1992)

Add citations

You must login to add citations.

logicism, intuitionism, and formalism - What has become of them?Sten Lindstr©œm, Erik Palmgren, Krister Segerberg & Viggo Stoltenberg-Hansen (eds.) - 2008 - Berlin, Germany: Springer.details The period in the foundations of mathematics that started in 1879 with the publication of Frege's Begriffsschrift and ended in 1931 with Gödel's Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I can reasonably be called the classical period. It saw the development of three major foundational programmes: the logicism of Frege, Russell and Whitehead, the intuitionism of Brouwer, and Hilbert's formalist and proof-theoretic programme. In this period, there were also lively exchanges between the various schools culminating in (...) Download Export citation Bookmark 1 citation
On some peculiar aspects of the constructive theory of point-free spaces.Giovanni Curi - 2010 - Mathematical Logic Quarterly 56 (4):375-387.details This paper presents several independence results concerning the topos-valid and the intuitionistic predicative theory of locales. 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. Download Export citation Bookmark 4 citations
Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.details Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...) Download Export citation Bookmark 44 citations
Compactness in locales and in formal topology.Steven Vickers - 2006 - Annals of Pure and Applied Logic 137 (1-3):413-438.details If a locale is presented by a “flat site”, it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and sufficient condition is derived for compactness of the locale . Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies. A predicative proof of the binary Tychonoff theorem is given, including a characterization of the finite covers of the product by basic opens. The discussion (...) Download Export citation Bookmark 8 citations
Fundamental results for pointfree convex geometry.Yoshihiro Maruyama - 2010 - Annals of Pure and Applied Logic 161 (12):1486-1501.details Inspired by locale theory, we propose “pointfree convex geometry”. We introduce the notion of convexity algebra as a pointfree convexity space. There are two notions of a point for convexity algebra: one is a chain-prime meet-complete filter and the other is a maximal meet-complete filter. In this paper we show the following: the former notion of a point induces a dual equivalence between the category of “spatial” convexity algebras and the category of “sober” convexity spaces as well as a dual (...) Download Export citation Bookmark 2 citations

1