Some points in formal topology.

DOI10.1016/S0304-3975(02)00704-1zbMath1044.54001MaRDI QIDQ1427787

Giovanni Sambin

Publication date: 14 March 2004

Published in: Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

03A05: Philosophical and critical aspects of logic and foundations

54A05: Topological spaces and generalizations (closure spaces, etc.)

03F65: Other constructive mathematics

Related Items

Forcing in Proof Theory, A constructive Galois connection between closure and interior, Convergence in formal topology: a unifying notion, Sublocales in formal topology, The generalised type-theoretic interpretation of constructive set theory, Every countably presented formal topology is spatial, classically, On constructing completions, Generalized geometric theories and set-generated classes, A universal Krull-Lindenbaum theorem, Atomicity, coherence of information, and point-free structures, Positivity relations on a locale, Competitive equilibrium with intuitionistic agents, A predicative completion of a uniform space, Almost new pre-apartness from old, A formal proof of the projective Eisenbud-Evans-Storch theorem, Derived rules for predicative set theory: an application of sheaves, An induction principle for consequence in arithmetic universes, Locatedness and overt sublocales, Reflections on function spaces, Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation, Independence results in formal topology, Objects: a study in Kantian formal epistemology, Pre-apartness structures on spaces of functions, A constructive and functorial embedding of locally compact metric spaces into locales, The basic Zariski topology, The Zariski spectrum as a formal geometry, A minimalist two-level foundation for constructive mathematics, A topos for algebraic quantum theory, Constructive metrisability in point-free topology., Unique existence, approximate solutions, and countable choice., The problem of the formalization of constructive topology, Non-deterministic inductive definitions, Spectral schemes as ringed lattices, A textural view of the distinction between uniformities and quasi-uniformities, A constructive notion of codimension, A topologist's view of Chu spaces, Vagueness, Kant and topology: a study of formal epistemology, Quasi-apartness and neighbourhood spaces, Aspects of general topology in constructive set theory, Heyting-valued interpretations for constructive set theory, Programming interfaces and basic topology, Maximal and partial points in formal spaces, Regular universes and formal spaces, Formal Zariski topology: Positivity and points, A Minimalist Foundation at Work, Metric complements of overt closed sets, Relative formal topology: the binary positivity predicate comes first

Cites Work

• Linear logic
• Finitary formal topologies and Stone's representation theorem
• Embedding metric spaces into CPO's
• Constructive domain theory as a branch of intuitionistic pointfree topology
• Inductively generated formal topologies.
• Constructive metrisability in point-free topology.
• The continuum as a formal space
• A cartesian closed category in Martin-Löf's intuitionistic type theory
• Formal spaces and their effective presentations
• Computer science today. Recent trends and developments
• Pretopologies and a uniform presentation of sup-lattices, quantales and frames
• Errett Bishop: Reflections on him and his research
• An intuitionistic proof of Tychonoff's theorem
• Tychonoff's theorem in the framework of formal topologies
• Formal topologies on the set of first-order formulae
• Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
• Pretopologies and completeness proofs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item