Indexed on: 08 Oct '19Published on: 06 Oct '19Published in: arXiv - Mathematics - Logic
In computational approaches to mathematics, open sets are generally studied indirectly via countable representations. For instance, an open set of real numbers with discontinuous characteristic function can be represented -or `coded'- by a sequence of open balls with rational center and radius. It is then a natural question whether the introduction of such codes changes the logical and computational properties of basic theorems pertaining to open sets. As we will see, sequential compactness seems unaffected by the use of codes, while (countable) open cover compactness is greatly impacted. Indeed, we identify numerous theorems for which the Main Question of Reverse Mathematics, namely which set existence axioms are necessary for a proving the theorem, does not have an (unique/unambiguous) answer when using the aforementioned characteristic functions in the stead of codes of open sets. In particular, we establish this for the Heine-Borel theorem (for countable covers) and the Heine, Urysohn, and Tietze theorems. We establish similar differences for the computational properties, in the sense of Kleene's S1-S9, of these theorems, namely a shift from `computable' to `not computable in any type two functional'. A finer study of representations of open sets leads to the new `$\Delta$-functional' which has unique computational properties. Finally, we also study the computational properties of Baire category theorem, resulting in similar results that however require very different proofs.