License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.CCA.2009.2262
URN: urn:nbn:de:0030-drops-22629
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2262/
Go to the corresponding OASIcs Volume Portal


Brattka, Vasco ; Gherardi, Guido
Contributed Papers

Effective Choice and Boundedness Principles in Computable Analysis

pdf-format:
Brattka.2262.pdf (0.4 MB)


Abstract

In this paper we study a new approach to classify mathematical theorems according to their computational content. Basically, we are asking the question which theorems can be continuously or computably transferred into each other? For this purpose theorems are considered via their realizers which are operations with certain input and output data. The technical tool to express continuous or computable relations between such operations is Weihrauch reducibility and the partially ordered degree structure induced by it. We have identified certain choice principles on closed sets which are cornerstones among Weihrauch degrees and it turns out that certain core theorems in analysis can be classified naturally in this structure. In particular, we study theorems such as the Intermediate Value Theorem, the Baire Category Theorem, the Banach Inverse Mapping Theorem, the Closed Graph Theorem and the Uniform Boundedness Theorem. Well-known omniscience principles from constructive mathematics such as $\LPO$ and $\LLPO$ can naturally be considered as Weihrauch degrees and they play an important role in our classification. Our classification scheme does not require any particular logical framework or axiomatic setting, but it can be carried out in the framework of classical mathematics using tools of topology, computability theory and computable analysis. Finally, we present a number of metatheorems that allow to derive upper bounds for the classification of the Weihrauch degree of many theorems and we discuss the Brouwer Fixed Point Theorem as an example.

BibTeX - Entry

@InProceedings{brattka_et_al:OASIcs:2009:2262,
  author =	{Vasco Brattka and Guido Gherardi},
  title =	{{Effective Choice and Boundedness Principles in Computable Analysis}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{11},
  editor =	{Andrej Bauer and Peter Hertling and Ker-I Ko},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2262},
  URN =		{urn:nbn:de:0030-drops-22629},
  doi =		{10.4230/OASIcs.CCA.2009.2262},
  annote =	{Keywords: Computable analysis, constructive analysis, reverse mathematics, effective descriptive set theory}
}

Keywords: Computable analysis, constructive analysis, reverse mathematics, effective descriptive set theory
Collection: 6th International Conference on Computability and Complexity in Analysis (CCA'09)
Issue Date: 2009
Date of publication: 25.11.2009


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI