Menù principale
B020988 - ADVANCED TOPICS IN LOGIC
Main information
Teaching Language
Course Content
Suggested readings
Learning Objectives
Prerequisites
Teaching Methods
Further information
Type of Assessment
Course program
Academic Year 2018-19
Course year
First year - Second Semester
Belonging Department
Humanities (DILEF)
Course Type
Single education field course
Scientific Area
M-FIL/02 - LOGIC AND PHILOSOPHY OF SCIENCE
Credits
12
Teaching Hours
72
Teaching Term
26/02/2019 ⇒ 07/06/2019
Attendance required
Yes
Type of Evaluation
Final Grade
Course Content
show
Course program
show
Lectureship
Teaching Language
Italian
Course Content
Introduction to Proof Theory
Suggested readings (Search our library's catalogue)
1) Lecture notes by the instructor (accessible online), with a reference
list;
2) for a deeper understanding of several topics touched in the lectures,
see:
(i) J.Y.Girard, Proof Theory and Logical Complexity, Napoli 1987;
(ii) A.S.Troelstra, H.Schwichtenberg, Basic Proof Theory, Cambridge 2000
(2nd ed.);
(iii) S.Negri and J. von Plato, Structural Proof Theory, Cambridge 2001;
(iv) M.H.Sorensen, P.Urczyn, Lectures on the Curry-Howard Isomorphism,
Amsterdam-New York 2006;
(v) H.Schwichtenberg, S.S.Wainer, Proofs and Computations, Cambridge
2012.
list;
2) for a deeper understanding of several topics touched in the lectures,
see:
(i) J.Y.Girard, Proof Theory and Logical Complexity, Napoli 1987;
(ii) A.S.Troelstra, H.Schwichtenberg, Basic Proof Theory, Cambridge 2000
(2nd ed.);
(iii) S.Negri and J. von Plato, Structural Proof Theory, Cambridge 2001;
(iv) M.H.Sorensen, P.Urczyn, Lectures on the Curry-Howard Isomorphism,
Amsterdam-New York 2006;
(v) H.Schwichtenberg, S.S.Wainer, Proofs and Computations, Cambridge
2012.
Learning Objectives
Understanding the notion of 'proof' in the light of fundamental developments of metalogic since 1930 together with the associated techniques of cut-elimination and normalization.
Prerequisites
An introduction to Logic (12 CFU), BA in Philosophy
Teaching Methods
Lectures, possibly with tutorials for exercises; attendance of the research seminar
Further information
Normal students are supposed to attend at least 2/3 of the class lectures. Part-time students (or those having special problems) are required to directly get in touch with the instructor. For further news and last minute infos, see the lecturer's UNIFI-web page
the web page of DILEF.
e-mail: andrea.cantini@unifi.it.
the web page of DILEF.
e-mail: andrea.cantini@unifi.it.
Type of Assessment
Oral examination, 45 minutes, three questions: it is aimed at witnessing an adequate mastering of (i) the basic theoretical notions and disciplinary lexicon, (ii) the logical techniques needed to solve exercises;(iii) some proof among those of the main results.Emphasis is put on adequate knowledge in Gentzen's formalisms.
The grading is obtained by a simple average over the marks assigned to the single answers.
The grading is obtained by a simple average over the marks assigned to the single answers.
Course program
1) Additional topics in propositional and predicative classical logic:
normal forms, theorems of Herbrand and Skolem; monadic logic.
2) Introduction to proof theory. Gentzen's sequent calculi. Proof of
the Hauptsatz. Application: the interpolation theorem via Maehara's
lemma.
3) Hauptsatz and abstraction: the consistency of Grishin's naive set theory.
4) Introduction to typed lambda calculus. Basic notions and fundamental
properties. Proof of strong normalization.
normal forms, theorems of Herbrand and Skolem; monadic logic.
2) Introduction to proof theory. Gentzen's sequent calculi. Proof of
the Hauptsatz. Application: the interpolation theorem via Maehara's
lemma.
3) Hauptsatz and abstraction: the consistency of Grishin's naive set theory.
4) Introduction to typed lambda calculus. Basic notions and fundamental
properties. Proof of strong normalization.