Proof Theory

Course manual 2019/2020

Course content

Like the empirical sciences, mathematics and logic are concerned with truth. But unlike the empirical sciences, mathematics and logic establish truths by writing down deductions on the blackboard or on a piece a paper. Indeed, within mathematics and logic these proofs are our sole method for obtaining knowledge.

But what are these proofs? What properties do they have? Wihin proof theory we study these questions mathematically.

The starting point is that what counts as a valid proof is a purely formal matter: indeed, it depends on the shape of the argument rather than its precise content. For this reason proofs can be studied using proof calculi, that is, formal systems for deriving statements.

Within this course we study three types of proof calculi, Hilbert systems, natural deduction and sequent calculus, and establish their main properties. We will not only study proof calculi for pure logic, but also for arithmetic, and we will also be concerned with systems for constructive (or intuitionistic) logic.

The precise contents are:

Part 1: Logic

• Intuitionistic and classical logic
• Hilbert-style proof systems, natural deduction
• Negative translation
• Semantics of classical logic
• Sequent calculus for classical logic
• Cut elimination for classical logic
• Applications of cut elimination for classical logic
• Kripke semantics for intuitionistic logic
• Sequent calculus for intuitionistic logic
• Cut elimination for intuitionistic logic
• Applications of cut elimination for intuitionistic logic
• Normalisation for intuitionistic natural deduction
• Term assignments for intuitionistic natural deduction

Part 2: Arithmetic

• BHK interpretation
• Goedel's T
• Arithmetic in finite types
• Modified realizability
• Provably total functions in Heyting and Peano arithmetic
• Existence and disjunction property for Heyting arithmetic

Study materials

Syllabus

• Reader

Objectives

• be able to give formal derivations in different proof calculi (Hilbert-style proof calculi, natural deduction and sequent calculus), both for classical and constructive logic.
• know the main properties of these calculi (such as normalisation and cut elimination) and be able to use these to give mathematical proofs about these proof calculi.
• understand the difference between constructive and non-constructive arguments and be able to recognise when proofs are constructive or not constructive.
• be able to write down realizers which make the algorithmic content of constructively valid statements explicit.
• use Kripke models to give semantic proofs for properties of intuitionistic logic.

Teaching methods

Lecture course plus exercise sessions.

Learning activities

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 (but very little) background knowledge in logic; roughly, what is needed is familiarity with the syntax and semantics of first-order languages. 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

• B. van den Berg