The principle of pointfree continuity

MaRDI QIDQ3121524zbMATH OpenFDO

Authors Tatsuji Kawai, Giovanni Sambin

Publication date 18 March 2019

Full work available at URL https://arxiv.org/abs/1802.04512

zbMATH Keywords

Baire spacechoice sequencesconstructive mathematicscontinuity principlepointfree topologyreal numbersspatiality

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Frames, locales (06D22) Continuous maps (54C05)

Abstract: In the setting of constructive pointfree topology, we introduce a notion of continuous operation between pointfree topologies and the corresponding principle of pointfree continuity. An operation between points of pointfree topologies is continuous if it is induced by a relation between the bases of the topologies; this gives a rigorous condition for Brouwer's continuity principle to hold. The principle of pointfree continuity for pointfree topologies $mathcalS$ and $mathcalT$ says that any relation which induces a continuous operation between points is a morphism from $mathcalS$ to $mathcalT$. The principle holds under the assumption of bi-spatiality of $mathcalS$. When $mathcalS$ is the formal Baire space or the formal unit interval and $mathcalT$ is the formal topology of natural numbers, the principle is equivalent to spatiality of the formal Baire space and formal unit interval, respectively. Some of the well-known connections between spatiality, bar induction, and compactness of the unit interval are recast in terms of our principle of continuity. We adopt the Minimalist Foundation as our constructive foundation, and positive topology as the notion of pointfree topology. This allows us to distinguish ideal objects from constructive ones, and in particular, to interpret choice sequences as points of the formal Baire space.

Recommendations

• Point-free continuum
• The fixed point property for continua
• Extension by continuity in pointfree topology
• On the continuity principle
• The Analytic Principle of Continuity
• scientific article; zbMATH DE number 3867634
• scientific article; zbMATH DE number 4055612
• scientific article; zbMATH DE number 3855987
• Absolute continuity from a topological point of view
• Points of continuity and quasicontinuity

Cites work

• A constructive proof of the Heine-Borel covering theorem for formal reals
• A minimalist two-level foundation for constructive mathematics
• Constructivism in mathematics. An introduction. Volume I
• Embedding locales and formal topologies into positive topologies
• Formal systems for some branches of intuitionistic analysis
• Formally continuous functions on Baire space
• From Sets and Types to Topology and Analysis
• scientific article; zbMATH DE number 3853067 (Why is no real title available?)
• scientific article; zbMATH DE number 4152376 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• scientific article; zbMATH DE number 41225 (Why is no real title available?)
• scientific article; zbMATH DE number 1531375 (Why is no real title available?)
• scientific article; zbMATH DE number 3216177 (Why is no real title available?)
• scientific article; zbMATH DE number 2247253 (Why is no real title available?)
• scientific article; zbMATH DE number 2247257 (Why is no real title available?)
• scientific article; zbMATH DE number 2247258 (Why is no real title available?)
• scientific article; zbMATH DE number 2247263 (Why is no real title available?)
• Inductively generated formal topologies.
• Information systems for continuous posets
• Some points in formal topology.
• Spatiality for formal topologies
• The continuum as a formal space

Cited in

(7)

• Why topology in the minimalist foundation must be pointfree
• Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
• From Intuitionistic Mathematics to Point-Free Topology
• Formally continuous functions on Baire space
• Reducibility, a constructive dual of spatiality
• Principles of bar induction and continuity on Baire space
• scientific article; zbMATH DE number 6288823 (Why is no real title available?)

This page was built for publication: The principle of pointfree continuity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3121524)