Course manual 2024/2025

Course content

As objects that witness validity of arguments, proofs are a central concept in logic and, more broadly, mathematics. Formal proofs come in many styles each equipped with their own toolkit. In this course we will look at some of the standard proof systems of classical and intuitionistic logic and develop an appreciation for pros and cons surrounding the different formalisms.

Main theorems covered in the course include Gentzen’s Hauptsatz (cut elimination) and a number of its consequences (subformula property, Herbrand’s theorem, existence and disjunction property, interpolation). Consistency, computational content, ordinal analysis (measuring strength of formal theories) will also be central to the curriculum.

In the second half of the course further advanced topics will be discussed including (but not limited to) omega logic, infinitary and cyclic proofs, predicative proof theory and unprovability results.

Study materials

Other

Lecture slides/notes will be provided through the course homepage.

Objectives

Present formal derivations in different proof calculi (Hilbert-style proof calculi, natural deduction and sequent calculus)
Explain the main properties of these calculi (such as normalisation and cut elimination)
Understand the difference between constructive and non-constructive reasoning
Recreate key concepts and techniques in proof theory
Demonstrate an understanding of proof theoretic methodology
Carry out combinatorial analyses of the structure of formal proofs
Critically compare different logics and proof calculi
Explain the role of proof theory in relation to other logical disciplines

Teaching methods

Lecture
Self-study
Seminar

Lecture course plus weekly exercise sessions.

Learning activities

Activity	Hours
Hoorcollege	28
Tentamen	3
Werkcollege	28
Self study	109
Total	168	(6 EC x 28 uur)

Attendance

This programme does not have requirements concerning attendance (TER-B).

Assessment

Item and weight	Details
Final grade
70% Tentamen	NAP if missing
30% Homework Assignments
1 (17%) Homework Assignment - Week 1
1 (17%) Homework Assignment - Week 2
1 (17%) Homework Assignment - Week 4
1 (17%) Homework Assignment - Week 3
1 (17%) Homework Assignment - Week 5
1 (17%) Homework Assignment - Week 6

The grading is on the basis of 6 weekly homework assignments and a final exam.
Your grade for the homework is based on the average grade you obtained on the 5 homework assignments for which you obtained the highest score.
Your final grade is calculated as the weighted average of these grades, with the homework /exam ratio being 30/70.

Inspection of assessed work

Contact the course coordinator to make an appointment for inspection.

Fraud and plagiarism

The 'Regulations governing fraud and plagiarism for UvA students' applies to this course. This will be monitored carefully. Upon suspicion of fraud or plagiarism the Examinations Board of the programme will be informed. For the 'Regulations governing fraud and plagiarism for UvA students' see: www.student.uva.nl

Course structure

Weeknummer	Onderwerpen	Studiestof
1
2
3
4
5
6
7
8

Additional information

We presuppose some background knowledge in logic; roughly, what is needed is familiarity with the syntax and semantics of first-order languages and ordinal numbers. More importantly, we assume that participants in the course possess some mathematical maturity, as can be expected from students in mathematics or logic at a MSc level.

Owner	Master Logic
Coordinator	dr. M. Girlando
Part of	Master Logic, Master Logic, track Logic and Mathematics, Master Logic, track Logic and Computation, Master Logic, track Logic and Philosophy, Master Logic, track Logic and Language, Master Logic, track Logic Year, year 1 Master Logic, track Exchange, year 1

Proof Theory