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 thirtysix page paper by a young mathematician,
Alan Turing, claiming to solve a
longstanding problem of the distinguished
German mathematician
David Hilbert. A byproduct of that solution
was the first machinebased model of what it means
for a numbertheoretic 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 reallife computers. The storedprogram 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 twentiethcentury
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 worldleading 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

Researchers
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 'ominimal' 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 ominimality 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 AxKochen/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 omegacategorical 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, VapnikChervonenkis dimension and density, and their applications.
PROOF THEORY & CONSTRUCTIVISM

Researchers
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 TransPennine 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
finestructural investigations of computationally
weak theories (Stan Wainer) and their spinoffs 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 socalled prooftheoretic
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 MartinLö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 settheoretic 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 categorytheoretic framework which subsumes both Homotopy Type
Theory and Quillen's homotopical algebra, the study of inductive and
higherinductive types, and the prooftheoretic 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, JeanClaude 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 wideranging 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 2025 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 twentyfive 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 200513) were coorganisers of
the 6month 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 cochair of the large 2012
Turing Centenary
Conference in Cambridge, and an organiser of the 6month 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 3week 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 coeditors 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 (200408)
and the FP7 Initial Training Network MALOA (200913).
Schuster coordinates an EU MarieCurie 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.