The principle of pointfree continuity
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4280/pdf |
| _version_ | 1827322828569968640 |
|---|---|
| author | Tatsuji Kawai Giovanni Sambin |
| author_facet | Tatsuji Kawai Giovanni Sambin |
| author_sort | Tatsuji Kawai |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:35:01Z |
| format | Article |
| id | doaj.art-ebc165e4c085482b87237599bb9924a7 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:01Z |
| publishDate | 2019-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-ebc165e4c085482b87237599bb9924a72024-03-08T10:27:56ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-03-01Volume 15, Issue 110.23638/LMCS-15(1:22)20194280The principle of pointfree continuityTatsuji KawaiGiovanni SambinIn 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.https://lmcs.episciences.org/4280/pdfcomputer science - logic in computer sciencemathematics - logic03f55, 06d22 |
| spellingShingle | Tatsuji Kawai Giovanni Sambin The principle of pointfree continuity Logical Methods in Computer Science computer science - logic in computer science mathematics - logic 03f55, 06d22 |
| title | The principle of pointfree continuity |
| title_full | The principle of pointfree continuity |
| title_fullStr | The principle of pointfree continuity |
| title_full_unstemmed | The principle of pointfree continuity |
| title_short | The principle of pointfree continuity |
| title_sort | principle of pointfree continuity |
| topic | computer science - logic in computer science mathematics - logic 03f55, 06d22 |
| url | https://lmcs.episciences.org/4280/pdf |
| work_keys_str_mv | AT tatsujikawai theprincipleofpointfreecontinuity AT giovannisambin theprincipleofpointfreecontinuity AT tatsujikawai principleofpointfreecontinuity AT giovannisambin principleofpointfreecontinuity |