Propositional and Predicate Logic

Previous year: ZS 2014/15 EN.
Lecture in Czech: ZS 2015/16 CZ, ZS 2014/15 CZ, ZS 2013/14 CZ

Schedule: Tuesday 14:00-15:30, room S10.
Lecturer: Petr Gregor (gregor(at)ktiml.mff.cuni.cz)
Information on the lecture: 2/2 Zk/Z NAIL062 in SIS

Plan of the lecture
The plan is only preliminary, almost surely it will not be fulfilled.

Introduction
• 06.10. Lecture 1: A brief history, paradoxes, the language of mathematics, relation of syntax and semantics, preliminaries, trees, König's lemma.

Propositional Logic
• 13.10. Lecture 2: Basic syntax and semantics, adequacy of logical connectives, normal forms, 2-SAT.
• 20.10. Lecture 3: Horn-SAT. Semantics in a theory, properties of theories, algebra of propositions. Tableau method - introduction.
• 27.10. Lecture 4: Tableau method: systematic tableau, soundness and completeness. Compactness.
• 03.11. Lecture 5: Hilbert's calculus. Resolution method: soundness and completeness, linear resolution, resolution in Prolog.

Predicate Logic
• 10.11. Lecture 6: Predicate Logic: Basic syntax, instances and variants. Basic semantic, structures. Validity in a structure.
• 17.11. no lecture (state vacation).
• 24.11. Lecture 7: Validity in a theory, models and properties of theories. Substructures, expansion, reduct. Open theories, theorem on constants. Boolean algebras.
• 01.12. Lecture 8: Tableau method in predicate logic: introduction, systematic tableau, equality. Soundness.
• 08.12. Lecture 9: Canonical model, completeness, corollaries. Extensions by definitions.
• 15.12. Lecture 10: Prenex form, Skolemisation, Herbrand's theorem. Resolution method in predicate logic.
• 22.12. Lecture 11: Soundness and completeness of resolution. Hilbert's calculus in predicate logic.

Model theory, decidability, incompleteness.
• 05.01. Lecture 12: Algebraic theories. Elementary equivalence, completeness. Isomorphisms, categoricity. Decidable theories, recursive axiomatizations.
• 12.01. Lecture 13: Undecidability of predicate logic. Arithmetization of syntax, self-reference principle, fixed-point theorem, undefinability of truth. Incompleteness theorems, corollaries.

Recommended literature

• 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.

Exam
The exam consists of an exam test and an oral exam. Details on the form and extent of the exam are specified here. An example of an exam test is here. A prerequisite for the exam is the credit from the seminar. Exam dates will be available in SIS.

Previous exam test: 27.1., 9.2., 11.2.

Consultation hours
Tuesday 17:10 - 18:00 (after the seminar), or by an (email) appointment.

Note
Any comments on inaccuracy or unclear parts of the lecture slides are most welcome.