LOGICA MATEMATICA

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 and a satisfactory ability in using more widespread formal methods for the verification or the refutation of logic consequence relationships.

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 principal formal systems for reasoning such as semantic tableaux, resolution, natural deduction, and the Davis-Putnam method.

Applying knowledge and understanding: students will acquire sufficient skills to translate claims from natural to formal language, to use systems of formal proof with the aim of verifying logic consequence relationships in the ambit of propositional and 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.

Classroom-taught lessons.

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.

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.

Propositional logic

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.

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

Theorem of Compactness for propositional logic. Decidability of propositional logic.

The method of semantic tableaux: expansion rules and construction. Correctness of tableaux system. Resolution method: expansion rules and the resolution rule. Correctness of the resolution system. Hintikka sets, Hintikka’s Lemma. The Theorem of existence of a model. Proof of completeness for a tableaux system and of propositional resolution. Semantic trees. Saturated sets of clauses. Sets of Robinson. Completeness of the resolution system.

Hilbert’s systems. Theorem of Deduction of Tarski-Herbrand. Correctness and completeness in a Hilbert’s system.

System of natural deduction. Strong correctness and completeness of the system.

Procedure of Davis-Putnam. Correctness of the procedure.

First-order logic

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

Herbrand models. Uniform notation for first-order logic. Principles of structural induction and of structural recursion for first-order logic. First-order Hintikka sets, Hintikka’s Lemma, Theorem of existence of a model for first-order logic. Theorem of Compactness for first-order logic. Theorem of Lowenheim-Skolem.

Semantic tableaux, resolution, Hilbert’s system, and natural deduction for first-order logic, their correctness and completeness.

Skolemization. Theorem of Skolemization. Skolemized and Prenex form.

Herbrand’s Theorem and its constructive form.

Finite models. Size of models. First-order theories.

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.