On the Uniform Computational Content of the Baire Category Theorem

Notre Dame Journal of Formal Logic 59 (4):605-636 (2018)
  Copy   BIBTEX


We study the uniform computational content of different versions of the Baire category theorem in the Weihrauch lattice. The Baire category theorem can be seen as a pigeonhole principle that states that a complete metric space cannot be decomposed into countably many nowhere dense pieces. The Baire category theorem is an illuminating example of a theorem that can be used to demonstrate that one classical theorem can have several different computational interpretations. For one, we distinguish two different logical versions of the theorem, where one can be seen as the contrapositive form of the other one. The first version aims to find an uncovered point in the space, given a sequence of nowhere dense closed sets. The second version aims to find the index of a closed set that is somewhere dense, given a sequence of closed sets that cover the space. Even though the two statements behind these versions are equivalent to each other in classical logic, they are not equivalent in intuitionistic logic, and likewise, they exhibit different computational behavior in the Weihrauch lattice. Besides this logical distinction, we also consider different ways in which the sequence of closed sets is “given.” Essentially, we can distinguish between positive and negative information on closed sets. We discuss all four resulting versions of the Baire category theorem. Somewhat surprisingly, it turns out that the difference in providing the input information can also be expressed with the jump operation. Finally, we also relate the Baire category theorem to notions of genericity and computably comeager sets.



    Upload a copy of this work     Papers currently archived: 86,213

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Some weak forms of the Baire category theorem.Kyriakos Kermedis - 2003 - Mathematical Logic Quarterly 49 (4):369.
Some More Conservation Results on the Baire Category Theorem.Takeshi Yamazaki - 2000 - Mathematical Logic Quarterly 46 (1):105-110.
An analogue of the Baire category theorem.Philipp Hieronymi - 2013 - Journal of Symbolic Logic 78 (1):207-213.
Topological framework for finite injury.Kyriakos Kontostathis - 1992 - Mathematical Logic Quarterly 38 (1):189-195.
Density and Baire category in recursive topology.Iraj Kalantari & Larry Welch - 2004 - Mathematical Logic Quarterly 50 (4-5):381-391.
Effective Borel measurability and reducibility of functions.Vasco Brattka - 2005 - Mathematical Logic Quarterly 51 (1):19-44.
Some remarks on Baire’s grand theorem.Riccardo Camerlo & Jacques Duparc - 2018 - Archive for Mathematical Logic 57 (3-4):195-201.


Added to PP

9 (#1,036,895)

6 months
1 (#864,772)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Completion of choice.Vasco Brattka & Guido Gherardi - 2021 - Annals of Pure and Applied Logic 172 (3):102914.

Add more citations