Inductively generated formal topologies.
This paper introduces the very useful concept of inductively generated formal topology (without or with the positivity predicate) in a predicative framework. Formal topology was introduced by P. Martin-Löf and G. Sambin to provide a predicative representation of the concept of locale and open locale [see \textit{G. Sambin}, ``Intuitionistic formal spaces -- a first communication, in: Mathematical Logic and its Applications, 187--204 (1987; Zbl 0703.03040), and ``Some points in formal topology, Theor. Comput. Sci. 305, No. 1--3, 347--408 (2003; Zbl 1044.54001)]. The inductive generation in topology is a very important tool since it allows one to reason on topology by induction, that is, by using proof-theoretic methods, and it provides predicative examples of formal topologies. One of these remarkable examples is the inductive formal topology of real numbers. In the paper, the authors start with discussing that the axiomatic definition of formal topology in the cited papers by G. Sambin is not inductive predicatively. At the end they also provide a counterexample of a predicative formal topology that is not inductive by taking the Dedekind-MacNeille cover on the Boolean set. Another difference between generic formal topologies and inductive ones is that, while inductively generated formal topologies are easily seen to be closed predicatively under suitable constructions, such as the closure under binary products, for formal topology it is still not known (predicatively!).
- A constructive proof of the Heine-Borel covering theorem for formal reals
- An extension of the Galois theory of Grothendieck
- An intuitionistic proof of Tychonoff's theorem
- Constructive domain theory as a branch of intuitionistic pointfree topology
- Continuous domains as formal spaces
- scientific article; zbMATH DE number 3853067 (Why is no real title available?)
- scientific article; zbMATH DE number 3853324 (Why is no real title available?)
- scientific article; zbMATH DE number 4152375 (Why is no real title available?)
- scientific article; zbMATH DE number 4152376 (Why is no real title available?)
- scientific article; zbMATH DE number 4108721 (Why is no real title available?)
- scientific article; zbMATH DE number 3787631 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 3581219 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- scientific article; zbMATH DE number 1302065 (Why is no real title available?)
- scientific article; zbMATH DE number 1420793 (Why is no real title available?)
- Inductive families
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- On the formal points of the formal topology of the binary tree
- Tychonoff's theorem in the framework of formal topologies
- Space of valuations
- A topos for algebraic quantum theory
- Constructive metrisability in point-free topology.
- Some points in formal topology.
- Embedding locales and formal topologies into positive topologies
- The problem of the formalization of constructive topology
- About Stone's notion of spectrum
- Predicativity and constructive mathematics
- Towards formal Baer criteria
- Equivalents of the finitary non-deterministic inductive definitions
- Cut elimination for entailment relations
- A constructive notion of codimension
- Vagueness, Kant and topology: a study of formal epistemology
- 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
- The intensional side of algebraic-topological representation theorems
- Positivity relations on a locale
- A minimalist foundation at work
- A point-free characterisation of Bishop locally compact metric spaces
- On the existence of Stone-Čech compactification
- Formalising overlap algebras in Matita
- The principle of pointfree continuity
- Spatiality and classical logic
- Relative formal topology: the binary positivity predicate comes first
- scientific article; zbMATH DE number 4152376 (Why is no real title available?)
- On some peculiar aspects of the constructive theory of point-free spaces
- Derived rules for predicative set theory: an application of sheaves
- Topological inductive definitions
- scientific article; zbMATH DE number 1531360 (Why is no real title available?)
- scientific article; zbMATH DE number 1746890 (Why is no real title available?)
- A constructive Galois connection between closure and interior
- Convergence in formal topology: a unifying notion
- Formal Baire space in constructive set theory
- A realizability semantics for inductive formal topologies, Church's thesis and axiom of choice
- Higher order functions and Brouwer's thesis
- Syntax for semantics: Krull's maximal ideal theorem
- scientific article; zbMATH DE number 7471696 (Why is no real title available?)
- Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
- The Jacobson radical for an inconsistency predicate
- Formal Topology and Univalent Foundations
- THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
- Generalising the fan theorem
- Representing continuous functions between greatest fixed points of indexed containers
- Sublocales in formal topology
- Presenting dcpos and dcpo algebras
- The generalised type-theoretic interpretation of constructive set theory
- Every countably presented formal topology is spatial, classically
- Completeness and cocompleteness of the categories of basic pairs and concrete spaces
- Dynamics in Foundations: What Does It Mean in the Practice of Mathematics?
- On Small Types in Univalent Foundations
- Apartness, sharp elements, and the Scott topology of domains
- Locatedness and overt sublocales
- Independence results in formal topology
- Cosheaves and connectedness in formal topology
- Sharp elements and apartness in domains
- A topological counterpart of well-founded trees in dependent type theory
- Patch locale of a spectral locale in univalent type theory
- Objects: a study in Kantian formal epistemology
- A topological reading of coinductive predicates in dependent type theory
- Continuous and algebraic domains in univalent foundations
- The patch topology in univalent foundations
- Effectiveness and continuity in intuitionistic quasi-toposes of assemblies
- Machine space. I: Weak exponentials and quantification over compact spaces
- Constructive substitutes for Kőnig's lemma
- A coverage construction of the reals and the irrationals
- Constructive characterizations of bar subsets
- A constructive and functorial embedding of locally compact metric spaces into locales
- Exact approximations to Stone-Čech compactification
- The basic Zariski topology
- Finitary formal topologies and Stone's representation theorem
- The Zariski spectrum as a formal geometry
This page was built for publication: Inductively generated formal topologies.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1412832)
