2026-07-22T04:54:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18571 2024-03-06T11:02:09Z ddc:004 open_access

Inductive Continuity via Brouwer Trees Cohen, Liron da Rocha Paiva, Bruno Rahli, Vincent Tosun, Ayberk Continuity Dialogue trees Stateful computations Intuitionistic Logic Extensional Type Theory Constructive Type Theory Realizability Theorem proving Agda 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Liron Cohen and Bruno da Rocha Paiva and Vincent Rahli and Ayberk Tosun 2023 Is Part Of LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2023.37 urn:nbn:de:0030-drops-185718 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.37 eng https://creativecommons.org/licenses/by/4.0/legalcode