Proof Theory and Computation

There is a fundamental question which, since the pioneering contributions of Gödel, Gentzen and Herbrand seventy 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 at the Logic-Computer Science interface, namely "What is the information content of a (constructive) formal proof and how can it be read off ?" 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 and practical realizations of these possibilities.

Subrecursive hierarchy classifications attempt to structure the computable functions by means of transfinite hierarchies which precisely reflect both their computational complexity and the logical complexity of their 'termination proofs'. Although no natural way has been found of classifying all computable functions in one hierarchy, proof-treoretically significant subclasses can be successfully analysed in terms of the so-called Fast and Slow growing hierarchies developed by Schwichtenberg, Wainer, Weiermann and others. This work has deep connections with various other branches of mathematical logic and computer science - Proof Theory, Independence Results, Finitary Combinatorics, Program Verification, Complexity Theory etc.

• G. E. Ostrin: "Proof theories of low subrecursive classes", Ph.D. University of Leeds 1999.
• N. Cagman: "Tiered arithmetic, its functional interpretation and slow growing bounds", Ph.D. University of Leeds 2000.
• R. Williams: "Proof theoretic ordinals and hierarchies".

• M. V. Fairtlough and S. S. Wainer, "Hierarchies of provably recursive functions", Chapter III in S. Buss (ed) Handbook of proof theory, Studies in Logic Vol. 137, Elsevier Science BV 1998, pp. 149-207. (Not available here)
• S. S. Wainer, "Accessible recursive functions", Bulletin of Symbolic Logic Vol. 5, ASL 1999, pp. 367-388. (Not available here)
• N. Cagman, G. E. Ostrin and S. S. Wainer, "Proof theoretic complexity of low subrecursive classes", in F. L. Bauer and R. Steinbrueggen (eds) Foundations of Secure Computation, IOS Press Amsterdam 2000, pp. 249-286. postscript file
• G. E. Ostrin and S. S. Wainer, "Proof theoretic complexity", in J. Tiuryn and R. Steinbruggen (eds) Proof and System Reliability, Kluwer 2002, to appear. postscript file
• G. E. Ostrin and S. S. Wainer, "Elementary arithmetic", Leeds Pure Math. preprint no. 29, 2001. postscript file
• S. S. Wainer, "Provable recursiveness and complexity", invited lecture to appear in Proc. of Logic Colloquium '01, Vienna 2001, ASL Lecture Note Series. postscript file