Parkinson Building Logic at Leeds

People
Research
Seminars
Postgrad
opportunities

Pure
Department

School of
Mathematics

University
of Leeds

Some
outside links

Graduate
courses

Homepage


Postgraduate Studies

Contents

Please also see the School of Maths Postgraduate Brochure, which has far more general information, and puts logic in the context of the other research groups.

INTRODUCTION

The Department of Pure Mathematics forms part of the School of Mathematics, the other departments being those of Applied Mathematical Studies and Statistics. The department has 20 academic staff, as well as a number of postdoctoral research fellows and research assistants. The Department was rated 5 in both of the last two Research Assessment Exercises.

There are usually about 30 research students. As well as the weekly seminars which are mentioned below, there is a less specialised departmental Colloquium which meets once or twice a term. There is also a graduate lecture course each year in each of Mathematical Logic, Algebra, Analysis and Differential Geometry.

The aim of the Department of Pure Mathematics at Leeds for many years has been to maintain and develop research groups of international standing in four of the most vital and central areas of mathematics: mathematical logic, algebra, analysis and differential geometry. In each of these subjects there is plenty of lively research activity at Leeds. The department is one of the largest and most active 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:

Background

A discussion amongst logicians The 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, set theory and foundations, proof theory, and in applications to algebra, analysis and theoretical computer science. The group has been very successful in obtaining EPSRC support for research assistants and post-doctoral fellows. It became the focus of extensive EPSRC and EC funded international collaboration during the recent Leeds Recursion Theory Year (see the photograph on the right). There is a developing trend of our more recent Ph.D.s moving to research or teaching positions in Computer Science departments.

The Logic Group has in recent years received funding under the EC Science Plan in three collaborative 'twinning' projects, in Proof Theory and Computability, in Complexity, Logic and Recursion Theory, and in Model Theory. This is part of a continuing process of widening international research collaboration. The Leeds Group expects to be centrally involved in future such developments. It has hosted a number of major conferences, including Logic Colloquium 1997, one of the main annual international conferences in Logic.

There is a weekly Logic seminar with invited speakers, which postgraduate students are expected to attend. In addition, a combined Leeds-Manchester seminar in Proof Theory has become established, and in Model Theory there are collaborative events involving the Universities of Leeds, Manchester, and Birmingham and UMIST, having been funded by a London Mathematical Society grant. In Computability Theory, there is a Special Interest Group in Logic and Computation, which organises seminars in cooperation with members of the School of Computing. The computability theorists and model theorists also run their own regular internal seminars.

Research Plans

Computability Theory

(Professors Cooper and Wainer, and Dr Lewis)

The seminal work of Gödel, Turing, Kleene, Post and others in the 1930's and 1940's, demonstrated the fundamental importance - in mathematics and in computer science - of the theory of computability and relative computability (previously called 'recursion theory'). New developments in areas such as chaos theory, quantum mechanics, and in the social sciences and humanities, have brought a growing awareness of incomputability as an omnipresent phenomenon. Deep structural analyses of the universes of computable and non-computable objects have been developed, using

(i) degree structures based on Turing's notion of relative computability, but also widened to allow possible non-determinate computations, and refined to take account of complexity restrictions on time and space; and

(ii) subrecursive hierarchies, measuring and classifying computable objects and their algorithms according to their logical and computational complexity. These analyses, and their intimate connections with other areas of mathematical logic and theoretical computer science, drive the research of the Leeds Logic Group in this area.

Degree theory reveals great complexity of structure, requiring highly sophisticated and technically difficult methods for its analysis. Its study has formed one of the central areas of research in computability theory over the last thirty years, yet it is only recently that some of the deeper patterns and interrelationships have emerged. One of the longest-standing open problems was solved by a member of the Leeds group - S. B. Cooper - who proved that it is possible to define the jump operation purely in terms of the ordering of degrees. More recently, Professor Cooper has attracted international attention for his work on nonrigidity of the Turing universe, and its scientific and philosophical implications. He has written a recently published graduate text on Computability Theory.

Subrecursive hierarchy classifications attempt to structure the outright- computable reals by means of transfinite hierarchies which precisely reflect both their computational complexity and the complexity of their 'termination proofs'. Many large and important subclasses have been successfully analysed in terms of the so-called Fast and Slow growing hierarchies developed by S. S. Wainer and others. This work has deep connections with various other branches of mathematical logic and computer science - Proof Theory, Independence Results, Finitary Combinatorics and Theories of Program Verification, Complexity Theory etc. There is a good deal of interest from the Artificial Intelligence and Computer Science communities, in this and related areas of Proof Theory (see below), and the Leeds Logic Group is continuing to develop both national and international research collaborations with other logic and computer science groups in this field.

Proof Theory

(Professors Wainer and 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

(Professors Macpherson, Pillay and 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.

Applied Logic - interdisciplinary links

(Professor Dales and others)

Several members of the Leeds Logic group have strong interests in developing applications, both interdisciplinary and within pure mathematics. Connections between Model Theory and Algebra are already described above. In addition, F.R. Drake - a retired member of staff with continuing links with the logic group - is well-known for his work on Set Theory and Foundations, and H.G. Dales, whose interests lie in Analysis, has done important work on the application of set theoretic methods in his field. The importance of Logic in providing crucial theoretical underpinnings for computer science, is now widely recognised. The Leeds Logic Group formed one of the principal bases upon which the University's Centre for Theoretical Computer Studies (CTCS) was built in 1985, to facilitate and encourage further collaboration between mathematicians, philosophers, and computer scientists. J. Derrick has for some years been actively involved in collaborative links within the CTCS, mainly in the area of machine-implemented proofs and theorem proving.

More recently, such links have continued within SIGLaC, the Special Interest Group in Logic and Computation. And the new Computability in Europe (CiE) initiative, bringing together logicians and computer scientists from sixty-five different European research centres, and coordinated from Leeds, is another expression of the continuing activity in this area.

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. A few international students of exceptional promise are partially funded through the ORSAS, the Overseas Research Students Award Scheme, whose awards are often supplemented by the School of Mathematics.

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. In addition, there are 'ORSAS awards', which make up the difference between the cost of fees for an overseas student and a home student. In combination with the University's Tetley & Lupton Scholarships, these cover the full cost of overseas fees (but not maintenance).

A source of funding until 2008 is MATHLOGAPS - or Mathematical Logic and Applications - which is an EU Marie Curie Early Stage Training (EST) grant involving three other European universities.

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. The School of Mathematics is well-equipped with Sun workstations and PCs. In addition the facilities of the University Computing Service are available.

Parkinson Building

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, write or telephone the

Pure Postgraduate Tutor, Department of Pure Mathematics, University of Leeds, Leeds LS2 9JT. Telephone: Leeds (0113) 3435109; email: rathjen@maths.leeds.ac.uk



Maintained by: Barry Cooper