The course aims to provide knowledge of classical and intuitionisitic logic (propositional and first order), and of lambda calculus and type theory. At the end of the course the students must demonstrate to have the necessary knowledge to reason within a formal logical system, both in a classical and intuitionisitic setting. This knowledge will allow the student to: i) carry out formal proofs with a deductive system; ii)reasoning with axiomatic systems. Moreover the students will have to know how to transfer the theoretical notions learned in logical contexts typical of computer science, such as the type systems for functional languages. Students will be able to continue their studies in the field of computer science logic.
1.Propositional logic:
-propositions and connectives
-semantics
-natural deduction
-soundness and completeness
2. Predicate logics:
-quantifiers
-structures
-similarity types
-semantics
-identity
-natural deduction
-soundness and completeness
3. normalization in natural deduction.
4. confluence.
5. basic model theory
- equivalence,
- isomporphism.
6. lambda calculus without types and with types.
7. the sequent calculus and the cut elimination theorem.
8, peano Arithmetic
-first and second incompleteness theorems
| Author | Title | Publisher | Year | ISBN | Note |
| Jean Louis Krivine, Rene Cori | Lambda-calculus, Types and Models | Ellis Horwood | 1993 | 978-0130624079 | |
| van Dalen, Dirk | Logic and Structure. (Edizione 5) | Springer | 2013 | 978-1-4471-4557-8 |
Written examination
