LOGIC
- Overview
- Assessment methods
- Learning objectives
- Contents
- Full programme
- Bibliography
- Teaching methods
- Contacts/Info
For a proficient learning of this course, the student has to master the mathematical notions and the proving techniques taught in the fundamental course in Algebra and Geometry during the first year, which is, in a any case, compulsory to pass before taking this examination.
The objective of the examination is to ascertain the acquiring of the pieces of knowledge and abilities described in the section “Learning Objectives”, evaluating the level of knowledge and the ability to apply the notions and the proving techniques seen during the course.
The examination is written and it is divided into three parts: (part A) two questions about the presentation and the application of the notions illustrated in the course; (part B) proof of one of the theorem explained during the course; (part C) two exercises similar to the one described during the course.
The final mark will be determined for the 30% from the knowledge of the definitions and the ability to apply them (part A), for the 30% from the knowledge and understanding of the proofs of theorems (part B), for the 40% from the capacity to apply the notions learned in the course to the solution of exercises (part C).
The final mark is expressed in thirtieths.
Learning Objectives
The course aims at providing the knowledge about the basic mechanisms of logical inference, by studying the fundamental notions of classical propositional and first order logic, These pieces of knowledge are directed toward forming and increasing the information abstraction ability using symbolic representations, and thus the ability to understand an abstract scientific language. Some more specialised subjects and tools will be sketched, such as program correctness and functional programming.
Learning Outcomes
The expected learning outcomes are the ability to detect errors and mistakes in a scientific argument, to possess a language competence high enough to state a theorem and describe its proof. Specifically, at the end of the course, the student is expected to acquire the following abilities:
1. to perform simple mathematical proofs in a formal system among the ones explained;
2. to perform proofs about a formal system among the ones illustrated in the course;
3. to relate proofs and computations.
The knowledge of the logical mechanisms of mathematical reasoning allows to acquire adequate abilities to deepen personal knowledge and to foster the personal development of new competencies.
A. Introduction
A1. Administrative and bureaucratical aspects, history of logic, relation with Computer Science. (2 hours)
B. Propositional Logic
B1. Structural induction, syntax, natural deduction (2 hours)
B2. Examples of formal derivations
B3. Truth table semantics, minimal sets of connectives, disjunctive and conjunctive normal forms, satisfiability (4 hours)
B4. Boolean algebras (2 hours)
B5: Soundness theorem, schema of the proof, and correctness of simple programs (2 hours)
B6. Completeness (2 hours)
C. First Order Logic
C1. Syntax, substitution, natural deduction (2 hours)
C2. Examples of derivation, examples of formalisation (2 hours)
C3. Tarski semantics, soundness theorem (2 hours)
C4. Resolution, unification, logical programming by examples (4 hours)
D. Simple Theory of Types
D1. λ-calculus, reductions (2 hours)
D2. Examples: data types in the λ-calculus; functional programming (4 hours)
D3. Simple theory of types, syntax, reductions (2 hours)
D4. Intuitionistic propositional logic, syntax, expressive power (2 hours)
D5. Curry-Howard isomorphism, proofs as programs, correctness by construction, strong normalisation, program termination (2 hours)
E. Limiting Results
E1. Compactness theorem, examples of non-standard models (2 hours)
E2. Peano arithmetic, coding (2 hours)
E3. Fixed point lemma, Gödel’s incompleteness theorem. (2 hours)
E4. Computable functions, Church-Turing thesis, Cantor’s theorem, existence of non-computable functions (2 hours)
E5. Non-computability and incompleteness, example: graph minors (2 hours)
With respect to the learning objectives,
- part A1 is specifically devoted to form the scientific language needed to start the course; this language will be improved in all the other parts;
- parts B1, B3, B5, C1, C3, D4, D5, E2, and E3 are mainly directed to form the knowledge about logical inference, with parts B2 and C2 specifically oriented toward the formation of the ability to perform formal proofs;
- parts B4, B5, B6, C3, D1, D3, D5, E1, E2, E3 and E5 are directed to form the competencies about formal abstraction, with some interaction with the previous learning objective when it is needed to link the abilities;
-parts B3, B5, C4, D2, D5 and E4 are deputed to strengthen the previous learning objectives in the Computer Science domain.
A. Introduction
A1. Administrative and bureaucratical aspects, history of logic, relation with Computer Science.
B. Propositional Logic
B1. Structural induction, syntax, natural deduction
B2. Examples of formal derivations
B3. Truth table semantics, minimal sets of connectives, disjunctive and conjunctive normal forms, satisfiability
B4. Boolean algebras
B5: Soundness theorem, schema of the proof, and correctness of simple programs
B6. Completeness
C. First Order Logic
C1. Syntax, substitution, natural deduction
C2. Examples of derivation, examples of formalisation
C3. Tarski semantics, soundness theorem
C4. Resolution, unification, logical programming by examples
D. Simple Theory of Types
D1. λ-calculus, reductions
D2. Examples: data types in the λ-calculus; functional programming
D3. Simple theory of types, syntax, reductions
D4. Intuitionistic propositional logic, syntax, expressive power
D5. Curry-Howard isomorphism, proofs as programs, correctness by construction, strong normalisation, program termination
E. Limiting Results
E1. Compactness theorem, examples of non-standard models
E2. Peano arithmetic, coding
E3. Fixed point lemma, Gödel’s incompleteness theorem.
E4. Computable functions, Church-Turing thesis, Cantor’s theorem, existence of non-computable functions
E5. Non-computability and incompleteness, example: graph minors
The slides of the lessons in pdf format are available on the course website, and they constitute the reference text. The additional bibliography is suggested but not compulsory, and it is cited in the last slide of every lesson.
On the same website, a collection of exercises and their solutions are available.
Conventional frontal lecture in Italian with slides and blackboard.
The teaching objectives are pursued as follows:
1. each of the five chapters of the course will be introduced by a general discussion to relate the topics to the other mathematical and computer science subjects, and to illustrate the philosophical meaning of what is going to be explained.
2. the fundamental definitions and theorems will be illustrated to provide a solid and well organised mathematical framework.
3. examples will complement the particularly relevant results, both to clarify their meaning, and to illustrate their applications.
4. the parts which need (the formal proofs) will be complemented with exercises to be solved in the classroom by the lecturer, with an emphasis on the techniques to solve them.
5. at the end of each chapter, a summary of what has been achieved is given, to provide the right perspective to critically evaluate the results, both with respect to their inner mathematical meaning, and with respect to what has been acquired in other courses.
The course website is: https://marcobenini.me/lectures/logica-informatica/
Student reception is by appointment to fix by email. The teacher will answer to email from the official university account of the sender only. If needed, the appointment could be done online.