UNIVERSITY OF LEEDS
Department of Pure Mathematics
MATHEMATICAL LOGIC SEMINAR
2000
ABSTRACTS

I recently finished a proof of half of something once known as Hancock's Conjecture. It has been 30 years in gestation, and should surely be known as Hancock's Proof; with this productivity rate there is little danger of a name clash.

There were already unsensational proofs of HC about 25 years ago, which are OK, but a little sleazy and ad hoc. Besides being more modern and therefore better, my proof has been machine checked by a very sacred Swedish type-checker ("Agda"); at last, the question can be left to fade peacefully into oblivion.

The subject (well ordering proofs in type theory) is a little exotic, and to explain its interest adequately would take a long time. Instead I'll just state what the problem is, and describe the overall form of its solution. This centres around the notion of a certain magnificatory gadget which I call a "lens".

The proof is in effect a program in dependent type theory (though it is a challenge to imagine circumstances in which anyone would want to run it). One novelty on which I shall focus is that it uses a cumulative sequence of (quite parsimonious) universe types (ie. types of types) besides conventional data structures.

Michael Zakharyashev (Leeds)
Decidable fragments of first-order modal and temporal logics
May 17th

The classical decision problem - to single out expressive and decidable fragments of first-order logic - has a long history and hardly needs any justification: after all, classical first-order logic was and still remains in the very center of logical studies, both in mathematics and applications. Here are only three examples (out of dozens) of such fragments:

• the fragment containing only monadic predicate symbols;
• the fragment with only two individual variables;
• the guarded fragment.

• the monadic fragment of many standard modal predicate logics is undecidable;
• the two-variable fragment of practically all modal predicate logics undecidable;
• the monadic two-variable fragment of linear temporal logic is not recursively enumerable;
• only the one-variable fragment of various standard modal predicate logics turns out to be decidable.

Ulrich Berger (Swansea)
$\mu$-recursion vs. least fixed points on the partial continuous functionals
May 23rd

We study the relationship between mu-recursion and least fixed point recursion on the partial continuous functionals `a la Scott and Ershov. We show that mu-recursion is weaker than least fixed point recursion for (a) partial continuous functionals of type two, (b) total continuous functionals of type three.

Finite model theory is concerned with the model theory of finite structures. It has strong connections with complexity theory and database theory. Whilst many of the tools of (infinite) model theory fail when we restrict interest to just finite structures, not all do. For example, Ehrenfeucht-Fra\"{\i}ss\'{e} Games enable one to prove undefinability results, and the hope is that (eventually) we might be able to use tools such as these to obtain logical undefinability results which translate into complexity-theoretic lower bound results. Some of the mainstream logics of finite model theory actually arise in the more computational context of program schemes. In this talk, I will introduce some classes of program schemes and their relationship with some logics from finite model theory, and show how the consideration of computations of program schemes enables us to prove logical undefinability results without having to play (complicated) games. This talk will be suitable for a broad audience.

This page is maintained by: M. Laura Crosilla
Last changed 31-Jan-2001.