Propositional and Predicate Logic
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.
This is the log of past lectures. "LN" refers to the lecture notes mentioned above.
|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
- 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 19 in LN).
- Tableau method in propositional logic: systematic tableau (being finished, finiteness) (page 25), soundness (Theorem 4), completeness (Theorem 5), compactness (Theorem 6), corollaries (pages 27-28).
- Resolution in propositional logic: soundness (Theorem 7), completeness (Theorem 8), LI-resolution (completness for Horn clauses) (Theorem 9).
- Semantics of predicate logic: theorem on constants (Theorem 10), open theories (page 46), deduction theorem (page 57).
- Tableau method in predicate logic: systematic tableau (finished, finite) (page 53), role of axioms of equality (pages 53-54), soundness (Theorem 11), canonical model (with equality) (page 56), completeness (Theorem 12).
- Löwenheim-Skolem theorem (Theorem 13). Compactness theorem and corollaries (Theorem 14 + page 58).
- Extensions by definitions (page 59), Skolem’s theorem (Theorem 15), Herbrand’s theorem (Theorem 16).
- Elementary equivalence, isomorphism and semantics. Corrolaries of Löwenheim-Skolem theorem (pages 72-73).
- ω-categoricity (Theorem 19).
- Conditions for open (page 77) 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.
- A. Nerode, R. A. Shore, Logic for Applications, Springer, 2nd edition, 1997.
- P. Pudlák, Logical Foundations of Mathematics and Computational Complexity - A Gentle 3. 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.
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.
|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)|