Bar recursion and products of selection functions
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 71277939
- Type
- D - Journal article
- DOI
-
10.1017/jsl.2014.82
- Title of journal
- Journal of Symbolic Logic
- Article number
- -
- First page
- 1
- Volume
- 80
- Issue
- 01
- ISSN
- 0022-4812
- Open access status
- Out of scope for open access requirements
- Month of publication
- March
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
-
- Citation count
- 10
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The product of selection functions gives computational content to the Tychonoff Theorem from topology. With this, we learn that certain infinite sets can be exhaustively searched in an algorithmic way. We discovered that this also optimally plays sequential games and gives computational content to the axiom of dependent choice. This paper further relates this with Spector's Bar recursion from proof theory, used to give computational content to classical analysis. It is the core of a body of work presented at the Institute Henri Poicare (Paris, 2014), CCC (Munich, 2015), Bergen University, Nordic Congress of Mathematicians, Leeds Logic Seminar and Tallin.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -