Inductively generated formal topologies.

DOI10.1016/S0168-0072(03)00052-6zbMath1070.03041MaRDI QIDQ1412832

Jan Smith, Giovanni Sambin, Silvio Valentini, Thierry Coquand

Publication date: 25 November 2003

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

Formal topologyInductive definitionsPredicative systems

Mathematics Subject Classification ID

Topological spaces and generalizations (closure spaces, etc.) (54A05) Frames, locales (06D22) Other constructive mathematics (03F65) Ordered topological structures (06F30) Intuitionistic mathematics (03F55)

Related Items (65)

Positivity relations on a locale ⋮ Spatiality and classical logic ⋮ Sublocales in formal topology ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ A Minimalist Foundation at Work ⋮ The Jacobson radical for an inconsistency predicate ⋮ A coverage construction of the reals and the irrationals ⋮ Constructive characterizations of bar subsets ⋮ THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY ⋮ A constructive and functorial embedding of locally compact metric spaces into locales ⋮ Exact approximations to Stone-Čech compactification ⋮ The basic Zariski topology ⋮ Relative formal topology: the binary positivity predicate comes first ⋮ Dynamics in Foundations: What Does It Mean in the Practice of Mathematics? ⋮ Generalising the fan theorem ⋮ On Small Types in Univalent Foundations ⋮ Apartness, sharp elements, and the Scott topology of domains ⋮ Unnamed Item ⋮ The intensional side of algebraic-topological representation theorems ⋮ Locatedness and overt sublocales ⋮ Derived rules for predicative set theory: an application of sheaves ⋮ Topological inductive definitions ⋮ A constructive notion of codimension ⋮ Independence results in formal topology ⋮ Cosheaves and connectedness in formal topology ⋮ Constructive metrisability in point-free topology. ⋮ Some points in formal topology. ⋮ A point-free characterisation of Bishop locally compact metric spaces ⋮ Unnamed Item ⋮ The principle of pointfree continuity ⋮ A constructive Galois connection between closure and interior ⋮ Finitary formal topologies and Stone's representation theorem ⋮ The Zariski spectrum as a formal geometry ⋮ Convergence in formal topology: a unifying notion ⋮ Unnamed Item ⋮ Embedding locales and formal topologies into positive topologies ⋮ Presenting Dcpos and Dcpo Algebras ⋮ Objects: a study in Kantian formal epistemology ⋮ Vagueness, Kant and topology: a study of formal epistemology ⋮ Completeness and cocompleteness of the categories of basic pairs and concrete spaces ⋮ The problem of the formalization of constructive topology ⋮ On some peculiar aspects of the constructive theory of point-free spaces ⋮ About Stone's notion of spectrum ⋮ On the existence of Stone-Čech compactification ⋮ Space of valuations ⋮ The generalised type-theoretic interpretation of constructive set theory ⋮ Formalising Overlap Algebras in Matita ⋮ Equivalents of the finitary non-deterministic inductive definitions ⋮ Every countably presented formal topology is spatial, classically ⋮ Cut elimination for entailment relations ⋮ Predicativity and constructive mathematics ⋮ A topos for algebraic quantum theory ⋮ Unnamed Item ⋮ Aspects of general topology in constructive set theory ⋮ Pretopologies and a uniform presentation of sup-lattices, quantales and frames ⋮ On the collection of points of a formal space ⋮ Heyting-valued interpretations for constructive set theory ⋮ Programming interfaces and basic topology ⋮ Dynamical algebraic structures, pointfree topological spaces and Hilbert's program. (Structures algébriques dynamiques, espaces topologiques sans points et programme de Hilbert) ⋮ Regular universes and formal spaces ⋮ Formal Zariski topology: Positivity and points ⋮ Compactness in locales and in formal topology ⋮ Towards formal Baer criteria ⋮ Higher order functions and Brouwer’s thesis ⋮ Syntax for Semantics: Krull’s Maximal Ideal Theorem

Cites Work

• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Inductive families
• Constructive domain theory as a branch of intuitionistic pointfree topology
• On the formal points of the formal topology of the binary tree
• An extension of the Galois theory of Grothendieck
• An intuitionistic proof of Tychonoff's theorem
• Continuous domains as formal spaces
• Tychonoff's theorem in the framework of formal topologies
• A constructive proof of the Heine-Borel covering theorem for formal reals
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Inductively generated formal topologies.