This website is being archived. Please visit the new Logic group Research page instead. Research in Logic at Leeds Mathematical logic, a young subject, has developed over the last 30 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, theoretical computer science, and more generally to physics, biology, social sciences and philosophy. Contents Computability Theory Model Theory Proof Theory & Constructivism The Leeds Logic Group

See also the School of Maths Postgraduate research degrees information page, 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

Background

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 the Turing Centenary edition of his book The Universal Computer: The Road from Leibniz to Turing , 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 Leeds is playing a world-leading role, with Cooper currently President of the Association Computability in Europe, a managing editor of its journal COMPUTABILITY, and, during the years leading up to 2012 and subsequently, Chair of the Turing Centenary Advisory Committee. See Barry Cooper's book on Computability Theory for further background:

Relative computability

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 & SET THEORY

Researchers

• Dr Andrew Brooke-Taylor
• Professor H Dugald Macpherson
• Dr Vincenzo Mantova
• Professor John K Truss

Model theory began life as the study of abstract logical expressibility in mathematical structures. Over the last 20 years it has had increasingly spectacular, and often unexpected, applications to other fields, whilst a rich and sophisticated internal theory has continued to develop.

The 'internal' theory has been dominated by the study of two categories. One is the category, in a first order structure, whose objects are the definable sets (solution sets of first order formulas), and whose morphisms are the definable maps between these sets. This may be viewed as an abstraction from the category of constructible sets and morphisms in algebraic geometry. The other is the category of all models of a given complete theory, where the morphisms are the elementary embeddings.

Model theorists investigate the borderline between 'tame' and 'wild' structures and theories. Whilst it is not clear where this border lies, it has meaning in both of the above categories. At the wild extreme we have theories such as those of Peano Arithmetic and Set Theory which are subject to the phenomena of Gödel's Incompleteness Theorems. At the tame end are theories such as that of the complex field, which are 'uncountably categorical: that is, all models of any given uncountable cardinality are isomorphic. Over the last 50 years, this tame context has been extended to that of 'stable' theories, and to other broader settings such as those of simple theories, NIP theories, and NTP2 theories (a common generalisation of simple and NIP). These notions from stability theory are often fruitfully localised to parts of a structure ('generically stable types') or to families of formulas. There is also an immensely rich notion of 'o-minimal' ordered structure, in which ideas are combined from stability theory, from Lie theory and real algebraic geometry, and from real analysis.

Model theory has diverse interactions with other parts of mathematics. For example, methods from o-minimality have connections to real Lie theory, to asymptotics, to neural networks, to economics, and, in striking recent work of Pila, Wilkie and others, to number theory and Diophantine geometry. Stability theory since the mid 1990s has also had important applications to Diophantine geometry, and has many connections to group theory, e.g. to algebraic groups (in the study of groups of finite Morley rank) and to geometric group theory (free groups have stable theory). Since the Ax-Kochen/Ershov results from the 1960s, the model theory of valued fields has had wide applications, most recently through motivic integration and through a new approach to Berkovich spaces in rigid analytic geometry.

In Leeds, we have current interests in many parts of model theory and its applications. These include:

- The model theory of valued fields, e.g. imaginaries in valued fields, the notion of generically stable type, and motivic integration and its applications (e.g. to representation theory and singularity theory).

- Homogeneous and omega-categorical structures, and connections to permutation group theory, combinatorics, topological dynamics, and constraint satisfaction. A major theme here is the classification of classes of structures with rich symmetry properties, and investigation of the algebraic, combinatorial, and topological structure of their automorphism groups.

- The model theory of finite and pseudofinite structures, under 'tameness' assumptions on the definable sets.

- The model theory of groups in various settings - for example, model theoretic properties of families of finite simple groups of any fixed Lie type, and applications.

- the combinatorics of generalisations of stability: for example, the NIP property, Vapnik-Chervonenkis dimension and density, and their applications.

PROOF THEORY & CONSTRUCTIVISM

Researchers

• Dr Nicola Gambino
• Professor Michael Rathjen
• Professor Stanley S Wainer
• Dr Olaf Beyersdorff (School of Computing)

Background

Both research areas have their roots in the radical transformation of mathematics in the 19th century. The most prominent names associated with them are Hilbert and Brouwer, respectively.

Proof theory studies the concepts of mathematical proof and provability and thereby also the 'negative' concept of unprovability. Since the notion of proof is central to mathematics, the mathematical analysis of proof structure is of great interest from the purely mathematical point of view. But it is also important in computer science and automated theorem proving.

The foundations of a systematic approach to constructive mathematics, CM, were laid in Brouwer's intuitionism and Bishop's mathematics. While CM is often reputed to be a particularly restrictive view of mathematics motivated by foundational philosophical concerns, it has turned out that intuitionistic reasoning emerges naturally in core areas of mathematics and in the theory of computation. Notwithstanding that historically proof theory and intuitionism seem to represent opposing views, there are profound connections between the two research areas at a deeper level.

Some of the research directions in Proof Theory and Constructivism pursued at Leeds are described below. The group has been holding almost weekly seminars during term time since 1996. The seminars offer an important stage for airing new ideas and discussing recent developments. In the past, they were often held jointly with the Manchester group around Peter Aczel. In 1996 it was called the Trans-Pennine Proof Theory Seminar, at that time Harold Simmons being one of the organizers. Later, when constructive set theory and type theory became a frequent topic, it transmogrified into the Leeds and Manchester Proofs and Sets Seminar, LaMPaSS. Today, the Manchester group is still very much involved in the seminar in that Nicola Gambino works now on the other side of the Pennines and Peter Aczel has become a Leeds fixture.

Research areas

Ordinal analysis of quite strong theories (Michael Rathjen) as well as fine-structural investigations of computationally weak theories (Stan Wainer) and their spin-offs in combinatorial independence proofs (of Kruskal and Ramsey type) and 'reverse mathematics' have driven much of the proof theoretical work in Leeds. The central theme of ordinal analysis is the classification of theories by means of transfinite ordinals that measure their 'consistency strength' and 'computational power'. The so-called proof-theoretic ordinal of a theory also serves to characterize its provably recursive functions and can yield both conservation and combinatorial independence results. This work has also played an important role in connecting differing frameworks for mathematics such as admissible set theory, constructive set theory, explicit mathematics, and Martin-Löf type theory.

Another major area of research (involving Nicola Gambino, Michael Rathjen, Peter Schuster, Andrew Swan and also Peter Aczel from Manchester) is constructive set theory, CST. CST provides a set theoretical framework for the development of constructive mathematics and a refining framework within which distinctions between notions, which are not apparent in the classical context, become revealed. Central questions of investigations concern the independence of set-theoretic principles, the formalization of mathematics within CST, predicativity, and the role of large set axioms, analogous to the large cardinal axioms of classical set theory.

A particularly active strand of research concerns the connections between type theory and homotopy theory which have been discovered in recent years, giving rise to Voevodsky's Univalent Foundations of Mathematics programme and to the research area generally known as Homotopy Type Theory. Our work in the area focuses on the development of a category-theoretic framework which subsumes both Homotopy Type Theory and Quillen's homotopical algebra, the study of inductive and higher-inductive types, and the proof-theoretic strength of Voevodsky's resizing rules. This research involves Michael Rathjen, Nicola Gambino, Andrew Swan and Christian Sattler.

Nicola Gambino is also working on the theory of analytic functors, with the aim of constructing cartesian closed bicategories with generalized versions of analytic functors as morphisms. This research is closely connected to the theory of operads and aspects of enumerative combinatorics (the theory of combinatorial species). This research is being developed in collaboration with André Joyal and with Marcelo Fiore, Martin Hyland, and Glynn Winskel.

Peter Schuster's fields of interest are constructive and predicative mathematics as well as Hilbert's Programme. Currently his focus is on extracting the computational content of classical proofs in algebra in which transfinite methods are at use. Schuster's key idea is to move from Zorn's Lemma, ubiquitous in algebra, to the logically equivalent but computationally much better suited principle of Open Induction, which he imported from infinite combinatorics (Ulrich Berger, Thierry Coquand, Jean-Claude Raoult). He is collaborating on this topic with Ulrich Berger and Davide Rinaldi.

THE LEEDS LOGIC GROUP

The Leeds Logic Group is one of a select group of international "centres" for Mathematical Logic in UK, including Oxford, Manchester, and UEA. It has a long and illustrious history tracing back sixty years to its establishment by M. H. Löb. It is the largest and 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 (Halupczok, Macpherson and Truss), proof theory (Beyersdorff, Gambino, Rathjen, Schuster 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 past Research Assessment Exercises, and over recent years has attracted a large number of the Department's graduate research students, with typically around 20-25 logic PhD students at any given time. Though the group is based mainly in the School of Mathematics, Beyersdorff is based in the School of Computing, and there are links to others in the School of Computing (Bennett, Cohn, Stell) and the School of Philosophy (Williams).

The group has a high international profile with, over the past twenty-five 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, Macpherson and Pillay (Leeds 2005-13) were co-organisers of the 6-month 2005 Newton Institute Programme Model theory with applications to Algebra and Analysis, Wainer chaired the programme committee for Logic Colloquium '05 in Athens, and Cooper was a co-chair of the large 2012 Turing Centenary Conference in Cambridge, and an organiser of the 6-month Isaac Newton Institute programme Semantics and Syntax: A Legacy of Alan Turing. Leeds has played a major role in the British Logic Colloquium, the UK organisation representing Logic, with Wainer as a past President, Macpherson as current President, and Cooper, Schuster, and Truss as past or present Committee members. The BLC annual conference was held in Leeds in 2004 and 2013. There have been many other recent logic events in Leeds, such as the 3-week 2009 Symposium on proof theory and constructivism. Cooper is President of the Association Computability in Europe, and Chair of the Turing Centenary Advisory Committee. Truss was until 2003 one of two co-editors of the Journal of the London Mathematical Society, Wainer an editor of the Archive for Mathematical Logic, Rathjen of the Journal of Symbolic Logic, Macpherson is a Managing Editor of Mathematical Logic Quarterly and the ASL book series Lecture Notes in Logic, and Cooper of Computability, of Logical Methods in Computer Science, of Science China - Information Sciences, and chairs the Editorial Board of the CiE/Springer book series Theory and Applications of Computability.

The group coordinated the EU FP6 Early Stage Training Network MATHLOGAPS (2004-08) and the FP7 Initial Training Network MALOA (2009-13). Schuster coordinates an EU Marie-Curie International Research Staff Exchange Scheme (IRSES) EU project entitled Correctness by Construction.

The group has many visitors, both for collaborations and through the regular Logic seminar. There are close links with new developments in computer science, for example through the Algebra, Logic and Algorithms seminar which alternates with the Logic seminar. In addition, there are often specialist study groups in branches of logic; at present there is a regular seminar in computability theory run by the research students in computability, a regular seminar in proof theory and constructivism, and in model theory, a weekly seminar as well as a weekly postgraduate seminar.