Logic

Overview

Questions regarding the lecture and exercises can be discussed on Zulip. You can subscribe to all Logic-* streams by visiting this stream and clicking the Cheshire Cat emoji.

Note: The lectures of week 2 cannot take place in person. Please watch last year’s recordings, April 20 and April 22 instead.

Prerequesites

The course assumes that you have had a basic introduction to logic already and are familiar with the following topics: syntax and semantics of both propositional and first-order logic; disjunctive and conjunctive normal forms; basic equivalences of propositional and first-order logic. These topics will only be refreshed briefly at the beginning of the course.

Content

Logic is the science of reasoning. It plays an important role in many disciplines, including mathematics (where it originated) and philosophy, but it is particularly central to computer science and sometimes referred to as the calculus of computer science. We emphasise the computational aspects of logic. These are the central topics of the course:

1. We learn how to perform proofs in multiple deductive systems, how to prove the soundness and completeness of a system with respect to a semantics, and how to translate proofs between systems. In particular we cover resolution, natural deduction, sequent calculus and Hilbert systems.
2. We learn about the limitations of first-logic and the relationship between logic and computability.
3. We learn how to solve logical problems algorithmically using (semi-)decision procedures like resolution (for pure logic) and quantifier elimination (for arithmetic).

Lecture Material

Slides

Propositional logic:

• Basics (Esparza/Schöning)
• Equivalences (Esparza/Schöning)
• Normal forms (Esparza/Schöning)
• Definitional CNF (Harrison)
• Horn formulas (Esparza/Schöning)
• Compactness (Harrison)
• Resolution (Esparza/Schöning)
• Basic Proof Theory (Troelstra&Schwichtenberg)
• Sequent Calculus (Troelstra&Schwichtenberg)
• Tableaux Calculus
• Natural Deduction (Troelstra&Schwichtenberg)
• Hilbert Systems (Troelstra&Schwichtenberg)

First-order logic:

• Basics (Esparza/Schöning)
• Normal forms (Esparza/Schöning)
• Herbrand theory (Esparza/Schöning)
• Resolution (Esparza/Schöning)
• Equality (Esparza)
• Undecidability (Cutland)
• Compactness (Harrison)
• The Classical Decision Problem (Harrison)
• Basic proof theory (Troelstra&Schwichtenberg)
• Theories (Harrison)
• Quantifier Elimination (Harrison/Enderton)
• Incompleteness (Schöning)
• Higher-Order Logic

Literature

1. Uwe Schöning. Logik für Informatiker (English: Logic for Computer Scientists).
2. A. Troelstra and H. Schwichtenberg. Basic Proof Theory.
3. Jean Gallier. Logic for Computer Science.
4. John Harrison. Handbook of Practical Logic and Automated Reasoning.
5. Melvin Fitting. First-Order Logic and Automated Theorem Proving.
6. Herbert Enderton. A Mathematical Introduction to Logic.
7. Ebbinghaus, Flum, Thomas. Einführung in die mathematische Logik (English: Mathematical Logic).