Compactness in Constructive Mathematics via Affine Logic

TL;DR

This paper explores a new notion of compactness within affine logic, extending constructive mathematics, and proves fundamental theorems like Heine-Borel for cuts, verified with an interactive theorem prover.

Contribution

It introduces a novel concept of compactness in affine logic and establishes key theorems, bridging to intuitionistic logic and formal verification.

Findings

Proved the extreme value theorem and Heine-Borel theorem for cuts in affine logic.

Derived the Heine-Borel theorem for one-sided reals via translation to intuitionistic logic.

Verified proofs using an interactive theorem prover, with code available online.

Abstract

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.