MATHEMATICAL LOGIC
Academic Year 2022/2023 - 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
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. Herbrand Models. Herbrand Theorem.
First order theories. Examples. Hints to non standard analysis. Number theory. Elimination of quantifiers.
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 | Herbrand Theorem and its constructive version. | Sections 8.6 and 8.7 of 2). |
12 | Hints to non standard analysis. | Sez. 2.8 di 1) |
13 | Number theory. Elimination of quantifiers. | Sections 3.0 and 3.1 of 1). |
14 | 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.
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.