Course Mathematical Logic 2 2026/2027

info examination

tutorial meeting on request

ANNOUNCEMENTS

PROGRAM

references

INFO on the final examination:
oral examination on a date agreed with prof. Trotta choosing one option among the following ones:

1. discussion about the solutions of some exercises agreed with the lecturers before hand
2. discussion on the whole course program
3. discussion on a report on a specific topic of the course analysed in full details agreed with the lecturers

Tutorial meeting :
in presence or via Zoom
(please send an email with your request to a lecturer).
Please just use your academic email address.

ANNOUNCEMENTS

lecture timetable:
Monday: from 12.30 up to 14.30 in 2BC60 (Torre)
Tuesday: from 12.30 up to 14.30 in 2BC60 (Torre)

Another master-course about logic is the course TYPE THEORY taught in the second semester within the master in Computer Science.
Information are available here

PROGRAM

Categorical Logic : Categories, Doctrines, Free Completions with Applications to Logic



32 hours by Prof. Davide Trotta
16 hours by Prof. Maria Emilia Maietti
1. Basic elements of category theory (first three chapters of the book: F. Borceux, Handbook of Categorical Algebra 1)
2. Lawvere's theory of doctrines for simply typed logic (from A.M. Pitts, Categorical logic. 1995- see references below)
3. Introduction to topos theory: Elementary Toposes (2nd chapter of P. Johnstone, Sketches of an Elephant - A Topos Theory Compendium vol.1, 2002.)
4. Classification and internal language theorems section 7-8-9-10-11-12.1-12.2 Notes on Category Theory
Please write to the author if you find mistakes!

Further material will be posted in the moodle of the course


An introduction to mathematical logic:
Notes on Mathematical Logic 1 by M.E. Maietti

References:

On general category theory:
S. MacLane (1971) Categories for the Working Mathematician (second edition), Springer

Francis Borceaux (1994): Handbook of Categorical Algebra, 1.2,3

P.Johnstone (2002): Sketches of an Elephant A Topos Theory Compendium vol. 1 e 2

Saunders Mac Lane, Ieke Moerdijk (1992) Sheaves in Geometry and Logic. A First Introduction to Topos Theory Springer


On the theory of doctrines:

Lawvere, F. (1969). Adjointness in foundations. Dialectica, 23:281-296.

Lawvere, F. (1970). Equality in hyperdoctrines and comprehension schema as an adjoint functor. In Heller, A., editor, New York Symposium on Application of Categorical Algebra, volume 2, pages 1-14. American Mathematical Society

A.M. Pitts (1995) Categorical logic. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, vol. 6,pages 39-129, OUP
( preprint copy)

"Quotient completion for the foundation of constructive mathematics" M.E. Maietti and Giuseppe Rosolini Logica Universalis,7(3): 371-402, 2013

"Elementary quotient completion" M.E. Maietti and Giuseppe Rosolini Theory and Applications of Categories 27(17):445--463, 2013

On the history of categorical logic:
"The History of Categorical Logic: 1963-1977", Marquis Jean Pierre and Reyes Gonzalo In: Handbook of the History of Logic, vol. 6, pp. 689-800. Elsevier (2011)