Propositional and Predicate Logic
Winter semester 2023/24
Previous years: ZS 2022/13 EN, ZS 2021/22 EN (by Jakub Bulín), ZS 2018/19 EN (by Martin Pilát), ZS 2015/16 EN, ZS 2014/15 EN.
Lecture in Czech: ZS 2023/24 CZ (Jakub Bulín).
Schedule: Thursday 9:00-10:30, room S4.
Lecturer: Petr Gregor (gregor(at)ktiml.mff.cuni.cz)
Information on the lecture: 2/2 Ex/C NAIL062 in SIS
Plan of the lecture
The plan is only preliminary. I will try to synchronize with the parallel lecture in Czech.
Introduction
- 05.10. Lecture 1: A brief history, paradoxes, the language of mathematics, relation of syntax and semantics. Basic syntax and semantics of propositional logic. Appendix.
Propositional Logic
- 12.10. Lecture 2: Semantics in a theory, adequacy of logical connectives, normal forms, satisfiability problem, SAT-solvers.
- 19.10. Lecture 3: 2-SAT, Horn-SAT, DPLL. Properties and extensions of theories. Algebra of propositions. Tableau method: introduction.
- 26.10. Lecture 4: Tableau method: proofs, systematic tableau. Soundness and completeness.
- 02.11. No lecture. (Dean's day)
- 09.11. Lecture 5: Compactness. Resolution method. Linear resolution, resolution in Prolog.
Predicate Logic
- 16.11. Lecture 6: Hilbert's calculus in propositional logic. Predicate logic: basic syntax, instances and variants. Semantics, models, theories.
- 23.11. Lecture 7: Substructures, expansion, reduct. Theorem on constants.
- 30.11. Lecture 8: Extensions by definitions. Definability. Tableau method in predicate logic.
- 07.12. Lecture 9: Systematic tableau, equality. Soundness. Canonical model, completeness.
- 14.12. Lecture 10: Löwenheim-Skolem theorem, compactness. Prenex form, Skolemisation, Herbrand's theorem. Resolution in predicate logic.
- 21.12. Lecture 11: Resolution, unification, soundness and completeness. LI-resolution.
Model theory, decidability, incompleteness.
- 04.01. Lecture 12: Hilbert's calculus in predicate logic. Elementary equivalence, completeness. Isomorphisms, categoricity. Axiomatizability.
- 11.01. Lecture 13: Decidable theories, recursive axiomatizations. Undecidability of predicate logic. Fixed-point theorem, undefinability of truth. Incompleteness theorems, corollaries.
Recommended literature
- M. Pilát, Lecture Notes on Propositional and Predicate Logic, 2020.
- A. Nerode, R. A. Shore, Logic for Applications, Springer, 2nd edition, 1997.
- P. Pudlák, Logical Foundations of Mathematics and Computational Complexity - A Gentle Introduction, Springer, 2013.
- J. R. Shoenfield, Mathematical Logic, A. K. Peters, 2001.
- W. Hodges, Shorter Model Theory, Cambridge University Press, 1997.
- W. Rautenberg, A concise introduction to mathematical logic, Springer, 2009.
Tutorials
The lecture is accompanied by tutorials on Thursday 10:40-12:10, room S1 (taught by me), or 14:00-15:30, room S6 (taught by Martin Pilát).
To obtain a credit from tutorials you need at least 120 points. There will be two tests during the semester (each for 45 minutes). The first one (in the mid of semester) will cover propositional logic, the other (at the end of semester) will cover predicate logic. For each test you can obtain max 100 points. Apart from that you can obtain max 20 points for occasional homework(s). At the end of semester it will be possible to write a remedial test that will replace the worst of the previous two test (during the first week of the exam period). There will be no other chances for remedy.
- 05.10. Tutorial 1: Statements expressed in formulas of various orders.
- 12.10. Tutorial 2: Statements into formulas (cont.), semantics in a theory, adequacy, DNF and CNF.
- 19.10. Tutorial 3: 2-SAT and Horn-SAT. Semantics in a theory. Analysis of theories over finite languages.
- 26.10. Tutorial 4: Tableau method in propositional logic.
- 09.11. Tutorial 5: Resolution method in propositional logic.
- 16.11. Tutorial 6: Examples for the midterm test.
- 23.11. Tutorial 7: Midterm test. Basic syntax and semantics of predicate logic.
- 30.11. Tutorial 8: Semantics, substructures, theories, extensions.
- 07.12. Tutorial 9: Extensions, definability.
- 14.12. Tutorial 10: Tableau method in predicate logic.
- 21.12. Tutorial 11: Prenex form, skolemization, resolution.
- 04.01. Tutorial 12: Resolution in predicate logic (cont.). Examples of test problems.
- 11.01. Tutorial 13: Examples of test problems. Final test.
Exam
The exam is oral with written preparation. Requirements for the exam correspond to the syllabus of the course in the extent that has been covered in the lecture. A prerequisite for the exam is the credit from the tutorials. Exam dates will be available in SIS. Details about the exam (questions, format, grading) are specified here.
Consultation hours
Thursday from 13:00 or by an (email) appointment.