Tatsuji Kawai ; Giovanni Sambin - The principle of pointfree continuity

lmcs:4280 - Logical Methods in Computer Science, March 5, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:22)2019
The principle of pointfree continuityArticle

Authors: Tatsuji Kawai ; Giovanni Sambin

    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 $\mathcal{S}$ and $\mathcal{T}$ says that any relation which induces a continuous operation between points is a morphism from $\mathcal{S}$ to $\mathcal{T}$. The principle holds under the assumption of bi-spatiality of $\mathcal{S}$. When $\mathcal{S}$ is the formal Baire space or the formal unit interval and $\mathcal{T}$ 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.


    Volume: Volume 15, Issue 1
    Published on: March 5, 2019
    Accepted on: February 17, 2019
    Submitted on: February 14, 2018
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03F55, 06D22
    Funding:
      Source : OpenAIRE Graph
    • Computing with Infinite Data; Funder: European Commission; Code: 731143

    Consultation statistics

    This page has been seen 1592 times.
    This article's PDF has been downloaded 513 times.