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

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.
Keywords Baire category   Weihrauch lattice   genericity   reverse mathematics  computable analysis
Categories (categorize this paper)
DOI 10.1215/00294527-2018-0016
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,290
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Effective Borel Measurability and Reducibility of Functions.Vasco Brattka - 2005 - Mathematical Logic Quarterly 51 (1):19-44.
Closed Choice and a Uniform Low Basis Theorem.Vasco Brattka, Matthew de Brecht & Arno Pauly - 2012 - Annals of Pure and Applied Logic 163 (8):986-1008.

View all 12 references / Add more references

Citations of this work BETA

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

Add more citations

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 (45):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 index

Total views
7 ( #1,071,713 of 2,519,272 )

Recent downloads (6 months)
3 ( #205,898 of 2,519,272 )

How can I increase my downloads?


My notes