The precise definition of formal proofs and the study of their structural properties are central issues in General (Structural) Proof Theory. On the other hand, Reductive (Interpretational) Proof Theory is mainly interested in the analysis of mathematical theories through their proofs and syntactical interpretation between them. General and Reductive studies is the classical division of Proof Theory. Cut elimination in sequent calculus and normalization theorems in natural deduction systems are fundamental results in general proof theory and are applied, for example, to decidability problems and to problems related to the complexity and identity of proofs. An important set of problems in reductive proof theory includes consistency problems, functional interpretations, ordinal analysis and translations between logics and theories. Although we have some very general and abstract results both in structural proof theory and in interpretational proof theory, an "Abstract Proof Theory" where one would be interested in very general and abstract conditions for structural/interpretational proof-theoretical analysis of formal systems still does not officially exist. The main purpose of this tutorial is to present some old and new proof-theoretical results in an abstract setting.

Basic proof theoretical methods will be presented from an abstract standpoint and four central topics will be discussed in details:

(1) A general strategy for cut elimination in the following sense: suppose that the rules of a certain sequent system S satisfy some very general conditions. Define rewriting rules for proof transformation. Then, one can prove that S satisfies cut elimination.

(2) A general normalization procedure for the abstract introduction and elimination rules due to P. Schröder-Heister.

(3) The general idea of ordinal analysis for a theory T.

(4) The relation between translation among logical systems and normalization procedures.

References:

1 Prawitz, D. Natural Deduction: A Proof-Theoretical Study. In Stockholm Studies in Phylosophy 3, Almqvist and Wiksell, Stockholm, 1965. Acta Universitatis Stockholmiensis.

2. Prawitz, D. Ideas and Results in Proof Theory. In J.E.Fenstad, editor, Proceedings of the Second Scandinaviam Logic Symposiym, North Holland, 1971.

3 Girard, J-Y., Lafond, Y. and Taylor, P. Proofs and Types. In Number 7 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1988.

4 Gentzen, G. Investigation into Logical Deductions. In M.E.Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68-131, North-Holland, Amsterdam, 1969.

5. Schröder-Heister, P. - A Natural Extension of Natural Deduction, In The Journal of Symbolic Logic, vol. 49, pp. 1284-1300.

6 Ungar, A.M. Normalization, Cut-Elimination and the Theory of Proofs. CSLI lectures notes, 28, 1992.

7. Troelstra, A.S. and Schwichtenberg, H. Proof Theory. Cambridge University Press, Cambridge, 1996