Some points in formal topology.

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

Publication date: 14 March 2004

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

Full work available at URL: https://doi.org/10.1016/s0304-3975(02)00704-1

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Topological spaces and generalizations (closure spaces, etc.) (54A05) Other constructive mathematics (03F65)

Related Items (68)

A universal Krull-Lindenbaum theorem ⋮ Atomicity, coherence of information, and point-free structures ⋮ Positivity relations on a locale ⋮ Metric complements of overt closed sets ⋮ Sublocales in formal topology ⋮ Spectral schemes as ringed lattices ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ A Minimalist Foundation at Work ⋮ Pre-apartness structures on spaces of functions ⋮ The Jacobson radical for an inconsistency predicate ⋮ THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY ⋮ A constructive and functorial embedding of locally compact metric spaces into locales ⋮ The basic Zariski topology ⋮ Relative formal topology: the binary positivity predicate comes first ⋮ Non-deterministic inductive definitions ⋮ Eliminating disjunctions by disjunction elimination ⋮ Competitive equilibrium with intuitionistic agents ⋮ Radical theory of Scott-open filters ⋮ On Small Types in Univalent Foundations ⋮ A predicative completion of a uniform space ⋮ Almost new pre-apartness from old ⋮ A textural view of the distinction between uniformities and quasi-uniformities ⋮ Unnamed Item ⋮ Locatedness and overt sublocales ⋮ 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 ⋮ A constructive notion of codimension ⋮ Reflections on function spaces ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ Independence results in formal topology ⋮ Constructive metrisability in point-free topology. ⋮ Unique existence, approximate solutions, and countable choice. ⋮ A point-free characterisation of Bishop locally compact metric spaces ⋮ Continuity of Motion in Whitehead’s Geometrical Space ⋮ The principle of pointfree continuity ⋮ A constructive Galois connection between closure and interior ⋮ THE LOGIC AND TOPOLOGY OF KANT’S TEMPORAL CONTINUUM ⋮ Point-Free Spectra of Linear Spreads ⋮ Factorizing the \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction through positive topologies ⋮ The Zariski spectrum as a formal geometry ⋮ Convergence in formal topology: a unifying notion ⋮ A topologist's view of Chu spaces ⋮ On constructing completions ⋮ Embedding locales and formal topologies into positive topologies ⋮ Objects: a study in Kantian formal epistemology ⋮ Vagueness, Kant and topology: a study of formal epistemology ⋮ Generalized geometric theories and set-generated classes ⋮ The problem of the formalization of constructive topology ⋮ Unnamed Item ⋮ Forcing in Proof Theory ⋮ Quasi-apartness and neighbourhood spaces ⋮ The generalised type-theoretic interpretation of constructive set theory ⋮ Every countably presented formal topology is spatial, classically ⋮ Cut elimination for entailment relations ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Topology as Faithful Communication Through Relations ⋮ The Hahn-Banach theorem by disjunction elimination ⋮ Ordering groups constructively ⋮ A topos for algebraic quantum theory ⋮ 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 ⋮ Towards formal Baer criteria ⋮ Syntax for Semantics: Krull’s Maximal Ideal Theorem

Cites Work

This page was built for publication: Some points in formal topology.