Introduction to Logic, Spring 2021
Welcome to the Introduction to Logic course!
Let me help you to orient yourself. We will be using
- a Discord server for quick communication (questions about exercises, during the exam etc.)
- the Brightspace forum for discussions that may need a lot of math and longer answers
- a Kaltura channel for instruction videos
- Zoom for live sessions
- Brightspace to organise the learning material, submissions and marks.
The course will be organised as follows. Throughout the semester, I will provide one chapter of lecture notes and a sheet with assignments per week. You will have to study these lecture notes and submit the mandatory weekly homework, see below. Furthermore, I will prepare short, in-depth video tutorials for difficult subjects, where I see fit or upon request. Have a look at the tutorials from last year to get an impression. Finally, we will have every Monday (with a few exceptions) live Q&A sessions, where we can have face-to-face interactions on Zoom. The workgroup timeslot can be used to interact directly with the tutors.
We will have in total 13 weeks, starting Monday, 01 February and ending 17 May. Due to events and holidays, there will be no material to be studied in the weeks of
- Monday, 08 February (Diesviering),
- Monday, 22 March (week with tests), and
- Monday, 05 April (Easter).
The exam and retake are scheduled for Monday, 14 June, 09:00 and Thursday, 15 July, 09:00, respectively.
Please note that private emails tend to get lost! Question, remarks and suggestions should thus be made on Discord (also private chat) and in the Brightspace forum.
Official information about the course can be found in the eProspectus/studiegids. Note that this information is not up-to-date, as of 31 Jan 2021.
Exam
The exam will be more like a small individual project to be completed within 24h. You can see here an example from last year. Note that this exam is subject to change.
Lecture Notes
Due to the difficult situation, I decided to base the course on lecture notes for self-study, complemented with tutorial videos. The lecture notes will be made available weekly here and on Brightspace.
Exercises and Homework
There will be weekly sets of exercises that accommodate the course and that can be worked on during the exercise hours. Out of these sets, one exercise will be mandatory homework and will be worth 30% of the final grade. Home work has to be handed in via Brightspace and submission have to be prepared using LaTeX. A template is available here and on Overleaf. The deadline for the homework will always on Friday and the new assignments will be made available on Monday before the lecture.
1 Introduction
Monday, 01 February, 14:15
- Course Technicalities
- Introduction and History
- Overview
- Preliminaries: Induction [OLP, Ch. 69], Formal Languages and Context-free Grammars
2 Language and Tools of Propositional Logic
Monday, 15 February, 14:15
- Natural language and introduction propositional logic (PL)
- Iteration and induction for formulas
3 Semantics of Propositional Logic
Monday, 22 February, 14:15
- Boolean semantics of propositional logic
- Basic notions: satisfiability, tautology, semantic equivalence
- Some properties of the Boolean semantics
4 Formal Deduction for Propositional Logic
Monday, 01 March, 14:15
- Deductive systems
- Natural deduction (ND) in sequent style (judgements)
- Derivations (proof trees)
- Fitch-style natural deduction
5 Classical Logic, Soundness and Completeness for Propositional Logic
Monday, 08 March, 14:15
- Soundness of ND
- Classical ND (cND) for PL (proof by contradiction)
- Double negation elimination (DNE) and law of excluded middle (LEM)
- Soundness and Completeness of cND for Boolean PL
6 Normal Forms, Automatic Proofs and SAT-Solving
Monday, 15 March, 14:15
- Normal forms and Horn clauses
- SAT-solving algorithms
- Using SAT solvers
7 First-Order Logic
Monday, 29 March, 14:15
- The need for first-order logic (FOL) (robot routing example)
- FOL language (Note that [HR04, Sec. 2.2] and [OLP, Sec. 14.3] do not use the dot after the bound variable in a quantifier and do not use the name signature!)
- Variables and binding (Note that [HR04, Sec. 2.2.3] is based on parse trees, while [OLP, Sec. 14.7] uses a textual description of the functions we use!)
8 Proof Theory of First-Order Logic
Monday, 12 April, 14:15
- Substitution
- Natural deduction for intuitionistic FOL (ND₁)
- Fitch-Style proofs in ND₁
- Natural deduction for classical FOL (cND₁ = ND₁ + Contra)
9 Semantics of First-Order Logic
Monday, 19 April, 14:15
- Models of FOL
- Semantics of terms
- Boolean semantics of formulas
- Substitution lemma
- Soundness
10 Extensions and Limits of First-Order Logic
Monday, 26 April, 14:15
- First-Order logic with equality
- Uniqueness quantifier
- Completeness
- Compactness
- Reachability not expressible
11 Gödel’s Incompleteness Theorem
Monday, 03 May, 14:15
- Expressing provability inside FOL
- Provability logic
- Prove Gödel’s incompleteness theorem using provability logic [Smo77]
12 First-Order Horn Clauses and Automatic Deduction
Monday, 10 May, 14:15
- Automatic Deduction and the Cut-Rule
- First-Order Horn Clauses and Logic Programming
- Uniform Proofs
- Unification
13 Summary and Exam Preparation
Monday, 17 May, 14:15
References
[HR04] Michael R. A. Huth and Mark D. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
[OLP] The Open Logic Project. Release ad7ff0f (2020-01-03)
[BE99] Jon Barwise and John Etchemendy. Language, Proof and Logic, CSLI Publications, 1999.
[Smo77] Craig Smoryński. The Incompleteness Theorems, in Handbook of Mathematical Logic, vol. 90, J. Barwise, Ed. Elsevier, 1977, pp. 821–865.
[Man10] Yu I. Manin. A Course in Mathematical Logic for Mathematicians, Second Edition, 2010.
[Gir11] Jean-Yves Girard. The Blind Spot: Lectures on logic
[NvP01] Sara Negri and Jan von Plato. Structural Proof Theory
[Gal87] Jean H. Gallier. Logic for Computer Science, John Wiley & Sons, 1987.
[BDKLM03] J.F.A.K. van Benthem, H.P. van Ditmarsch, J. Ketting, J.S. Lodder, and W.P.M. Meyer-Viol. Logica voor informatica, derde editie Pearson Education, 2003.
[LS88] J. Lambek and P.S. Scott. Introduction to higher order categorical logic, paperback, Cambridge University Press, 1988.