On the computational properties of the Baire Category Theorem

TL;DR

This paper explores the computability aspects of the Baire Category Theorem using a novel lambda calculus model that captures classical computation schemes, revealing their computational equivalence.

Contribution

It introduces a new lambda calculus-based model for computability, analyzing classical theorems like Baire and Volterra within this framework.

Findings

Baire and Volterra theorems are computationally equivalent in the new model

The theorems are analyzable using fragments of Goedel's T

The model captures partial and total objects in computability

Abstract

Computability theory is a discipline in the intersection of computer science and mathematical logic where the fundamental question is: given two mathematical objects X and Y, does X compute Y in principle? In case X and Y are real numbers, Turing's famous 'machine' model provides the standard interpretation of 'computation' for this question. To formalise computation involving (total) abstract objects, Kleene introduced his S1-S9 computation schemes. In turn, Dag Normann and the author have introduced a version of the lambda calculus involving fixed point operators that exactly captures S1-S9 and accommodates partial objects. In this paper, we use this new model to develop the computability theory of various well-known theorems due to Baire and Volterra and related results; these theorems only require basic mathematical notions like continuity, open sets, and density. We show that these theorems due to Baire and Volterra are computationally equivalent from the point of view of our new model, sometimes working in rather tame fragments of Goedel's T.