CONSTRUCTIVE REVERSE MATHEMATICS: COMPACTNESS PROPERTIES

Abstract

This chapter proposes a base formal system for constructive reverse mathematics to classify various theorems in intuitionistic, constructive recursive, and classical mathematics by logical principles, function existence axioms, and their combinations. The system is weak enough to allow for a comparison of the results obtained in it with those obtained within classical reverse mathematics as well as to prove theorems in Bishop's constructive mathematics. The chapter also formalizes results on compactness properties, such as the Heine-Borel theorem, the Cantor intersection theorem, the Bolzano-Weierstrass theorem, and sequential compactness, in the base formal system as test cases of its adequacy and faithfulness for the purpose of constructive reverse mathematics. The computability of function existence axioms and their combination with logical principles are also investigated, identifying them with closure conditions on a class of functions.