Research in Logic at Leeds Mathematical logic, a young subject, has developed over the last 20 years into an amalgam of fast-moving disciplines, each with its own sophisticated techniques. These are linked by profound common concerns, around definability, decidability and (feasible) computability, the nature of the continuum, foundations. Some branches are highly multidisciplinary, and force the researcher to be fully conversant with other fields (eg. algebra, computer science). Logic research at Leeds covers a wide spectrum of topics, and includes three of the main areas of mathematical logic, as well as linking to other areas of mathematics and theoretical computer science. Contents Computability Theory Model Theory Proof Theory The Leeds Logic Group

See also the School of Maths Postgraduate Brochure, or the Postgraduate Opportunities page accessed by the link on the left. The personal homepages also contain more detailed information on research activities.

COMPUTABILITY THEORY

Researchers

• Professor S Barry Cooper
• Professor Stanley S Wainer
• Dr George Barmpalias
• Dr Andrew E M Lewis

It has been claimed that while the focus in 20th century mathematics was to develop grand formalisms like algebra and topology, the focus in the 21st century will be on extracting data and algorithms.

We can see now that the world changed in 1936, in a way quite unrelated to the newspaper headlines of that year concerned with such things as the civil war in Spain, economic recession, and the Berlin Olympics. The end of that year saw the publication of a thirty-six page paper by a young mathematician, Alan Turing, claiming to solve a long-standing problem of the distinguished German mathematician David Hilbert. A by-product of that solution was the first machine-based model of what it means for a number-theoretic function to be computable, and the description of what we now call a Universal Turing Machine. At a practical level, as Martin Davis describes in his 2001 book Engines of Logic: Mathematicians and the Origin of the Computer, the logic underlying such work became closely connected with the later development of real-life computers. The stored-program computer on one's desk is a descendant of that first universal machine. What is less often remembered is Turing's theoretical contribution to the understanding of the limitations on what computers can do. There are quite easily described arithmetical functions which are not computable by any computer, however powerful. And even the advent of quantum computers will not change this.

Before computers, computer programs used to be called algorithms. Algorithms were just a finite set of rules, expressed in everyday language, for performing some general task. What is special about an algorithm is that its rules can be applied in potentially unlimited instances of a particular situation. We talk about the algorithmic content of Nature when we recognise patterns in natural phenomena which appear to follow general rules. Ideally algorithms and algorithmic content need to be captured precisely in the language of mathematics, but this is not always easy. There are areas (such as sociology or the biological sciences) where we must often resort to language dealing with concepts not easily reducible to numbers and sets. One of the main tasks of science, at least since the time of Isaac Newton, is to make mathematically explicit the algorithmic content of the world about us. A more recent task is to come to terms with, and analyse, the theoretical obstacles to the scientific approach. This is where the discovery of incomputability, and the theory which flows from it, play such an important role.

It is only in the last century, of course, that computability became both a driving force in our daily lives and a concept one could talk about with any sort of precision. Computability as a theory is a specifically twentieth-century development. And so of course is the computer, and this is no coincidence. Today this contemporary awareness and understanding of the algorithmic content of everyday life is still in its infancy, and forms the basis of a rich and deeply relevant research area. Since its inception, computability theory has provided deep conceptual insights, new algorithmic and programming ideas and technique, and mathematical theories on which to found software technology. For example, in the standard courses on computability one finds the origins of: the universal computer; recursion; lambda calculus; rewrite systems; formal specification of computations; higher types; classification of decision problems; classification of data representations; computational complexity. In each case, seen from contemporary Computer Science, the mathematical investigations in computability theory that led to these fundamental ideas are brilliant theoretical speculations - quite simply, basic mathematics at its best.

Today, computability retains this important speculative role in our quest to understand the big ideas of algorithm, computation, program, machine, and formal system description. A number of computability theorists are now both mathematicians and computer scientists, and European science -- including scientists brought together for the CiE project, coordinated from Leeds -- continue to play a world-leading role. Here in Leeds computer scientists and logicians maintain SIGLaC - the Special Interest Group in Logic and Computer Science. See Barry Cooper's new book for further background:

Relative computability and degree structures

The concepts of this area are in the center of foundational research in computability (and computational complexity) theory. It also provides a powerhouse of new techniques which become progressively utilised in other areas such as computable analysis, computable model theory, and complexity theory. The most exciting recent work (much of it involving researchers connected with Leeds) concerns Turing automorphisms and definability, and its modelling implications for the real universe. A major task is to extend and apply the new techniques and to further work out the consequences of the Turing model throughout science and the humanities.

At the technical level, there is a close connection between definability in local structures and longstanding undecidability problems for small fragments of the theory of the computably enumerable (c.e.) Turing degrees. A main aim is to pursue the elusive natural definitions of basic degree classes, which everyone believes to exist, and to answer some basic algebraic questions on the meet operator (related to the longstanding embedding problem for finite lattices, generating sets and automorphism bases).

Enumeration reducibility and enumeration degrees are receiving more and more attention among computability theorists. Enumeration degrees provide a wider context for the Turing degrees, and other notions of relative computability such as the continuous degrees. Enumeration reducibility also arises naturally in applications of computability theory to other areas of mathematics, for instance the analysis of types in effective model theory and the study of existentially closed groups. A main objective is to investigate the first order theory of the enumeration degrees, with the eventual aim of characterising theories for the local structure.

MODEL THEORY

Researchers

• Professor H Dugald Macpherson
• Professor Anand Pillay
• Dr Alan B Slomson
• Professor John K Truss
• Dr Roman Wencel

Model theory began life as the study of abstract logical expressibility in mathematical structures. Over the last 15 years it has had spectacular interactions with other fields. In one direction, the notion of o-minimality has given a model-theoretic framework for semi-algebraic and subanalytic geometry. There have been striking applications of o-minimality to diverse fields such as Lie theory, asymptotics, and neural networks.

In another direction, stability and simplicity theory, whilst providing in their own right an abstract theory of independence and dimension, have had startling applications in diophantine geometry. Another body of model theory, around definable sets in pseudofinite and valued fields, has had sophisticated applications to the burgeoning theory of motivic integration. There have also been important applications between model theory and group theory: model theory offers insight on algebraic groups and finite simple groups, for example through work on groups of finite Morley rank; there has been an extremely deep interaction between model theory and hyperbolic geometry, leading to a logical understanding of free groups; and there have been mutually beneficial interactions between model theory and permutation group theory, with model theory providing examples, and group theory providing classification techniques for models via their symmetry groups.

The UK has world leaders in this field and there will be a six-month semester Model theory and applications to algebra and analysis at the Newton Institute, Cambidge, January--July 2005, with one of the organisers (Macpherson) from Leeds. Also, Leeds is a participant in the Marie Curie Research Training Network MODNET, which runs from 1 January 2005 to 31 December 2008.

PROOF THEORY

Researchers

• Professor Michael Rathjen
• Professor Stanley S Wainer

Proof theory, the mathematical analysis of proof structure, has deep interest from the purely mathematical point of view. It isolates notions of constructibility, intimately connected with set theory. There are also close connections with computer science, for there is ever-increasing research activity in synthesizing verified programs from their formally derived specification proofs.

One application arises as follows: it is undecidable in general whether a given program meets its specification. By contrast, it can be checked easily by machine whether a formal proof is correct, and from a constructive proof one can, by fundamental proof--theoretic methods, automatically extract a corresponding program, which by its very construction is correct as well. This opens a way to produce correct software, e.g. for safety-critical applications.

THE LEEDS LOGIC GROUP

The Leeds Logic Group is one of three international "centres" for Mathematical Logic in UK, the others being Oxford and Manchester. It has a long and illustrious history tracing back fifty years to its establishment by M. H. Löb. It is the largest, most wide-ranging of these UK groups and one of the strongest and broadest worldwide. It includes international leaders in the fields of model theory (Macpherson and Truss), proof theory (Rathjen and Wainer) and computability theory (Cooper). Truss and Rathjen also have strong interests in aspects of set theory. The logic group was specifically highlighted in the feedback reports of the last two Research Assessment Exercises (in both of which the Pure Mathematics Department received a grade 5), and over recent years has attracted a large number of the Department's graduate research students.

The group has a high international profile with, over the past fifteen years, an impressively strong record of invitations to speak at major conferences. In 1997, the European Logic Colloquium (the largest international annual logic meeting, sponsored by the Association for Symbolic Logic) was held in Leeds for the fourth time. Members of the group are involved in the organisation of many other meetings, both in the UK and abroad; for example, Truss was the main organiser of a major Euresco meeting on Algebra and Discrete Mathematics in Hattingen in 2003, Wainer is one of the Directors of a biennial NATO--sponsored summer institute on Logic and Computation in Bavaria, and will chair the programme committee for Logic Colloquium '05 in Athens. Cooper co-organised a number of international meetings as part of the recent INTAS funded project Computability and Models for which he was coordinator, and is co-chair of the programme committee for Computability in Europe 2005 in Amsterdam. Leeds has played a major role in the British Logic Colloquium, the UK organisation representing Logic, with Wainer as a past President, Truss a past Treasurer, and Macpherson (presently) and Cooper (previously) committee members. The BLC annual conference was held in Leeds in 2004. Truss was until 2003 one of two co-editors of the Journal of the London Mathematical Society, Wainer is an editor of the Archive for Mathematical Logic, Rathjen of the Journal of Symbolic Logic and Macpherson of the Bulletin of Symbolic Logic and Communications in Algebra.

The group has many visitors, both for collaborations and through the weekly seminar. There are close links with new developments in computer science via SIGLaC - a Special Interest Group in Logic and Computer Science. In addition, there are often specialist study groups in branches of logic; at present there is a regular study group in computabiity theory, and another, joint with Manchester, on applications of model theory to motivic integration.