Predicate and Propositional Logic > Propositional and Predicate Logic

Propositional and Predicate Logic

Published on Sept. 28, 2016, 9:37 p.m.


The topics from the lecture will be covered in the lecture notes (GitHub repository, pdf). These are currently a work in progress, the goal is to publish a new part every week before the lecture. 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 5, 2017 Introduction, preliminaries (LN pages 1-7)
October 12, 2017 Size of sets, introduction to propositional logic - formulas, models (LN pages 7-13)
October 19, 2017 Normal forms, theories, analysis of finite theories, intro to SAT (LN pages 14-18)
October 26, 2017 2-SAT, HornSAT (proofs), tableau method - tableau (from theory), systematic tableau (LN pages 18-25)
November 2, 2017 Tableau method - soundness, completeness. Compactness (LN pages 25-28)
November 9, 2017 Hilbert systems, resolution method - soundness and completeness, linear resolution (LN pages 28-35)
November 16, 2017 Completeness of LI resolution for Horn formulas, introduction to predicate logic - basic syntax (LN pages 34-43)
November 23, 2017 Open Day - the lecture is cancelled
November 30, 2017 Predicate logic - semantics, theories, substructures (LN pages 43-47)
December 7, 2017 Predicate logic - tableau method, systematic tableau (LN pages 47-53)
December 14, 2017 Predicate logic - theorem on constants, soundness and completeness of tableau method (LN 53-57)
December 21, 2017 Predicate logic - compactness, prenex normal form, Skolem variant, Herbrand model, Herbrand theorem (LN 58-65)
January 4, 2018 Predicate logic - unification algorithm, resolution (only ideas of proofs of soundness and completeness), model theory basics (LN 66-72)
January 11, 2018 Predicate logic - categoricity, axiomatizability, decidability, incompleteness (LN 72-81)


The exam consists of an exam test and an oral exam. A prerequisite for the exam is the credit from the seminar.

Exam test takes 90 minutes and you need to obtain at least 1/2 of the points in order to advance to the oral part. The test covers most of the topics we did during the lecture/seminar, except

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:

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.

Additional reading

  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.


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 and you need to get at least 13 points for both of the tests to get the credit for the seminar.

[Added on Nov. 1, 2017] There will also be two homework assignments. You can get additional points for these (1.5 point for each, 3 points in total).

Exercises from the seminar

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

Date Topic
October 4, 2017 Introduction, syntax vs. semantics, propositional formulas vs first-order and higher-order formulas (PG seminar 1, only exercise 1)
October 11, 2017 Formulas with a given meaning in propositional, first-order, and second-order languages (PG seminar 1)
October 18, 2017 Adequacy, CNF and DNF (PG seminar 2)
October 25, 2017 2-SAT, HornSAT (PG seminar 3)
November 1, 2017 Theories over finite languages, tableau method (PG seminar 4), First Homework (deadline - Nov. 10, 11:55 pm)
November 8, 2017 Dean's sports day (no seminar)
November 15, 2017 Applications of compactness, resolution in propositional logic (PG seminar 5)
November 22, 2017 First test
November 29, 2017 Predicate logic - basic syntax and semantics, validity in a structure, definable sets (PG seminar 6 and 7 - only exercise 3)
December 6, 2017 Structures and substructures, generated structures (PG seminar 8)
December 13, 2017 Extensions of theories, tableau method in predicate logic (PG seminar 9)
December 20, 2017 Prenex normal form, Skolemization, Herbrand models (PG seminar 10)
January 3, 2018 Resolution in first order logic (PG seminar 11)
January 10, 2018 Second test, isomorphism and categoricity, dense linear orders (LN 73-74)