Propositional and Predicate Logic

In this semester, I teach only the Czech version of the seminar. The information on this page was relevant for year 2018/2019. For current information check the webpages of Jakub Bulín and Petr Gregor.

Lecture

The topics from the lecture will be covered in the lecture notes (GitHub repository, pdf). These were written last year and some small changes may happen this year. If you find any errors in the lecture notes, or if you believe some parts could be explained better, let me know.

You may also be interested in the presentations and other information from last year on Petr Gregor’s web.

Past Lectures

This is the log of past lectures. “LN” refers to the lecture notes mentioned above.

Date Topic
October 4, 2018 Introduction, propositional logic - formulas (LN pages 1-13)
October 11, 2018 Propositional logic - formulas, models, normal forms (LN pages 13-17)
October 18, 2018 Propositional logic - normal forms, theories, SAT solvers (glucose) (LN pages 17-18)
October 25, 2018 Propositional logic - theories, analysis of finite theories, 2-SAT (LN pages 18-21)
November 1, 2018 Propositional logic - tableau method, soundness, completeness (LN pages 23-29)
November 8, 2018 Compactness. Resolution method - soundness and completeness, linear resolution (LN pages 29-35)
November 15, 2018 Completeness of LI resolution for Horn formulas, introduction to predicate logic - basic syntax (LN pages 35-44)
November 22, 2018 Open Day - lecture cancelled
November 29, 2018 Predicate logic - semantics, theories, substructures (LN pages 44-49)
December 6, 2018 Predicate logic - tableau method, systematic tableau (LN pages 51-55)
December 13, 2018 Predicate logic - theorem on constants, soundness and completeness of tableau method (LN 55-59)

Exam

The exam consists of an exam test and an oral exam. A prerequisite for the exam is the credit from the seminar. Details will be added later.

The exam test covers most of the topics we did during the lecture/seminar except

• Hilbert’s systems (neither at oral exam)
• LD, SLD resolution, SLD trees (neither at oral exam)
• Programs in Prolog (neither at oral exam)
• (Un)decidability and incompleteness

Some examples of the test are available on Petr Gregor’s web from past years.

Oral exam takes approximately 20 minutes and contains definitions, algorithms and constructions, statements of theorems, and a proof of a specified theorem or lemma.

The proof of the following lemmas/theorems are at the oral exam:

• Cantor’s theorem (Theorem 1), König’s lemma (Lemma 1).
• Algorithms for 2-SAT (Theorem 3) and Horn-SAT (correctness) (page 21 in LN).
• Tableau method in propositional logic: systematic tableau (being finished, finiteness) (page 27), soundness (Theorem 4), completeness (Theorem 5), compactness (Theorem 6), corollaries (pages 30).
• Resolution in propositional logic: soundness (Theorem 7), completeness (Theorem 8), LI-resolution (completeness for Horn clauses) (Theorem 9).
• Semantics of predicate logic: theorem on constants (Theorem 10), open theories (page 48), deduction theorem (page 59).
• Tableau method in predicate logic: systematic tableau (finished, finite) (page 55), role of axioms of equality (pages 55-56), soundness (Theorem 11), canonical model (with equality) (page 58), completeness (Theorem 12).
• Löwenheim-Skolem theorem (Theorem 13). Compactness theorem and corollaries (Theorem 14 + page 60).
• Extensions by definitions (page 61), Skolem’s theorem (Theorem 15), Herbrand’s theorem (Theorem 16).
• Elementary equivalence, isomorphism and semantics. Corrolaries of Löwenheim-Skolem theorem (pages 74-75).
• ω-categoricity (Theorem 19).
• Conditions for open (page 79) and finite axiomatizability (Theorem 20).
• Invariance of definable sets to automorphisms (Lemma 12).

Note: The numbers of Theorems and Lemmas correspond to the lecture notes. The page numbers reference the pages in the lecture notes, where the propositions/observations/corollaries that are not explicitly labeled as a “lemma” or a “theorem” are mentioned and proved in the notes. The references should help you to find the specific theorem/lemma/… in the lecture notes, however, you should still understand the rest of the lecture. You should know all the definitions, lemmas and theorems mentioned in the lecture notes but other proofs are not required. For example, you should know how resolution in predicate logic works and be able to define/describe it, even though it is not mentioned in the list above, but you do not need to know the proof of its soundness and completeness.

1. A. Nerode, R. A. Shore, Logic for Applications, Springer, 2nd edition, 1997.
2. P. Pudlák, Logical Foundations of Mathematics and Computational Complexity - A Gentle 3. Introduction, Springer, 2013.
3. J. R. Shoenfield, Mathematical Logic, A. K. Peters, 2001.
4. W. Hodges, Shorter Model Theory, Cambridge University Press, 1997.
5. W. Rautenberg, A concise introduction to mathematical logic, Springer, 2009.

Seminar

Credit requirements

There will be two tests during the term (one on propositional and one on predicate logic). It will be possible to get 10 points for each test. There will also be 3 homework assignments, each for 2 points. In order to obtain the credit for the seminar (which is required before you can take the exam), you need to obtain at least 16 points.

Homeworks

1. k-colorable graphs and SAT - deadline October 31, in the evening, see linked zip for details.

2. propositional logic - deadline is November 13, in the evening, see the linked pdf for questions

3. predicate logic - deadline is January 3, before the seminar, see the linked pdf for questions

Exercises from the seminar

We will mostly use the exercises from Petr Gregor’s seminar.

Date Topic
October 4, 2018 Introduction, syntax vs. semantics, propositional formulas vs first-order and higher-order formulas (PG seminar 1, exercise 1-2)
October 11, 2018 Formulas with a given meaning in propositional, and first-order languages, adequacy of sets of connectives, CNF and DNF using models (PG seminar 1, ex. 3, 5, 6, and seminar 2, ex. 5, 6)
October 18, 2018 Adequacy, CNF and DNF, HornSAT (PG seminar 2)
October 25, 2018 Implication graph (PG seminar 3, ex. 3, 5, and 9)
November 1, 2018 Tableau method in propositional logic (PG seminar 4, ex. 3-5)
November 8, 2018 Compactness. Resolution (PG seminar 5, ex. 4, 5, 6a, 8)
November 15, 2018 LI-resolution, Hilbert calculus, basics of syntax in predicate logic. (PG seminar 6, ex. 1, 4-6)
November 22, 2018 Open Day - seminar cancelled
November 29, 2017 First test
December 6, 2017 Semantics of predicate logic, structures, substructures (PG seminar 7, ex. 4-8)
December 13, 2017 Structures, substructures, tableau method in predicate logic (PG seminar 8, ex. 9-11, and seminar 9, ex. 2 and 4)