Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compactness in Constructive Mathematics via Affine Logic

Kazumi Kasaura

Abstract

We study topology, particularly compactness, as an extension of Shulman's work for constructive mathematics via affine logic, while allowing propositional impredicativity. In addition to some basic properties of compactness, we prove 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 its proof with the interactive theorem prover. The code is available at https://github.com/hziwara/CutsHeineBorel.

Compactness in Constructive Mathematics via Affine Logic

Abstract

We study topology, particularly compactness, as an extension of Shulman's work for constructive mathematics via affine logic, while allowing propositional impredicativity. In addition to some basic properties of compactness, we prove 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 its proof with the interactive theorem prover. The code is available at https://github.com/hziwara/CutsHeineBorel.
Paper Structure (7 sections, 19 theorems, 69 equations)

This paper contains 7 sections, 19 theorems, 69 equations.

Table of Contents

  1. Introduction
  2. Notation
  3. Topology
  4. Compactness
  5. Topology on Cuts
  6. Antithesis Translation of the Heine-Borel Theorem
  7. Conclusion

Key Result

Proposition 4

Moore interior operators correspond one-to-one to Moore collections of open subsets, and interior operators correspond one-to-one to collections of open subsets.

Theorems & Definitions (57)

  • Remark 1
  • Definition 2
  • Definition 3
  • Proposition 4
  • proof
  • Remark 5
  • Definition 6
  • Proposition 7
  • proof
  • Remark 8
  • ...and 47 more