MATHEMATICAL LOGIC
Academic Year 2023/2024 - Teacher: MARIANNA NICOLOSI ASMUNDOExpected Learning Outcomes
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.
Course Structure
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.
Required Prerequisites
Attendance of Lessons
Detailed Course Content
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.
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 | Induction and recursion. | Sect. 1.4 of 1). |
2 | Syntax of propositional logic. | Sect. 1.1. of 1), Sect. 2.2 of 2). |
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 | First order logic: languages, substitutions. | Sections 2.0 and 2.1 di 1) and Sections 5.1, 5.2 and 7.2 of 2). |
7 | 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). |
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. Elimination of quantifiers. | Sections 3.0, 3.1 and 3.2 of 1). |
12 | Repreentable relations and functions | Section 3.3 of 1). |
13 | Arithmetization of syntax | Section 3.4 of 1). |
14 | Incompleteness and Undecidability. | Section 3.5 of 1). |
15 | 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
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.