Proof Theory

Course manual 2021/2022

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.

Attendance

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

Assessment

• 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:
  • the homework /exam ratio is 30/70;
  • an additional proviso is that the you need to score at least 50/100 points on the exam.

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

Timetable

The schedule for this course is published on DataNose.

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.

Contact information

Coordinator

• dr. B. Afshari