School of Mathematics

Search site

PhD research topics in pure mathematics

Proof Theory
Wainer, Rathjen 

A central theme running through all the main areas of modern Mathematical Logic is the classification of sets, functions, theories or models, by means of transfinite hierarchies whose ordinal levels measure their 'rank' or 'complexity' in some sense appropriate to the underlying context. Such hierarchy classifications differ widely of course, in their modes of construction and their intended application, but they often provide the means to discover deep connections between areas which may on the surface seem quite unrelated.

In Proof Theory, from the work of Gentzen in the 1930's up to the present time, this central theme is manifest in the assignment of 'proof theoretic ordinals' to theories, measuring their 'consistency strength' and 'computational power', and providing a scale against which those theories may be compared and classified. There is a 'process' (not yet fully understood in the abstract, but emerging clearly in practice) by means of which the proof theoretic ordinal of a theory is computed: one first unravels the induction and comprehension principles of the given theory into infinitary rules which reflect their intended meaning. A proof which was finite in the original theory thus becomes an infinite well-founded derivation-tree whose height is measured by some ordinal. The problem is then to transform this tree with its complex logical structure and comprehension rules, into another derivation-tree in which the premises of any rule are less complex (logically) than is the conclusion. For then it is easy to see, by induction through the derivation, that no inconsistency can be proven. This, generally speaking, is Cut Elimination or Normalization.

If one can estimate the 'operational cost' of Cut Elimination, in terms of the transformation in the sizes of derivation-trees as they get normalized, then the least ordinal closed under that operation will measure the length of transfinite induction needed to prove the theory consistent, i.e. 'consistency strength'. In fact more explicit computational information is gained as well: this ordinal also turns out to be the least upper bound on the termination orderings of all functions which can be provably computed in the given theory. Thus if a program can be proved to terminate in the theory, the cut-elimination transformation provides a complexity bound in terms of the so-called Fast Growing Hierarchy. Not only does this link directly to the extraction of combinatorial independence results for specific theories, it is also one of the crucial points where Proof Theory nowadays interacts with Theoretical Computer Science, in providing pure mathematical underpinnings for constructive type theories, the verification and synthesis of programs, and the measurement of their complexity.

Ordinal Analysis is now a sophisticated and technically complex area of Proof Theory, and it is particularly interesting because the more powerful set-existence principles codified into a theory seem to necessitate the use of large cardinals from set theory (or their analogues from generalized recursion theory) in the construction of their proof theoretic ordinals by so-called 'collapsing functions'. Even though the proof theoretic ordinal will in the end be countable, its construction and computation may use abstract diagonalization processes which need to be 'indexed' along the way, and as Bachmann first realised, the most natural way to do this is to utilize higher cardinals. Their set theoretic complexity will thus be reflected in the size of the final proof theoretic ordinal and in the complexity of its 'presentation' as a well ordering on natural numbers. But why? and how? We need to understand the underlying mechanisms.

Model Theory
HalupczokMacpherson, Truss

Model Theory is the study of the first-order properties of mathematical structures. First-order logic is strong enough to give a lot of information about a structure, but weak enough that any reasonable first-order theory has many different models, and often a result can be proved in one model and transferred by logical considerations to other models. A major contribution of model theory is to provide general notions of independence and dimension which extend those of linear algebra and algebraic geometry. Model theory is pursued for its own interest, but in recent years it has also had exciting applications in many subjects, such as number theory, algebraic geometry, and group theory.

Structures arising in model theory often have rich automorphism groups, and permutation group theory has had many applications in model theory, whilst model theory is the main source of examples of infinite permutation groups. H.D. Macpherson and J.K. Truss have worked extensively in this area, and recent and current research topics include: omega-categorical structures (a class for which most model-theoretic conditions have exact group-theoretic translations); the structure of automorphism groups; the extent to which a structure is recoverable from its automorphism group; infinite families of finite permutation groups, and the corresponding infinite limits; the model theory of permutation groups (as 2-sorted structures).

There is particular interest in ordered and treelike structures. This has led to work by Truss on various treelike partial orders and their automorphism groups, and by Macpherson to the development of notions related to o-minimality, and in turn to the model theory of valued fields, possibly with analytic structure.

Truss works also on certain set-theoretic topics, usually related to model theory and permutation groups via questions about the axiom of choice. Certain independences between weak versions of the axiom of choice are related to properties of suitable universal-homogeneous structures in model theory, and the connection between definability (of subsets or more complicated configurations) in first order structures, and existence in corresponding set-theoretical universes is a very fruitful one. Analogues of strong minimality and o-minimality in set theory without choice have also been studied.

Some of the work by Macpherson and Truss on permutation groups is purely group-theoretic and combinatorial, without model-theoretic connections. For example, Macpherson has worked on maximal subgroups of infinite symmetric groups, and Truss has proved a number of results concerning simplicity of automorphism groups of infinite structures.


Gauge fields, or connections, are a generalisation of electromagnetic fields studied in theoretical physics and differential geometry; they are one of the key ingredients in the standard model of particle physics.  Instantons are gauge fields which extremise an energy functional (the Yang-Mills functional), and studying instantons on four-dimensional manifolds led to a number of breakthroughs in the subject of four-manifold topology.  Now it is hoped that studying instantons in higher dimensions will lead to similar progress, particularly in the study of so-called G_2-manifolds and Spin(7)-manifolds.  This project will focus on some explicit examples of instantons on such manifolds, with the goals being determination of the dimension of the moduli space in which they reside and the construction of new solutions.

Goemetry and dynamics of topological solitons
Speight, Harland

Field theory is the natural mathematical language to explain fundamental physics, from particle physics, to condensed matter, to gravitation and cosmology. In many field theories it is possible for the dynamical field, a map from spacetime into some manifold, to wrap itself up rather like a high-dimensional knot. Such a field traps large amounts of energy in a smooth, spatially localized lump, called a topological soliton ,which can move around and interact with other solitons in remarkably particle-like fashion. Solitons are natural candidates for fundamental particles (e.g. magnetic monopoles, protons, neutrons), but they also model large scale structures in condensed matter physics (e.g. vortices in superconductors) and cosmology (e.g. cosmic strings). There is a beautiful geometric theory of the dynamics of solitons which describes their motion in terms of the moduli space of static multisolitons, a mathematically rich and fascinating object in its own right. The aim of this project is to study the geometry of topological solitons and connect it to their dynamics, in one of many possible specific contexts. There is flexibility to give the project an algebraic-geometric (e.g. twistor constructions in gauge theory) or differential-geometric flavour (e.g. geometry of the moduli space of harmonic maps) flavour, or even a more direct physical slant, with some numerical work (solitons in exotic superconductors).

Operators on spaces of analytic functions

Many Hilbert spaces of analytic functions on the complex right half-plane can be seen as corresponding, via the Laplace transform, to weighted L^2 spaces on the positive real line. These include the classical Hardy and Bergman spaces, as well as a large class of spaces known as Zen spaces. Although (weighted) Hankel, Toeplitz and composition have been much studied in the context of the classical spaces, a lot less is known for Zen spaces, and many significant questions may be investigated. There are also potential applications in systems and control theory.