MATHEMATICAL LOGIC

Mathematical logic is a discipline that studies the systematic formalization and  catalogation of valid formal methods for mathematical reasoning problems.

Aim of the course is to present main formal instruments  for reasoning in various ambits of mathematics. Students will acquire the capability of translating claims from the natural language in formal language, also through examples and concrete case studies in several ambits of mathematics. Moreover, they will gain a satisfactory knowledge of syntactic and semantic aspects of propositional and predicative logic, via the study of basic notions of model theory and proof theory.  

General educational objectives in terms of expected learning results.

Knowledge and understanding: the course aims to deliver knowledge that enables students to understand syntactic and semantic aspects of propositional and predicative logic, specifically, students will acquire familiarity with several first order theories and formal proof systems such as axiomatic Hilbert's systems and semantic tableaux.

Applying knowledge and understanding: students will acquire sufficient skills to translate claims from natural to formal language, to use main formal proof systems with the aim of verifying logic consequence relationships in the ambit of propositional logic and theories of first order logic.

Making judgements: Studying and analysing concrete examples of formalization and logic deduction, students will acquire the capability of understanding correctness of proposed solutions and of using autonomously solutions able to guarantee a correct formal representation and proof of complex case studies.

Communication skills: students will acquire adequate communication abilities and expressive appropriateness in the use of formal language of logic in several mathematical ambits, both theoretical and applicative.

Learning skills: the course has the aim to provide students practical tools and theoretical notions to tackle and autonomously solve new formalizations and inference questions in mathematics.       

Teaching organization
total study 150 hours
103 hours of individual study
35 hours of frontal lectures

12 hours of exercises

Classroom-taught lessons in which, in addition to basic notions and concepts concerning formalization and proof in propositional and first order logic, several examples and case studies will be presented in order to stimulate discussions in class and make the understanding of the arguments easier. 

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.

No prerequisite.

The course introduces the syntax, the semantics, and main characteristics of propositional and first-order logic. It considers questions concerning decidability, definability, and first-order structures, it presents principal formal proof methods such as semantic tableaux, resolution, natural deduction, and axiomatic systems of Hilbert.

DETAILED CONTENT

Introduction to the course. Definition of sets by induction. Principle of structural induction. Definition of functions by recursion.

Syntax of propositional logic. Construction of the language of propositional logic. Principles of structural induction and recursion. Notion of subformula.

Semantics of propositional logic. Connectives, Boolean evaluations. Tautologies, satisfiable formulae, and satisfiability of sets of formulae. Theorem of semantic deduction. Notion of duality for binary connectives. Theorem of Compactness for propositional logic.

Theorems of substitutions. Negation normal form. Smullyan’s uniform notation. Generalized conjunctions and disjunctions. Literals, clauses, dual clauses, Conjunctive Normal Form, Disjunctive Normal Form. 

Decidability of propositional logic.

First-order logic: languages, substitutions. Truth and models. Logical implication. Definability in a structure.

Definability in a class of structures.

Homomorphisms and homomorphism Theorem. 

An axiomatic deductive calculus. Correctness and completeness of the calculus. 

Finite models. Size of models. Loewenheim-Skolem Theorem. 

First order theories. Examples. Number theory. Elimination of quantifiers. Representable relations and functions. Arithmetization of Syntax. Incompleteness and undecidability. 

Formal systems: semantic tableaux, resolution, Hilbert's axiomatic systems and natural deduction, their correctness and completeness.  

 

1) Herbert B. Enderton. A Mathematical Introduction to Logic, 2^nd edition. Academic Press, 2010. pp. VII-317.

2) Melvin Fitting. First-order logic and automated theorem proving, 2^nd edition. Springer-Verlag New York, 1996, pp. XVII-326. 

The exam consists of a written test, in which the student is invited to solve some exercises, and an oral test on the arguments explained in class.  

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. 

1) Prove that a first order formula is a logical consequence of a set of first order formulae (the student can be asked to apply a specific proof method: tableaux, natural deduction...)

2) Show that a sentence is finitely valid. 

3) Prove the Compactness Theorem for propositional logic. 

4) Prove the Homomorphism Theorem. 

5) Prove the Loewenheim-Skolem Theorem. 

6) When is a theory axiomatizable? When is it finitely axiomatizable? Provide examples.