Course syllabus
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.
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 introductory lecture will be on XX. See the schedule on TimeEdit (will be posted later) 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.
Search here for course syllabus and litterature list for more information: link.
Contact information
- Course coordinator Ivan Di Liberti, ivan.di.liberti@gu.se answers questions about the course content, literature and schedule.
- Education administrator Sandra Schriefer, sandra.schriefer@gu.se answers questions about registration, study interruptions, study breaks, certificates, etc.
- Education administrator Annika Herrström, annika.herrstrom@gu.se answers questions about examination administration.
- Program Coordinator Ivan Di Liberti, ivan.di.liberti@gu.se is responsible for programme issues and study guidance for students of the programme.
- Education Coordinator Andreas Ott, andreas.ott@gu.se
Plagiarism and academic integrity
Please take the time to go through the module Academic Integrity 1 to make sure that you understand what plagiarism is, why one should not plagiarise, and what happens if one does plagiarise.
Student information
Welcome to the department of Philosophy, Linguistics and Theory of Science