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

I recommend the book An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs by Mancosu, Galvan, and Zach (Oxford UP, 2021; doi: 10.1093/oso/9780192895936.001.0001). Access is available through the university library.  

The official course text is A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory (2nd edition). Cambridge University Press, 2000. doi: 10.1017/CBO9781139168717. An e-book is available from the University libraries. This book technically focused and I recommend using the book An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs as a first reference. 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

A very good article discussing some of the central aims and results of proof theory is: Samuel R. Buss. “An Introduction to Proof Theory” In: Handbook of Proof Theory, edited by S. R. Buss. Elsevier, Amsterdam, 1998, pp 1-78. An electronic copy of this article is made available by the author from his 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

This will be primarily a reading course. Course meetings will provide complementary material and be used to discuss parts of the main text and exercises. See Modules for more information.

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

Schedule

The course runs weeks 3–12. Classes will be on Tuesday and Thursday at 10.15–12 (with some exceptions). See the schedule on TimeEdit and the overview page. Weekly assignments are due Friday afternoons. The course paper will be due before the end of the course (precise date TBD) and presentations will in the final course meetings (weeks 11/12). The first meeting of the course is on Tuesday, 18 January 2022 at 13.15-15.00 in room J406. More detail about course structure 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.