Skip to main content
CODE 107014
ACADEMIC YEAR 2024/2025
CREDITS
SCIENTIFIC DISCIPLINARY SECTOR MAT/01
LANGUAGE Italian (English on demand)
TEACHING LOCATION
  • GENOVA
SEMESTER 2° Semester

OVERVIEW

Proof theory is one of the four pillars of mathematical logic, and is of fundamental interest to mathematicians, computer scientists, philosophers, and linguists.  Proof theory has historical roots in  Aristotle's syllogisms and in  Leibniz's dream of a calculus ratiocinator for the formalization and automation of reasoning. In the 20th century  proof theory was strongly called for by  Hilbert's program and with the groundbreaking contributions by Gentzen and the invention of natural deduction and sequent calculus was developed into an independent field of study. Proof theory is concerned with the development of formal systems of deduction, conceived as syntactically defined formal objects, the study of their properties, and their applicability to concrete problems beyond the discipline.

 

 

AIMS AND CONTENT

LEARNING OUTCOMES

The course introduces the study of demonstrations as formal objects of mathematics by analyzing their structure and applying it to particular logical systems, with attention to the automation of demonstrations.

AIMS AND LEARNING OUTCOMES

In this course we will study deductive systems for classical and intuitionistic logic and their extensions for mathematical theories.

In particular, we will study the relationship between axiomatic systems, of natural deduction and sequent calculus, with particular emphasis on their use for the search for proofs.

The purpose of the course is, on the one hand, to present the central results of proof  theory and, on the other hand, to enable the students to autonomously define and use deductive systems with good properties for the meta-theoretical study of logical systems, their applications, and the automation of proofs.

 

SYLLABUS/CONTENT

0. Introduction to proof theory

1.  From natural deduction to sequent calculus 

2. An invertible classical calculus for classical propositional logic

3. Constructive reasoning 

4. Intuitionistic sequent calculus

5. Admissibility of contraction and cut 

6. Consequences of cut elimination 

7. Completeness 

8. Quantifiers in natural deduction and in sequent calculus 

9. Completeness of classical predicate logic

10. Variants of sequent calculi

11. Structural proof analysis of axiomatic theories, with examples from algebra, geometry, lattice theory.

12. The constructive content of classical proofs

13. Labelled calculi for modal and non-classical logics.

 

 

RECOMMENDED READING/BIBLIOGRAPHY

In addition to articles and notes that will be made available on AulaWeb, the following textbooks will be used:

S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press 2001.

S. Negri and J. von Plato, Proof Analysis, Cambridge University Press 2011.

A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory, second edition. Cambridge University Press 2000. 

 

 

TEACHERS AND EXAM BOARD

LESSONS

LESSONS START

The timetable for this course is available here: Portale EasyAcademy

Class schedule

The timetable for this course is available here: Portale EasyAcademy

EXAMS

EXAM DESCRIPTION

Evaluation based on exercises carried out during the course and a final presentation on a topic to be agreed with the teacher.

ASSESSMENT METHODS

Evaluation based on exercises carried out during the course and a final presentation on a topic to be agreed with the teacher.

The final assessment will evaluate the acquisition of the ability to use demonstrative tools and methods, to relate theory and its applications, and to present recent publications on proof theory to other participants by synthesizing them and connecting them to the topics covered in the course.