Reverse mathematics for the working mathematician

The project resides in the EPSRC research area of logic and combinatorics.

Investigations by a long list of mathematical logicians (e.g. Weyl, Hilbert, Bernays, Takeuti, Feferman, Friedman, Simpson to name a few) have shown that large swathes of ordinary mathematics can be undergirded by theories of fairly modest consistency strength.
This confirms what Hilbert surmised in his conservativity program, namely that elementary results (that is, those expressible in the language of number theory) proved in abstract,
non-constructive mathematics can in principle be proved by elementary means.
To obtain such results, logicians have developed elaborate theories for the formalization of mathematics, and shown, by a plethora of elaborate techniques from mathematical logic, that they are conservative over various elementary theories.

The best known program for determining the strength of theorems from ordinary mathematics is reverse mathematics (RM). RM's scale for measuring strength is furnished by certain standard systems couched in the language of second order arithmetic. However, this language is not expressive enough to be able to talk about higher order objects, such as function spaces, directly.
There are other suggestions, using formal systems in which higher order mathematical objects can be directly accounted for.
The price for maintaining conservativity over elementary theories, however, is that one has to adopt a semi-intuitionistic logic or define the concept of function in a non-set-theoretic
manner (or the imposition of other subtle restrictions).

One part of this PhD project consists of studying the connections between the various systems and determining their strength. This requires techniques from ordinal analysis and other tools of mathematical logic.

Another goal of the project is to find a formal system for reverse mathematics that can be easily learned and used by the working mathematician. Here a novel aspect is to use different logics for mathematical objects, namely classical logic for numbers but intuitionistic logic for higher type mathematical objects. The switch to intuitionistic logic for higher type objects has the advantage that the logical strength of the theories can be tamed, while at the same time allowing for the expressiveness of higher order languages. A further exciting aspect of intuitionistic logic is that it introduces a new dimension of axiomatic freedom in mathematics. However, the switch to intuitionist logic might be too radical for most mathematicians. Thus, another route to be explored aims to find better axioms for higher type object that do not engender enormous consistency strength even when classical logic is used.