Proof Theory

There is a fundamental question which, since the pioneering contributions of Godel, Gentzen and Herbrand over fifty years ago, has motivated the continued development of that area of Mathematical Logic known as "Proof Theory", and which now drives much present-day activity in Theoretical Computer Science, namely "What is the information content of a constructive formal proof and how can it be read off ?" or, more specifically, "How is it possible to synthesize programs from formal proofs of their specifications , and hence classify and compare them - and the functions which they compute - according to their proof -theoretic complexity ?"

If, from a formal proof of the specification, it were possible effectively to extract or synthesize a program P which satisfies it, then the program would automatically be a "verified" one. If, in addition, it were possible to read off from the proof, bounds on the existential theorems occurring in it, this would provide an effective way of estimating the complexity of P. If this connection between proofs and programs were sufficiently close, then "natural" transformations on proofs would correspond to natural program transformations. Mathematical logic provides theoretical realizations of these possibilities, based on the deep and well known correspondence which exists between proof-rules and recursive program-constructs.

Applied Logic

• Proof Development Systems and Theorem Proving is an area of increasing importance, where Computer Science and Logic become indistinguishable, and where theory and practice go 'hand in hand'. The underlying ideas are supplied by Proof Theory, and practical implementation is made possible by powerful workstations. J. Derrick has for some years been active in the development of a collaborative network of research interests, linking with other groups in Computer Studies and Philosophy. It is intended to extend this activity in the coming years so as to provide a small Logic research laboratory based on two or three good workstations, for theorem-proving and inter-active proof development systems.. This would also be of benefit to other areas in pure mathematics,where certain problems necessitate the use of high powered computation.
• Set Theory provides an abstract axiomatic framework within which all areas of mathematics may be developed. However there are some crucial assumptions used in mathematics which are known to be independent of the set theory axioms, for example, forms of the Axiom of Choice are used in Algebra, and the Continuum Hypothesis is used in parts of Analysis. Thus there is a deep area of overlap here, between the foundational aspects of Set Theory and other fields of mathematics. F. R. Drake 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, and has ongoing collaborations with set theorists in USA.