Welcome to the Introduction to Logic course!

Let me help you to orient yourself. We will be using Brightspace for information and to organise the learning material, submissions and marks. If you still have some questions after reading the information on Brightspace and the course material, then please contact us via one of the following channels. Please do not send private emails, unless otherwise agreed, as they tend to get lost.

• Use the Brightspace forum for group communication (questions about exercises, during the exam etc.);
• Use the the e-mailbox 2124-S2 Introduction to Logic <itl24@liacs.leidenuniv.nl> for individual requests.

The course will be organised as follows. Throughout the semester, there are 13 lectures and exercise classes, see the Course Schedule for details. For every exercise class, we will distribute an assignment with practice assignments and mandatory homework. You will have to submit at least half of the homework assignments, and the grade of the homework is part of your final grade, see Exercises and Homework for details. During the exercise classes you can work on the assignment and get help from the tutors.

The lectures are complemented by a set of lecture notes, but it is expected that you come to the lectures as the information provided there is not necessarily identical to the lecture notes and, more importantly, it is during the lectures that we interactively try to resolve your questions.

The course will end with an exam, which makes the bulk of your final grade, see the Exam section below.

Course Schedule

The lectures take place weekly on Tuesdays at 13:15, except on 26 March and 14 May, see the table below for a detailed list. Moreover, the 14th lecture does not provide new content but is meant for a summary and exam preparation. Finally, MyTimetable shows another lecture scheduled for 28 May but we will only use that time slot in case something goes wrong (like illness). The exercise class follows the corresponding lecture on Monday at 15:15 in the following week, and the homework will be due on the Friday of that week. This means that there is a large time gap between the lecture and the corresponding exercise class, but this is how the time slots were scheduled for us. The locations are

• Gorleaus C4/5 for the lectures, and
• various rooms in the Gorleaus, Huygens and Oort buildings for the exercise classes (see the Practical Rooms below).

Here is the timetable of the course, numbered by week:

Practical Rooms

The following table shows the detailed list of rooms where exercise classes take place and which exercise group is assigned to each. Please consult the table carefully, as rooms are booked differently per week. The rooms starting with “H” are in the high Huygens building, “Sitter” is the Sitterzaal in the Oortbuilding, and C1 and C3 are in the Gorleaus building.

Lectures and Lecture Notes

The lectures take place on Mondays in the 5th block (17:15 – 19:00) Gorleaus C4/5. The course is based on lecture notes that should be studied before the lectures. On the above page, you will find always the current release on the top and you can download the PDF by clicking on “Compiled PDF”.

Exercises and Homework

There will be weekly sets of exercises that accommodate the course and that can be worked on during the exercise classes. The exercise classes take place on Mondays in block 4 (15:15 – 17:15) in Gorleaus C1 and C3.

Out of exercise 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, see instructions on Brightspace. A template is available here and on Overleaf. The exercise sheets and deadlines will be made available on Brightspace.

We will also use he Proof Rondo first-order logic proof checker that for formalising Fitch-style proofs in the course.

Exam

The exam and retake take place online are scheduled for

• Fri, 07 Jun, 09:00 and
• Thu, 04 Jul, 09:00, respectively.

Details will follow.

Lectures

Lecture 1

Introduction and history, syntax of propositional logic (PL), translating natural language to formulas, parse trees, subformulas

Lecture 2

Deductive systems, natural deduction (ND) in sequent style, derivations (proof trees), machine-checked proofs

For practising derivations with proof trees, you can download the Android application CoolProof. A direct download for the package Android package is available on Brightspace.

Lecture 3

Fitch-style natural deduction, truth tables, satisfiability, tautologies, classical ND (cND) for PL (proof by contradiction)

Lecture 4

Intro first-order logic (FOL): motivation, language, variables and binding

Lecture 5

Proof Theory of FOL, Substitution, natural deduction for intuitionistic FOL (ND₁) and classical FOL (cND₁), Fitch-Style proofs in ND₁

Lecture 6

Machine-checked proofs and proof-assistants for FOL, unification

The system Jape is extremely powerful for exploring proofs and to produce counterexamples, it supports custom logical systems, and it has a large database of example problems that you can use for additional practice. After downloading and starting it, go to File → Open and load I2L.jt from the folder examples/natural_deduction in your Jape installation folder. This will show you a bunch of conjectures in different windows. The sequents in the window “Conjectures” are provable in ND, those in the window “Classical conjectures” require cND. Pick one conjecture and try to prove it in Fitch-style on paper. Then fill in the proof in Jape to see if your proof is correct. Note that Jape uses box style proofs, which is the same as Fitch-style only that a flag is replaced by a box. Moreover, the rule (Assum) from the lecture is found under the menu item “hyp”. In case of questions about Jape, please consult the manual.

Lecture 7

Proof normalisation, Herbrand’s theorem, First-Order Horn Clauses for Automatic Deduction

Lecture 8

Labelled trees and their induction principles, iteration and induction for formulas

Lecture 9

FOL with equality including natural deduction system ND₁ and cND₁, uniqueness quantifier

Lecture 10

Models of FOL, Semantics of terms, Boolean semantics of formulas, Substitution lemma, soundness

Lecture 11

Semantic equivalence, completeness for cND₁, compactness, Reachability not expressible

Lecture 12

Computable functions, axiomatisations, primitive recursion and primitive recursive arithmetic

Lecture 13

Expressing provability inside FOL, Gödel’s Incompleteness Theorems

Lecture 14

Summary and exam preparation

Lecture 15

Backup if delay occurs somewhere

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.