The Logic group is based in the
Department of Pure Mathematics, part of the School of Mathematics, the other
departments being those of Applied Mathematics and Statistics. The Logic
group also has members in the School of Computing, with which it has
increasingly close links, and also has connections to the School of
The Department of Pure Mathematics has around 20 permanent academic staff,
as well as a number of postdoctoral research fellows and research
assistants. There are research groups of international standing in four of
the most vital and central areas of mathematics: Algebra, Analysis,
Differential Geometry, and Logic. The Algebra and Differential Geometry
groups combine with the Integrable Systems group in Applied Mathematics to
form the AGIS group. The Logic group members in Computing are part of the
larger Algorithms and Complexity group.
There are usually about 35-45 research students in Pure Mathematics. As well
as regular research group seminars and more specialised working group
seminars, there are Departmental and School Colloquia of broader interest.
In addition, through the
weekly Pure Mathematics Postgraduate Seminar, PhD students interact with
those in other research groups. Postgraduate level courses are provided
through the MAGIC Taught Course centre, along with some courses provided
internally by the research groups.
The Department of Pure Mathematics is one of the major
centres for pure mathematics research in the UK, and is an ideal place in
which to obtain postgraduate training.
CURRENT RESEARCH IN MATHEMATICAL LOGIC
The Mathematical Logic Group
The Logic group is one of the largest and most active in Europe, with an
international reputation for research in several of the main areas of
mathematical logic - computability theory, model theory, proof theory,
computational complexity, and in applications to other parts of mathematics
and theoretical computer science. The group has been very successful in
obtaining research funding from EPSRC, the EU, and several other sources, in
all of its main areas of research. There is a continuing pattern of our
recent Ph.D.s being recruited to research or teaching positions in the UK
and around the world, particularly in Mathematics and Computer Science
The Logic Group has received extensive recent funding under EU schemes, for
postgraduate students, for postdoctoral researchers, and to coordinate
various research networks funding travel and conference activity for Leeds
logicians at all levels. This is part of a continuing process of widening
international research collaboration.
The group frequently hosts international conferences, workshops, and
postgraduate summer schools.
Postgraduate students are expected to attend the Logic seminar, which runs
roughly every second week, alternating with the Algebra, Logic, and
Algorithms seminar which builds links to other Leeds researchers in
mathematics and computer science. In addition, there are regular seminars,
developed primarily for research students, in computability theory, model
theory, and proof theory. There are also strong regional links: for example,
the Leeds model theorists, jointly with researchers in Manchester and
Preston, run the LYMOTS network funded by the London Mathematical Society.
(Rathjen and Gambino)
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 & Set Theory
(Macpherson, Truss, Brooke-Taylor and Mantova)
Model theory concerns the expressibility in formal logical languages,
typically in first order logic, of mathematical concepts. It is at the heart
of where logic meets the rest of mathematics, and it is common, at a model
theory conference, to hear in succession talks in pure Logic, in Algebra, in
Combinatorics, in Number Theory, and in Analysis. The subject is young. The
general theory (concepts such as type, elementary extension, saturation,
ultraproduct) was developed mostly in the 1950s and 1960s, and a much more
sophisticated theory (stability theory, and generalisations still being
developed) emerged in the 1970s and 1980s. Since the 1960s there have been
striking applications of model theory to other parts of mathematics. In
recent years, these parts include group theory, transcendental number
theory, geometry, combinatorics, analysis, and model theory has connections
also to parts of computer science such as computational complexity and
statistical learning theory.
We mention two interlocked themes in model theory, both central to stability
theory and generalisations.
One is a goal to explain how some mathematical objects (or 'structures'),
such as the field of complex numbers, are `tame' from the viewpoint of
Logic, and others, such as the field of rationals, are 'wild'. Typically,
the wild mathematical objects satisfy versions of Goedel's First
Incompleteness Theorem and many questions about them are undecidable, whilst
for the tame objects, often first order axioms can be identified and there
may be a rudimentary theory of dimension and independence, abstracted from
that in linear algebra.
A second theme is that of a 'definable set' (the solution set of a first
order formula in a first order structure). This is a kind of generalisation
of an algebraic variety (the solution set of a system of polynomial
equations in a field such as the complex numbers). Just as
algebraic geometers have developed a powerful theory to explain how
algebraic varieties inter-relate, e.g. with a dimension and independence
theory, so model theorists develop dimension and independence theories for
definable sets, viewing them as geometric objects. This tends to work best
in 'tame' structures.
There are other important features of model theory. First order logic seems
to have just the right level of expressiveness: it can express important
mathematical concepts (such as a field being algebraically closed), but
satisfies the Compactness Theorem, and first order sentences cannot pin down
an (infinite) mathematical structure completely. This often means that
important mathematical properties can be proved in a suitable structure and
'transferred' by means of Logic to other structures where they are far from
obvious. (As an example, a first order sentence is true of an algebraically
closed field K of characteristic 0 if and only if it is true of the complex
field, if and only if, for all but finitely many primes p, it is true for
some (or any) algebraically closed field of characteristic p. This was used
by Ax to show that if f is a polynomial injective map from a complex
variety to itself then f is surjective.)
Also, model theory has beautiful construction techniques (ultraproducts,
forcing, Fraisse amalgamation) which yield rich and compelling structures
often not visible to mathematicians with other backgrounds.
In Leeds, PhD students, postdocs, and staff work on many of these themes,
around topics such as the following.
The p-adic fields, like the real field, are completions of the
rationals, of great importance in number theory and algebra, and are
examples of valued fields. There is a beautiful model theory of valued
fields, stemming from the Ax-Kochen/Ershov Theorem of the 1960s, with many
applications. In Leeds we work on the pure model theory of valued fields
(from the viewpoint of stability theory), and on its applications, for
example in 'motivic integration'. This has deep applications, for example in
the representation theory of groups, in singularity theory, and in
Fraisse amalgamation gives a model theoretic method to construct
countable combinatorial structures (e.g. graphs, partial orders) with large
automorphism groups, and concepts of model theory (such as 'type') can be
translated into concepts from permutation group theory (such as 'orbit'). We
study the interplay between such structures and their automorphism groups,
looking at combinatorial properties of the former (e.g. properties coming
from Ramsey theory), and algebraic properties of the latter (e.g. simplicity
of the automorphism group). There are many applications, for example to
'constraint satisfaction', which is an approach to computational complexity
in computer science. Often, problems in this area, which links model theory,
combinatorics, permutation groups, and other topics, can be very concrete:
we consider detailed questions about automorphism groups of particular
structures, about classification for certain classes of highly symmetric
structures, and about what is definable in a particular combinatorial
Traditionally, model theorists look at infinite structures, since
for particular finite structures, first order logic is too expressive
(though there is an important subject of rather different flavour, finite
model theory, motivated more by theoretical computer science). However,
model theory is very well equipped to handle `families' of finite
structures. The ultraproduct construction replaces such a family by an
infinite limit with 'asymptotically' the same first order properties.
Model-theoretic methods are then applied to the infinite ultraproducts, and
transferred down to the finite structures. There are many applications, for
example in finite group theory.
Sometimes, abstract concepts identified by model theorists are later
seen to be familiar in other parts of mathematics. An example is the NIP
condition on a formula (a generalisation of the notion of stable formula).
It turns out that a family of sets defined by a NIP formula
is a Vapnik-Chervonenkis class, a notion identified in statistics in the
early 1970s, and important in statistical learning theory and neural
networks. We investigate Vapnik-Chervonenkis invariants in natural
Logic has intimate connections and applications to other parts of
mathematics, and to other disciplines. Within mathematics, some of the many
applications of model theory are described above, proof theory has expanding
links to homotopy theory, whilst constructivism represents an approach to
mathematics as a whole. Computability theory has had repeated interactions
with other parts of mathematics, for example probability theory (through
notions of randomness), and, historically, combinatorial group theory.
At a more interdisciplinary level, Logic is central to parts of Philosophy,
e.g. philosophical logic and foundations of mathematics. It also has crucial
interconnections on many levels, some described above, to Theoretical
Computer Science, and indeed, much of the membership of the
Colloquium comes from Computer Science and Philosophy departments. Other
fields developing links to Logic include Physics (e.g. through quantum
logic), Economics (for example through o-minimality in model theory), and
the social sciences.
This wider relevance of Logic motivates much of our research in Leeds. As
one example, we have seen since 2005 the emergence of the
Computability in Europe (CiE) and its conference series, bringing together
over 1200 logicians and computer scientists from hundreds of different
research centres - with Leeds providing the current President (Cooper).
Computability-theoretic issues underly many areas of
science, computer science and the humanities.
Most home students are fully funded (fees and maintenance)
by the Engineering and Physical Sciences Research
Council (EPSRC). Applications should be made to the department, which in
turn makes an application in July to EPSRC. It is advisable to make
applications and enquiries as early as possible. EPSRC can also fund fees
(but not maintainance) for other EC students.
are available to international, UK and EU students and you may be eligible.
The department welcomes overseas students, and for students without their
own source of funds there is a limited number of postgraduate scholarships
offered by the University for well-qualified students.
There are other routes to funding, including the
Further advice can be obtained from the Pure Postgraduate tutor (see below).
Programme of Study
for M.Phil. and Ph.D.
The degrees of M.Phil. and Ph.D. are awarded after study in the Department
for a minimum period of two or three years respectively. A research student
is normally registered as a provisional Ph.D. student. If progress is
satisfactory, his/her registration for the Ph.D. will be confirmed at the
beginning of the second year. Each student has his/her research directed by
one or more members of staff appointed as supervisor(s).
All research students are expected to attend at least one of the weekly
seminars in the department. They are urged to attend at least two
graduate lecture courses per year. We also encourage postgraduate students
to organise their own working seminars, and we provide guidance for this.
Facilities for computing and word-processing
Word-processing facilities are available for research students to type
papers and theses, as well as a number of laser printers. The School of Mathematics is well-equipped with
a variety of computing resources, including commonly used software. In addition the facilities
of the University Computing Service are available.
Wherever possible, students interested in studying for a research
degree are invited to the Department. If you require further
information on postgraduate work, or wish to arrange a visit, please
contact the Pure Mathematics Postgraduate Tutor,