Andrej Bauer ; Andrew Swan - Every metric space is separable in function realizability

lmcs:4651 - Logical Methods in Computer Science, May 23, 2019, Volume 15, Issue 2 - https://doi.org/10.23638/LMCS-15(2:14)2019
Every metric space is separable in function realizabilityArticle

Authors: Andrej Bauer ; Andrew Swan ORCID

    We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic does not show the existence of a non-separable metric space, or an uncountable set with decidable equality, even if we assume principles that are validated by function realizability, such as Dependent and Function choice, Markov's principle, and Brouwer's continuity and fan principles.


    Volume: Volume 15, Issue 2
    Published on: May 23, 2019
    Accepted on: April 24, 2019
    Submitted on: June 29, 2018
    Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,54E35, 03F60, 03F55

    Consultation statistics

    This page has been seen 1734 times.
    This article's PDF has been downloaded 322 times.