Compactness in Constructive Mathematics via Affine Logic
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914409653207040 |
|---|---|
| author | Kasaura, Kazumi |
| author_facet | Kasaura, Kazumi |
| contents | 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 verified the proof with an interactive theorem prover. The code is available at https://github.com/hziwara/CutsHeineBorel. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_19003 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Compactness in Constructive Mathematics via Affine Logic Kasaura, Kazumi Logic General Topology 03B47 (Primary) 54A99, 26E40 (Secondary) 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 verified the proof with an interactive theorem prover. The code is available at https://github.com/hziwara/CutsHeineBorel. |
| title | Compactness in Constructive Mathematics via Affine Logic |
| topic | Logic General Topology 03B47 (Primary) 54A99, 26E40 (Secondary) |
| url | https://arxiv.org/abs/2602.19003 |