LOG221 Proof Theory, 7,5 credits

The course treats derivations and proofs as mathematical objects, and study these from a formal, syntactic point of view, unlike model theory that can be said to be the semantic theory of the corresponding phenomena.

Among the many proof formalisms that have been constructed, studied and implemented we focus on two central classes of systems: natural deduction and sequent calculus. The most fundamental theorems, whose proofs are implemented in detail are cut elimination and normalisation for propositional logic and predicate logic, but also for stronger systems, such as formalised arithmetic.

Philosophical and linguistic aspects of proof theory, as its connection with semantics and anti-realism, will also be addressed.

Literature

The main reference for this course is

• Structural Proof Theory by Sara Negri and Jan von Plato. (Cambridge University Press, 2001). Available as e-book in the University Library.

The following two textbooks are not necessary but may be useful as references:

• An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs by Mancosu, Galvan, and Zach (Oxford UP, 2021). Access through the university library. This book covers the main results from the course from a slightly different perspective.
• Basic Proof Theory by A.S. Troelstra and H. Schwichtenberg (CUP, 2000, 2nd edition). An e-book is available from the University libraries. This book technically focused (and dense) and covers a wide range of applications of proof theory. A list of errata (incomplete) is available from the first author’s webpage: http://www.uva.nl/profiel/t/r/a.s.troelstra/a.s.troelstra.html

Finally, two survey articles that are recommended are

• Samuel R. Buss’ “An Introduction to Proof Theory,” the opening chapter to the Handbook of Proof Theory (S. R. Buss, ed; Elsevier, Amsterdam, 1998). An electronic copy of this article is available from the author’s webpage: http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookI/
• The Stanford Encyclopedia of Philosophy has a very detailed article on Proof Theory which I also recommend.

Supplementary references will be listed in the corresponding modules.

Course plan and assessment

The course comprises lectures, classes and independent study. See the Modules for the syllabus and provisional schedule.

The course will be assessed in three parts: weekly exercises (five/six), a course paper, and a short presentation of the paper. To obtain a Pass (G) for this course, all assessed parts of the course should be passed. For a Pass with distinction (VG), the course should be passed and VG obtained in the course paper and presentation; criteria for these will be published alongside the assignments.

Schedule

The course runs weeks 3 to 12. The introductory lecture will be on Monday, 15 January 13.15 (room J577). There will two lectures each week on Monday and Wednesday, with an exercise class on Thursday led by Dominik Wehr. See the schedule on TimeEdit for times and rooms. Weekly assignments are due on Fridays at 17:00. The deadline for the course paper and presentations can be found in the list of Assignments. More information about course will be given in the first meeting.

Learning outcomes

On successful completion of the course the student will be able to:

Knowledge and understanding

• describe central concepts, methods and constructions in proof theory,
• contrast proof theory with other disciplines in logic,
• describe the relationship between natural deduction and sequent calculus,
• contrast structural systems with non-structural ones,
• demonstrate knowledge of proof theoretic semantics,

Competence and skills

• formulate and present proofs of the most important results in the course – in particular cut elimination and normalisation – as well as of lemmas that are used in the proofs,
• carry out advanced derivations in the formal proof systems that are introduced in the course,

Judgement and approach

• critically discuss, analyse and evaluate results in the course as well as their applications,
• show awareness of the relationships between on the one hand proof theory and constructive mathematics, and on the other hand proof theory and semantics.

See the course syllabus for more information.