Aldo Ursini
University of Siena - Dipartimento di Ingegneria dell'Informazione e Scienze Matematiche

Course Type

Type B

Calendar

17, 18, 19, 20 , 24, 25, 26 Giugno ore 10-13.
Presso Pian dei Mantellini 44

Room

Program

Proof Theory is that part of mathematical logic which investigates the notion of
proof (deduction) in formal systems of logic. The course will deal with:
Natural Deduction and Sequent Calculus for classical and intuitionistic Logic.
Theorem of cut-elimination in sequent calculus and its consequences. The
typed Lambda calculus and the paradigm "proof-as-programs" known as Curry-Howard
isomorphism. Theorem of Church-Rosser and theorem of strong normalization (uniqueness
of result and termination for the proof-as-programs).