This website is being archived. Please visit the new Logic group page instead. Postgraduate Studies in Logic Contents Introduction Current Research in the Mathematical Logic Group Funding International Students Programme of Study for M.Phil. and Ph.D Facilities Enquiries

Please also see the School of Maths Postgraduate research degrees information page, which has more general information, and sets logic in the context of the other research groups.

INTRODUCTION

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 Philosophy.

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.

Research Degrees. M.Phil., Ph.D.

CURRENT RESEARCH IN MATHEMATICAL LOGIC

The Mathematical Logic Group

Staff:

• Associate Professor Olaf Beyersdorff (School of Computing)
• Dr Andrew Brooke-Taylor
• Associate Professor Nicola Gambino
• Professor H. Dugald Macpherson
• Dr Vincenzo Mantova
• Professor Michael Rathjen
• Dr Paul Shafer
• Professor John K. Truss
• Research Professor Stanley S.Wainer

Background

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 departments.

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.

Research Plans

Proof Theory

(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.

1. 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 geometry.
2. 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 structure.
3. 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.
4. 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 mathematical structures.

Beyond Logic

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 British Logic 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 Association 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.

Funding

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. Postgraduate Scholarships are available to international, UK and EU students and you may be eligible.

International Students

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 Postgraduate Scholarships. 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.

Enquiries

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, Prof Martin Speight.