Abstract
Continuity is a key principle of intuitionistic logic that is generally accepted by constructivists but is inconsistent with classical logic. Most commonly, continuity states that a function from the Baire space to numbers, only needs approximations of the points in the Baire space to compute. More recently, another formulation of the continuity principle was put forward. It states that for any function F from the Baire space to numbers, there exists a (dialogue) tree that contains the values of F at its leaves and such that the modulus of F at each point of the Baire space is given by the length of the corresponding branch in the tree. In this paper we provide the first internalization of this "inductive" continuity principle within a computational setting. Concretely, we present a class of intuitionistic theories that validate this formulation of continuity thanks to computations that construct such dialogue trees internally to the theories using effectful computations. We further demonstrate that this inductive continuity principle implies other forms of continuity principles.
Original language | English |
---|---|
Title of host publication | 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) |
Editors | Jérôme Leroux, Sylvian Lombardy, David Peleg |
Publisher | Schloss Dagstuhl |
Pages | 37:1-37:16 |
Number of pages | 16 |
ISBN (Electronic) | 9783959772921 |
DOIs | |
Publication status | Published - 21 Aug 2023 |
Event | 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) - Bordeaux, France Duration: 28 Aug 2023 → 1 Sept 2023 Conference number: 48 https://mfcs2023.labri.fr/ |
Publication series
Name | Leibniz International Proceedings in Informatics |
---|---|
Publisher | Schloss-Dagstuhl - Leibniz Zentrum für Informatik |
Volume | 272 |
ISSN (Electronic) | 1868-8969 |
Conference
Conference | 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) |
---|---|
Abbreviated title | MFCS |
Country/Territory | France |
City | Bordeaux |
Period | 28/08/23 → 1/09/23 |
Internet address |