
Course unit
LOGIC 2
SC02111834, A.A. 2015/16
Information concerning the students who enrolled in A.Y. 2015/16
Mutuating
Course unit code 
Course unit name 
Teacher in charge 
Degree course code 
SC03119738 
MATHEMATICAL LOGIC 2 
MARIA EMILIA MAIETTI 
SC1172 
ECTS: details
Type 
ScientificDisciplinary Sector 
Credits allocated 
Educational activities in elective or integrative disciplines 
MAT/01 
Mathematical Logic 
6.0 
Course unit organization
Period 
First semester 
Year 
1st Year 
Teaching method 
frontal 
Type of hours 
Credits 
Teaching hours 
Hours of Individual study 
Shifts 
Practice 
2.0 
16 
34.0 
No turn 
Lecture 
4.0 
32 
68.0 
No turn 
Examination board
Board 
From 
To 
Members of the board 
8 Logica Matematica 2  a.a. 2019/2020 
01/10/2019 
30/09/2020 
MASCHIO
SAMUELE
(Presidente)
MAIETTI
MARIA EMILIA
(Membro Effettivo)
BONOTTO
CINZIA
(Supplente)
CIRAULO
FRANCESCO
(Supplente)

7 Logica Matematica 2  a.a. 20182019 
01/10/2018 
30/09/2019 
MASCHIO
SAMUELE
(Presidente)
MAIETTI
MARIA EMILIA
(Membro Effettivo)
BONOTTO
CINZIA
(Supplente)
CIRAULO
FRANCESCO
(Supplente)
SAMBIN
GIOVANNI
(Supplente)

6 Logica Matematica 2  2017/2018 
01/10/2017 
30/09/2018 
SAMBIN
GIOVANNI
(Presidente)
MAIETTI
MARIA EMILIA
(Membro Effettivo)
CIRAULO
FRANCESCO
(Supplente)
MASCHIO
SAMUELE
(Supplente)

5 Logica Matematica 2  2016/2017 
01/10/2016 
30/11/2017 
SAMBIN
GIOVANNI
(Presidente)
MAIETTI
MARIA EMILIA
(Membro Effettivo)
BONOTTO
CINZIA
(Supplente)
CIRAULO
FRANCESCO
(Supplente)
MASCHIO
SAMUELE
(Supplente)

4 Logica Matematica 2  a.a. 2015/2016 
01/10/2015 
30/09/2016 
MAIETTI
MARIA EMILIA
(Presidente)
VALENTINI
SILVIO
(Membro Effettivo)
BONOTTO
CINZIA
(Supplente)
CIRAULO
FRANCESCO
(Supplente)
ZANARDO
ALBERTO
(Supplente)

Prerequisites:

It is recommended to have followed an introductory course on logic
but it is not strictly necessary. 
Target skills and knowledge:

Expressive power and theoretical limits of the concept of formal proof.
Differences between classical and constructive reasoning.
Introduction to proof theory of constructive logic and mathematics and their applications to computer science. 
Examination methods:

The final examination will be chosen by the student among one of the following options:
1. oral examination about all the topics in the course;
2. written examination about all the topics in the course;
3. oral talk on a topic agreed with the teacher and deeply investigated by the student together with the presentation of solutions regarding exercises delivered by the teacher during the course. 
Assessment criteria:

The student is required to master the concepts presented in the course by himself/herself.
The student is required to solve some easy exercises to test his
understanding of the grasped concepts and its main properties. 
Course unit contents:

Sequent calculus for classical predicate logic.
Sequent calculus for intuitionistic predicate logic.
Decision procedure for propositional intuitionistic logic.
Constructive proof of Gentzen's cut elimination theorems for both calculi.
Peano arithmetics.
Heyting arithmetics.
Differences between Peano and Heyting arithmetics with respect to formal Church thesis and axiom of choice.
Sketches of proofs about Goedel incompleteness theorems and comparison between proofs for classical and constructive arithmetics.
Realizability (computational) semantics for Heyting arithmetics.
Brief sketched connection between the topics of prooftheory studied before and concepts of category theory and categorical logic. 
Planned learning activities and teaching methods:

The student is required to participate to the lectures actively,
to develop its critical sense together with grasping new notions.
Lectures will be followed by class discussions, exercises to be solved by the students alone and talks given on deep investigations
agreed with the teacher about topics delivered during the course. 
Additional notes about suggested reading:

Syllabus, class exercises, papers for deep investigations provided by the teacher. 
Textbooks (and optional supplementary readings) 

A. S. Troelstra and D. van Dalen, Constructivism in Mathematics. An Introduction. : NorthHolland, 1988. volume I and II

A. M. Pitts, Categorical Logic in Handbook of Logic in Computer Science, vol. 5. Algebraic and Logical Structures.. : Oxford University Press, 2000. Chapter 2

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


