Reverse mathematics of general topology

Think back to school, where we are taught mathematical facts, or theorems, such as the Pythagorean theorem and the fundamental theorem of calculus. These facts are true because they can be deduced by chains of logical steps. This is the standard of truth in mathematics: a mathematical statement is considered true and is called a theorem if there is a reasoned proof that the statement is true. Thus a mathematical proof is intended to be a demonstration of the absolute certainty of the theorem being proved. However, a proof is a chain of logical reasoning, and chains have to start somewhere. Behind every proof is a collection of basic assumptions, called axioms, about how the mathematical world works. These basic assumptions are the focus of our research.

Mathematics became more intricate and more abstract throughout the 1800s, largely due to great advances in algebra, geometry, and real analysis (the theoretical basis of calculus). Disagreements concerning the validity of certain proofs arose, and the need for a unified foundations of mathematics became apparent. Early attempts to provide these foundations were plagued by contradictions, such as Russell's famous paradox. These failures precipitated the so-called "foundational crisis in mathematics" of the early 1900s. In response to the crisis, David Hilbert, the greatest mathematician of his day, proposed what is now called "Hilbert's program." Hilbert encouraged mathematicians to seek the ultimate axioms, from which all mathematical statements can be either proved true or refuted as false; for which all proofs can be verified mechanically (nowadays, we would say by a computer); which are free of contradictions; and, critically, which can be proved to be free of contradictions using the axioms themselves. Such axioms would provide the ideal foundations, as they would answer any conceivable mathematical question without fear of contradiction.

In the 1930s, Kurt Gödel surprised the mathematical world with his incompleteness theorems, which imply that there can be no single collection of axioms founding all of mathematics as Hilbert desired. Part of what Gödel showed is that reasonable collections of axioms cannot prove themselves to be free of contradictions. Thus there is no solid foundation for all of mathematics; we can never know for sure that there is no contradiction lurking among our basic assumptions. From the work of Gödel, Tarski, Turing, and others, we now know that axiomatic systems form a sort of tower. The bottom levels correspond to weak axioms, where few theorems can be proved but the foundational footing is strong. The upper levels correspond to powerful axioms that can prove many theorems, but whose foundations are much shakier.

In the 1970s, Harvey Friedman initiated a program called "reverse mathematics" whose goal is to pinpoint exactly how far up the axiomatic tower one needs to climb in order to prove core mathematical theorems. This is interesting because by exactly determining what axioms are required prove a certain theorem, we exactly determine the foundational commitment we make by accepting its proof. There are potential practical benefits to such an inquiry as well. Weak axioms tend to be algorithmic in nature, so if a theorem can be proved from weak axioms, then sometimes computational information can be extracted from the proof. Conversely, if a theorem requires strong axioms, then this can mean that no such extraction is possible.

In this project, we analyze key theorems from topology (the study of mathematical spaces) in the style of reverse mathematics. To date, this has only been done in a fairly piecemeal fashion, despite topology being central to modern mathematics. Part of the problem is that topology is extremely general, whereas reverse mathematics works best when restricting to specific sorts of mathematical objects. We work to expand reverse mathematics and to help give a full account of the foundations of topology.

The project's topic is computability theory and its connections to proof theory and the foundations of mathematics. Specifically, we aim to develop the reverse mathematics of general topology. Reverse mathematics is a program in the foundations of mathematics designed to determine exactly what axioms are necessary and sufficient to prove core mathematical theorems. Many theorems throughout mathematics have been analyzed in the style of reverse mathematics. However, the reverse mathematics of topology is largely confined to the study of complete separable metric spaces. Our project will develop new approaches to the reverse mathematics of topology, thus moving well beyond the setting of complete separable metric spaces. This will have a major impact on researchers interested in computability theory, proof theory, and the foundations of mathematics. Through our efforts, a core mathematical subject that has been neglected by reverse mathematics will become much more accessible to researchers in the field. We expect our project to inspire many new directions in reverse mathematics. See "Academic Beneficiaries" and the "Case for Support" for more details of the mathematical impact of our research.

The project's wider impact will be to revitalize research in computability theory in the UK. Computability theory is one of the main branches of mathematical logic, along with model theory, proof theory, and set theory. Despite having a large international community and a history of UK excellence extending back to Turing, current UK capability in computability theory lags behind that of the other branches of logic. There are deep connections among the branches of mathematical logic. Indeed, the proposed project exhibits a connection between computability theory and proof theory. Thus increasing UK competitiveness in computability theory opens up new research directions, ultimately increasing UK competitiveness, in model theory, set theory, and proof theory as well. Increased capability in computability theory will also have long term economic and societal benefits for the UK. Many students of logic and computability make their careers in critical fields such as teaching, software engineering, finance, security, and defense.

In order to revitalize computability theory in the UK, the first step is to get more computability theorists into the UK. This will be accomplished by supporting a full-time research fellow and several short-term collaborating visiting researchers, all of whom will be invited to give research talks in Leeds and at other UK universities. The next step is to get young researchers actively engaged with the subject. To do this, we will develop and deliver a MAGIC course on computability theory. MAGIC (for Mathematics Access Grid Instruction and Collaboration) is a network of 21 UK universities that share PhD courses in mathematics via live video lectures. A MAGIC course on computability theory will be a great way to reach young researchers throughout the UK. The course will cover core topics in computability and survey contemporary research directions, such as reverse mathematics, highlighting how computability relates to other areas of mathematics.

Promoting mathematics to the public at large and encouraging students to study mathematics is an important part of every project. Our outreach activities will be in collaboration with MathsWorldUK, a Leeds-based organization currently developing a touring mathematics exhibition. We will help MathsWorldUK build exhibitions for its tour, and we will also volunteer at several of the science centers and science fairs that the tour will visit. We will also design new exhibitions on logic and computability for MathsWorldUK to add to its repertoire.

See "Pathways to Impact" for more details of how the project will promote mathematics, logic, and computability in the UK.