{"id":"arxiv/2602.19003","url":"https://arxiv.org/abs/2602.19003","tags":["math.LO","math.GN"],"score":0,"title":"Compactness in Constructive Mathematics via Affine Logic","domain":"math.LO","source":"arxiv","authors":["Kazumi Kasaura"],"reviews":0,"subject":"math.LO","summary":"We study topology, particularly compactness, as an extension of Shulman's work on constructive mathematics via affine logic, while allowing propositional impredicativity. We introduce a notion of compactness in affine logic and prove the fundamental properties of compactness, including the extreme value theorem and the Heine-Borel theorem for 'cuts', which are a version of Dedekind cuts in affine logic. Moreover, from the antithesis translation of the Heine-Borel theorem for cuts to intuitionistic logic, we derive the Heine-Borel theorem for one-sided reals intuitionistically, and have…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-02-22","reactions":{}}