Salta al contenuto principale della pagina

PROOF THEORY

CODE 107014
ACADEMIC YEAR 2021/2022
CREDITS
  • 5 cfu during the 2nd year of 9011 MATEMATICA(LM-40) - GENOVA
  • SCIENTIFIC DISCIPLINARY SECTOR MAT/01
    TEACHING LOCATION
  • GENOVA
  • SEMESTER 2° Semester
    TEACHING MATERIALS AULAWEB

    OVERVIEW

    Proof theory  is the branch of mathematical logic aimed at the study of proofs intended as mathematical objects, usually presented as inductively generated tree structures.

    Proof theory, in addition to being one of the pillars of the foundations of mathematics, together with model theory, axiomatic set theory, computability theory, and category theory, plays a primary role in the theory of programming languages.

    AIMS AND CONTENT

    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.

    AIMS AND LEARNING OUTCOMES

    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.

     

    PREREQUISITES

    An introductory logic course

    TEACHING METHODS

    Traditional lectures

    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

    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

    Exam Board

    SARA NEGRI (President)

    RICCARDO CAMERLO

    GIUSEPPE ROSOLINI (President Substitute)

    LESSONS

    Class schedule

    All class schedules are posted on the EasyAcademy portal.

    EXAMS

    ASSESSMENT METHODS

    Valutazione basata su esercizi svolti durante il corso ed una presentazione finale su una tematica da concordare con la docente.