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;
• a Kaltura channel for recordings and instruction videos; and
• Zoom for stream of lectures (see Brightspace calendar).

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 quick communication (questions about exercises, during the exam etc.);
• the Brightspace forum for discussions that may need a lot of math and longer answers; or
• the e-mailbox 2122-S2 Introduction to Logic <itl22@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, 07 February and ending 16 May. Due to events and holidays, there will be no lectures in the weeks of

• Monday, 28 March (test week) and
• Monday, 18 April (Easter).

In the official schedules is a lecture planned on 23 May, but we keep this date as backup if something has to be moved during the semester.

The course ends with an exam, which will be held online, see below for details. Exam and retake are scheduled for Monday, 20 June, 09:00 and Thursday, 21 July, 09:00, respectively.

Exam

The exam will be more like a small individual project, running from 9:00 to 18:00 on the day of the exam. You can see here an old example, which is subject to change for this year.

Lectures and Lecture Notes

The lectures take place on Mondays in the 6th and 7th block (14:15 – 16:00) in Gorleaus 03. These lectures will also be available in a Zoom live stream and as recording afterwards. I will try to record these as best as I can, but I cannot make any guarantees for the quality because we will be using the blackboard. Additionally, there are lecture notes available that complement the lecture and 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 the two blocks after the lecture (16:15 – 18:00) in Gorleaus 03 and Snellius 402, 405 and 408. I hope that we can get another room, otherwise we have to combine two groups with tutors in GORL/03.

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 deadline for the homework will always on Friday and the new assignments will be made available on Monday before the lecture.

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
  • Regular practice and repetition helps to build these connections
  • Use 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
  • Allocate some fixed time during which you practise and plan what you want to do during that 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
  • Solve your problems before repeating
  • Approach exercises slowly and take the time to think about what you are doing, 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
  • Come prepared to the exercise classes
  • Explain the material to others, teaching is the best method of learning

1 Introduction

Monday, 07 February, 14:15

• Course Technicalities
• Introduction and History
• Overview
• Preliminaries: Maps, Induction [OLP, Ch. 69], Formal Languages and Context-free Grammars

2 Language and Tools of Propositional Logic

Monday, 14 February, 14:15

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

3 Semantics of Propositional Logic

Monday, 21 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, 28 February, 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, 07 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
• Kripke semantics of PL
• Soundness and Completeness of ND for Kripke semantics

6 Normal Forms, Automatic Proofs and SAT-Solving

Monday, 14 March, 14:15

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

7 First-Order Logic

Monday, 21 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, 04 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, 25 April, 14:15 (Monday, 11 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, 02 May, 14:15 (Monday, 25 April, 14:15)

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

11 Gödel’s Incompleteness Theorem

Monday, 09 May, 14:15 (Monday, 02 May, 14:15)

• Expressing provability inside FOL
• Provability logic
• Prove Gödel’s incompleteness theorem using provability logic [Smo77]

12 First-Order Horn Clauses for Automatic Deduction

Monday, 16 May, 14:15 (Monday, 09 May, 14:15)

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

13 Summary and Exam Preparation

Monday, 23 May, 14:15 (Monday, 16 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.