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.

• the Discord server for group communication (questions about exercises, during the exam etc.);
• the e-mailbox 2123-S2 Introduction to Logic <itl23@liacs.leidenuniv.nl> for individual requests.

The course will be organised as follows. Throughout the semester, we will have weekly lectures, supported by lecture notes and a weekly sheet with assignments and homework. You will have to follow the lectures, study the lecture notes and submit the mandatory weekly homework, see below. Furthermore, there will be some short, in-depth video tutorials for difficult subjects upon request. Finally, there are weekly exercise classes, during which you can work on the assignments, discuss them and ask questions to the tutors.

We will have in total 13 weeks, starting Monday, 06 February and ending 22 May. There will be no lectures and exercise sessions on

• Monday, 27 March (Test week),
• Monday, 10 April (Easter) and
• Monday, 01 May (Labour Day/School holidays).

The course ends with an exam, which will be held online, see below for details. Exam and retake are scheduled for Monday, 05 June, 09:00 and Monday, 10 July, 09:00, respectively. We may consider moving the retake exam forward, if scheduling allows it.

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.

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 before the lecture (15:15 – 17:15) in Havingazaal and Snellius 312, 403, 407/409, 408 and 412, and in one small online group.

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.

How to Prepare for the Exam?

Most importantly: You need to be able to do the exam without any notes, course material or books. You can use any of those during the exam, but the content is too difficult to actually benefit from them. Notes can help as backup to avoid blanks during the exam, but you need to be able to do the exam from memory. This needs preparation, and thus time and organisation. Here is some help on how to efficiently prepare yourself.

• Practise regularly: Only during sleep does our brain make connections. Practise regularly with the weekly assignments and make your own exercises.
• Take time to concentrate 100% while reading and practising: Switch off your phone and remove distractions (people in the room, social media, websites, …) for practice time. Make every minute count!
• Repeat only something that you can handle and don’t practise difficulties. This does not mean that you should not practise to overcome difficulties but you need to solve your problems before repeating. Approach exercises slowly and take the time to think about what you are doing and be in control. If you practise something wrong 10 times and correctly 2 times, your brain will learn the wrong thing.
• Discuss with others: Make use of the exercise classes to discuss problems and come prepared to classes. Explain the material to others, teaching is the best method of learning.

1 Introduction

Read chapter 1 and appendix of lecture notes.

Monday, 06 February, 17:15

• Course Technicalities
• Introduction and History
• Overview
• Preliminaries: Labelled trees and their induction principles, formal Languages and context-free grammars

2 Language and Tools of Propositional Logic

Read chapter 2 of lecture notes.

Monday, 13 February, 17:15

• Natural language and introduction propositional logic (PL)
• Iteration and induction for formulas

3 Semantics of Propositional Logic

Read chapter 3 of lecture notes.

Monday, 20 February, 17:15

• Boolean semantics of propositional logic
• Basic notions: satisfiability, tautology, semantic equivalence
• Some properties of the Boolean semantics

4a Formal Deduction for Propositional Logic

Read sections 4.1 – 4.3 of lecture notes.

Monday, 27 February, 17:15

• Deductive systems
• Natural deduction (ND) in sequent style (judgements)
• Derivations (proof trees)
• Fitch-style natural deduction

Hint 1: 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.

Hint 2: For practising natural deduction in Fitch-style, download Jape and start it. Then 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.

4b Classical Logic, Soundness and Completeness for Propositional Logic

Read sections 4.4 – 4.5 of lecture notes.

Monday, 06 March, 17: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
• Kripke semantics of PL
• Soundness and Completeness of ND for Kripke semantics

5 Normal Forms, Automatic Proofs and SAT-Solving

Read chapter 5 of lecture notes.

Monday, 13 March, 17:15

• Normal forms and Horn clauses
• SAT-solving algorithms
• Using SAT solvers

6 First-Order Logic

Read chapter 6 of lecture notes.

Monday, 20 March, 17: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!)

7 Proof Theory of First-Order Logic

Read chapter 7 of lecture notes.

Monday, 03 April, 17:15

• Substitution
• Natural deduction for intuitionistic FOL (ND₁)
• Fitch-Style proofs in ND₁
• Natural deduction for classical FOL (cND₁ = ND₁ + Contra)

8 Semantics of First-Order Logic

Read chapter 8 of lecture notes.

Monday, 17 April, 17:15

• Models of FOL
• Semantics of terms
• Boolean semantics of formulas
• Substitution lemma
• Soundness

9 Extensions and Limits of First-Order Logic

Read chapter 9 of lecture notes.

Monday, 24 April, 17:15

• First-Order logic with equality
• Uniqueness quantifier
• Completeness
• Compactness
• Reachability not expressible

10 Gödel’s Incompleteness Theorem

Read chapter 10 of lecture notes.

Monday, 08 May, 17:15

• Computable functions and axiomatisations
• Primitive recursion and primitive recursive arithmetic
• Expressing provability inside FOL
• Prove Gödel’s incompleteness theorem using inspiration of provability logic [Smo77]

11 First-Order Horn Clauses for Automatic Deduction

Read chapter 11 of lecture notes.

Monday, 15 May, 17:15

• Automatic Deduction and the Cut-Rule
• First-Order Horn Clauses and Logic Programming
• Uniform Proofs

Summary and Exam Preparation

Monday, 22 May, 17: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.