The course of Logical Theories 1 is part of the program in Philosophical Sciences (MA level) and is included among the complementary training activities. The objective of the course is to provide an in-depth understanding of some aspects of the essential issues and debates connected to the field Logical Theories 1. The golas of the course is to acquire a basic knowledge of Zermelo-Fraenkel axiomatic set theory.
teacher profile teaching materials
***************************************
Natural Deduction
Sequent Calculus for Classical Logic (LK) and Intuitionistic Logic (LJ)
Cut elimination for LK and LJ sequent proofs
Sequent calculus for Linear Logic(LL)
Cut Elimination Theorem for LL
Focusing Theorem for LL proofs
Proof Nets
*************************************
(proof-structures, correctness, normalization, adequacy, sequentialization, focusing, complexity)
Pure Multiplicative Proof Nets
Multiplicative and Additive Proof Nets
Multiplicative and Exponenial Proof Nets
Denotational Semantics
https://sites.google.com/view/lm510/
Programme
Sequent Calculus Proofs***************************************
Natural Deduction
Sequent Calculus for Classical Logic (LK) and Intuitionistic Logic (LJ)
Cut elimination for LK and LJ sequent proofs
Sequent calculus for Linear Logic(LL)
Cut Elimination Theorem for LL
Focusing Theorem for LL proofs
Proof Nets
*************************************
(proof-structures, correctness, normalization, adequacy, sequentialization, focusing, complexity)
Pure Multiplicative Proof Nets
Multiplicative and Additive Proof Nets
Multiplicative and Exponenial Proof Nets
Denotational Semantics
Core Documentation
NOTES AND SLIDES AVAILABLE ON THE COURSE WEB PAGEhttps://sites.google.com/view/lm510/
Reference Bibliography
J.-Y. Girard, Proofs and Types AA.VV., Handbook of Linear Logic V. Danos and L. Regnier, The structure of Multiplicatives O. Laurent, Sequentialization of Multiplicative Proof Nets J.-M. Andreoli and R. Maieli, Focusing and proof nets in linear and non-commutative logic R. Maieli, Cut Elimination for Monomial Proof Nets of the Purely Multiplicativeand Additive Fragment of Linear Logic D. Mazza, Attack of the Exponentials C. Retoré, On the relation between coherence semantics and multiplicative proof netsType of delivery of the course
LECTURES WITH EXERCISES in classroom and by streamingType of evaluation
questions and exercises on the topics covered in class with an individual seminar