A Computational Perspective on Metamathematics

Vasco Brattka (UniBwM Munich) gives a talk at the MCMP Colloquium (29 January, 2015) titled "A Computational Perspective on Metamathematics". Abstract: By metamathematics we understand the study of mathematics itself using methods of mathematics in a broad sense (not necessarily based on any formal system of logic). In the evolution of mathematics certain steps of abstraction have led from numbers to sets of numbers, from sets to functions and eventually to function spaces. Another meaningful step in this line is the step to spaces of theorems. We present one such approach to a space of theorems that is based on a computational perspective. Theorems as individual points in this space are related to each other in an order theoretic sense that reflects the computational content of the related theorems. The entire space is called the Weihrauch lattice and carries the order theoretic structure of a lattice enriched by further algebraic operations. This space yields a mathematical framework that allows one to classify theorems according to their complexity and the results can be essentially seen as a uniform and somewhat more resource sensitive refinement of what is known as reverse mathematics. In addition to what reverse mathematics delivers, a Weihrauch degree of a theorem yields something like a full "spectrum" of a theorem that allows one to determine basically all types of computational properties of that theorem that one would typically be interested in. Moreover, the Weihrauch lattice is formally a refinement of the Borel hierarchy, which provides a well-known topological complexity measure (and the relation of the Weihrauch lattice to the Borel hierarchy is very much like the relation between the many-one or Turing semi-lattice and the arithmetical hierarchy). Well known classes of functions that have been studied in algorithmic learning theory or theoretical computer science have meaningful and very succinct characterizations in the Weihrauch lattice, which underlines that this lattice yields a very natural model. Since the Weihrauch lattice is defined using a concrete model, the lattice itself and theorems as points in it can also be studied directly using methods of topology, descriptive set theory, computability theory and lattice theory. Hence, in a very true and direct sense the Weihrauch lattice provides a way to study metamathematics without any detour over formal systems and models of logic.