Logic and Formal Language TheoryModule Advanced Topics in Mathematical Logic for Computer Science
Academic Year 2026/2027 - Teacher: MARIANNA NICOLOSI ASMUNDOExpected Learning Outcomes
The course covers advanced and relevant topics in mathematical logic, a discipline concerned with the systematic formalization and cataloging of valid formal methods for reasoning in mathematics and computer science.
Knowledge and understanding: The aim of the course is to enable students to acquire knowledge that allows them to understand the main characteristics of first-order number theory and second-order logic. In particular, students will gain knowledge regarding significant results such as, for example, Gödel's incompleteness theorems and the boundaries of Diophantine definability.
Applying knowledge and understanding: Students will acquire the necessary skills to apply procedures such as quantifier elimination to prove the decidability of logical theories, as well as Skolemization and Herbrand expansion for developing formal and automated proofs, and to concretely understand features of first-order logic such as semi-decidability. Furthermore, students will be able to identify the logical-structural strategy underlying complex systems of polynomial equations.
Making judgements: Through the study and analysis of concrete examples of formalization and logical deduction, students will consolidate their ability to evaluate the correctness of advanced logical-mathematical solutions. They will also learn to critically interpret the fundamental trade-off between the expressive power of a logic (e.g., the categoricity of second-order logic) and the loss of its fundamental metatheoretic properties (completeness, compactness).
Communication skills: Students will consolidate and improve their communication skills in using the formal language of logic, even regarding advanced topics. They will be able to rigorously describe complex syntactic concepts, both in terms of the arithmetization of syntax (Gödel numbers), in the critical presentation of profound undecidability results, or in the analysis of non-standard semantics (Henkin general structures).
Learning skills: The course provides practical tools and theoretical concepts to independently address and solve advanced, even complex, formalization and inference problems in both theoretical and applied research contexts within mathematics and computer science.
Course Structure
Classroom-taught lessons in which, in addition to the explanation of basic notions and concepts related to the topics covered, several examples and case studies will be presented in order to stimulate classroom discussion and facilitate the understanding of the subjects.
Should teaching be offered in mixed mode or remotely, it may be necessary to introduce changes with respect to previous statements, in line with the programme planned and outlined in the syllabus.
Required Prerequisites
Attendance of Lessons
Detailed Course Content
- First block: Introduction to first-order number theory and a discussion of its relevance, also with regard to Gödel's incompleteness theorems. The theory of natural numbers with successor is presented, proving its completeness and decidability via quantifier elimination; this concrete procedure will be applied to prove the decidability of various logical theories, such as the theory of natural numbers with successor only, the theory with successor and less-than relation, and Presburger arithmetic. Furthermore, a finitely axiomatizable subtheory of number theory will be analyzed, showing its incompleteness and undecidability as a consequence of Gödel's Theorem, followed by the definition and proof of Gödel's second incompleteness theorem.
- Second block: The topic of Diophantine definability in relation to Hilbert's Tenth Problem. A cultural and structural analysis of the problem itself and the fundamental DPRM Theorem (Davis-Putnam-Robinson-Matiyasevich) is provided. During the lectures, Pell's equations and their related step-down lemmas will be examined, utilized as advanced arithmetic tools to control exponential growth. Techniques for combining and compacting Diophantine relations using polynomials and Putnam's trick will also be presented. The module concludes with a critical analysis of the specification of exponentiation with 13 unknowns.
- Third block: Second-order logic and the study of its expressiveness in mathematics and computer science. The focus will be on the analysis of model categoricity and the systematic failure of key metatheoretic properties such as the Compactness and Löwenheim-Skolem theorems. Skolem functions, second-order Skolemization, and the study of many-sorted logic with its reductions are then introduced. To overcome the expressive limitations of standard semantics, general structures and Henkin semantics are introduced in order to restore the completeness theorem. Finally, the coverage extends to automated theorem proving methods through the study of expansion techniques, Herbrand's Theorem, and optimizations of the delta-rule for semantic tableaux.
Textbook Information
1) Herbert B. Enderton. A Mathematical Introduction to Logic, 2nd edition. Academic Press, 2010. pp. VII-317.
2) Melvin Fitting. First-order logic and automated theorem proving, 2nd edition. Springer-Verlag New York, 1996, pp. XVII-326.
Course Planning
| Subjects | Text References | |
|---|---|---|
| 1 | Number theory | Sect. 3.0 of 1) and additional material. |
| 2 | Natural numbers with successor and elimination of quantifiers. | Sez. 3.1. of 1) and additional material. |
| 3 | Semantics of propositional logic. | Sect. 1.2 of 1), Sections 2.3, 2.4 of 2). |
| 4 | Substitution theorems. Normal forms. | Sections 2.5 to 2.8 of 2). |
| 5 | Compactness and decidability. | Sect. 1.7 di 1). |
| 6 | Truth and models. Logical implication. Definability in a structure. Definability in a class of structures. Homomorphism and homomorphism Theorem. | Sect. 2.2 of 1) and Sect. 5.3 of 2). |
| 7 | First order logic: languages, substitutions. | Sections 2.0 and 2.1 di 1) and Sections 5.1, 5.2 and 7.2 of 2). |
| 8 | An axiomatic deductive calculus. | Sect. 2.3 of 1). |
| 9 | Correctness and completeness of the calculus. | Sect. 2.4 of 1). |
| 10 | Finite models. Size of models. First order theories. | Sect. 2.6 of 1). |
| 11 | Number theory. | Sections 3.0 and 3.1 of 1). |
| 12 | Formal systems: semantic tableaux, resolution, Hilbert's axiomatic system, natural deduction. Their correctness and completeness. | Chapters 3,4 and 6 of 2). |
Learning Assessment
Learning Assessment Procedures
Verification of learning can be carried out also in a telematic way, in case the situation would require it.
Final grades will be assigned taking into account the following criteria:
rejected: Basic knowledges have not been acquired. The student is not able to solve simple exercises.
18-23: Basic knowledges have been acquired. The student solves simple exercises and has sufficient communication skills and making judgements.
24-27: All the knowledges have been acquired. the student solves all the proposed exercises making feww errors and has good communication skills and making judgements.
28-30 cum laude: All the knowledges have been completely acquired. The student applies knowledge and has excellent communication skills.
Examples of frequently asked questions and / or exercises
- Define the theory of natural numbers with successor and prove its decidability.
- Prove Gödel's second incompleteness theorem.
- Define the problem of Diophantine definability.
- State and discuss the DPRM Theorem.
- Define the notion of second-order Skolemization and prove its related theorems.
- Define and prove the constructive version of Herbrand's Theorem.
Please note that these questions are purely indicative; the questions actually asked during the exam may vary, even significantly, from those listed here.