arXiv Open Access 2026

Compactness in Constructive Mathematics via Affine Logic

Kazumi Kasaura

Lihat Sumber

Abstrak

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.

Topik & Kata Kunci

math.LO math.GN

Penulis (1)

Kazumi Kasaura

Format Sitasi

APA MLA BibTeX

Kasaura, K. (2026). Compactness in Constructive Mathematics via Affine Logic. https://arxiv.org/abs/2602.19003

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2026
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓