Propositional and Predicate Logic

Winter semester 2025/26

Previous years: ZS 2024/25 EN.
Lecture in Czech: ZS 2025/26 CZ (Jakub Bulín).

Schedule: Tuesday 15:40-17:10, room S3.
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

30.09. Lecture 1: Introduction to logic: history, paradoxes, relation of syntax and semantics. Propositional logic: basic syntax and semantics. Appendix.

Propositional Logic

07.10. Lecture 2: Semantics in a theory. Universality of logical connectives, normal forms. Properties and extensions of theories.
14.10. Lecture 3: Algebra of propositions. Satisfiability problem, SAT-solvers. 2-SAT, Horn-SAT, DPLL. Tableau method: introduction.
21.10. Lecture 4: Tableau method: proofs, systematic tableau. Soundness and completeness. Compactness.
28.10. no lecture (state holiday)
04.11. Lecture 5: Resolution method, soundness and completeness. Predicate logic: basic syntax.

Predicate Logic

11.11. Lecture 6: Semantics of predicate logic, models, theories. Substructures, expansions, reducts.
18.11. Lecture 7: Extensions of theories, extensions by definitions. Definability. Tableau method in predicate logic.
25.11. Lecture 8: Systematic tableau, equality. Soundness. Canonical model, completeness.
02.12. Lecture 9: Löwenheim-Skolem theorem, compactness. Prenex form, Skolemisation, Herbrand's theorem. Resolution in predicate logic.
09.12. Lecture 10: Resolution, unification, soundness and completeness. Resolution in Prolog. Hilbert's calculus in predicate logic.

Model theory, decidability, incompleteness.

16.12. Lecture 11: Elementary equivalence, completeness. Isomorphisms, categoricity. Axiomatizability.
06.01. Lecture 12: Recursive axiomatizations and decidable theories. Undecidability of predicate logic. Incompleteness theorems, corollaries.

Recommended literature

J. Bulín, Lecture Notes on Propositional and Predicate Logic, 2025.
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 Wednesday 9:00-10:30, room S11 (taught by me), or on Thursday 15:40-17:10, room S11 (taught by Jakub Bulín).

To obtain a credit from tutorials you need at least 140 points out of max 250 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, and in each test you must obtain at least 40 points. Apart from that you can obtain max 40 points for SAT solver project and 2x5 points for two homeworks. At the end of semester it will be possible to write a remedial test for each test (during the first week of the exam period). If you did not score at least 40 points, you will need to take these remedial test. There will be no other chances for remedy.

01.10. Tutorial 1: Statements expressed in formulas of various orders.
08.10. Tutorial 2: Statements into formulas (cont.), semantics in a theory, universality, DNF and CNF.

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) in the previous year are specified here.

Consultation hours
Tuesday 17:20 (after the lecture), Wednesday 10:40 (after the tutorials), or by an (email) appointment.