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 such as co-finite choice,
discrete choice, interval choice, compact choice and closed choice, 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.
We also explore how existing classifications of the Hahn—Banach Theorem and
Weak Kőnig's Lemma fit into this picture.
Well-known omniscience principles from constructive mathematics such as LPO and LLPO
can also naturally be considered as Weihrauch degrees and they
play an important role in our classification.
Based on this we compare the results of our classification with existing classifications
in constructive and reverse mathematics and we claim that in a certain
sense our classification is finer and sheds some new light on the computational
content of the respective theorems.
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.
We develop a number of separation techniques based on a new parallelization
principle, on certain invariance properties of Weihrauch reducibility,
on the Low Basis Theorem of Jockusch and Soare and based on the Baire Category Theorem.
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.