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.