Online Lectures

The lectures are now taking place online on Mondays in the 6th and 7th block (14:15 – 16:00) in the Kaltura Live Room announced on Blackboard. The exercise classes take place in the two blocks afterwards (16:15 – 18:00) in the breakout rooms of the same Live Room. During the lecture, I will use video snippets, quizzes and I will answer as many questions as possible. All the video snippets and the recording of the lectures are available in the channel of the course. You can also subscribe to the channel to receive updates.

We will have in total 13 lectures, starting Monday, 03 February and ending 25 May. Due to events and holidays, there will be no lectures and exercise classes on

• Monday, 23 March,
• Monday, 13 April,
• Monday, 27 April,
• Monday, 04 May, and
• Monday, 01 June.

The exam and retake are scheduled for Monday, 15 June, 14:15 and Tuesday, 07 July, 14:15, respectively.

Question and remarks can be send to LIACS - Introduction to Logic 2020 <itl20@liacs.leidenuniv.nl>.

Lecture Notes

Due to the difficult situation, I decided to write lecture notes for the course. I may not have the time to finish them but at least the second half on first-order logic will be available towards the end of the course.

Exam

The exam will be more like a small individual project to be completed within 24h. It will look exactly like this, but the parameters are individually varied: the picture, the FOL signature and the graph.

Exercises and Homework

There will be weekly sets of exercises that accommodate the course and that can be worked on during the exercise classes. 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 on Blackboard and have to be prepared using LaTeX. A template is available here. The deadline for the homework will always on Friday and the new assignments will be made available on Monday before the lecture.

The rooms are distributed as follows.

Links

• eProspectus/studiegids
• Blackboard

1 Introduction

Monday, 03 February, 14:15

• Course Technicalities
• Introduction and History
• Natural language and introduction propositional logic (PL)

The first assignment is available. Solutions will be available later this week.

Here are the slides of the first lecture with the technicalities and history.

2 Tools and Semantics of Propositional Logic

Monday, 10 February, 14:15

• Iteration and induction for formulas [OLP, Section 7.3]
• Boolean semantics of propositional logic [OLP, Section 7.4]
• Basic notions: satisfiability, tautology, semantic equivalence [OLP, Section 7.5]

The second assignment is available. Note that the template has been updated to help with the new notation.

3 Formal Deduction for Propositional Logic

Monday, 17 February, 14:15

• Some properties of the Boolean semantics [OLP, Section 7.5]
• Deductive systems
• Natural deduction (ND) in sequent style (judgements) for PL [BDKLM03], , and [OLP, Chap. 10]

The third assignment is available. Note that the template has been updated to help with the new notation.

4 Natural Deduction, Classical Logic, Soundness and Completeness for Propositional Logic

Monday, 24 February, 14:15

• The remaining proof rules for ND
• Derivations (proof trees) [OLP, Sec. 10.3]
• Soundness of ND and classical ND (cND) for Boolean PL [OLP, Sec. 10.8]
• Add Proof by contradiction, double negation elimination (DNE) or the law of excluded middle (LEM) to ND to obtain classical ND (cND)
• Soundness of cND for Boolean PL [OLP, Sec. 10.8]
• Completeness of cND [OLP, Sec. 13.6]
• Fitch-style natural deduction [BE99, Chap. 6]

The fourth assignment is available and the template has been updated.

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

5 Normal Forms, Automatic Proofs and SAT-Solving

Monday, 02 March, 14:15

• Demonstration of Jape for ND/cND
• Normal forms and Horn clauses [HR04, Sec. 1.5]
• SAT-solving algorithms [HR04, Sec. 1.6]
• Using SAT solvers

The fifth assignment is available.

6 Predicate Logic

Monday, 09 March, 14:15

• The need for predicate 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!)

The sixth assignment is available and the template has been updated.

7 Proof Theory of Predicate Logic (Part 1)

Monday, 30 March, 14:15 Monday, 16 March, 14:15

• Substitution (lecture notes)

7 Proof Theory of Predicate Logic (Part 2)

Monday, 06 April, 14:15

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

The seventh assignment is available and the template has been updated.

8 Semantics and Soundness of Predicate Logic

Monday, 20 April, 14:15 Monday, 30 March, 14:15

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

The eighth assignment is available and the template has been updated.

9 Completeness and Expressiveness of Predicate Logic

Monday, 11 May, 14:15 Monday, 06 April, 14:15

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

The ninth assignment is available and the template has been updated.

10 Horn Clauses and Automatic Deduction

Monday, 18 May, 14:15 Monday, 20 April, 14:15

• First-Order Horn clauses and logic programming
• Uniform Proofs
• Unification (not exam-relevant)
• Resolution for Horn clause theories (not exam-relevant)

The tenth assignment is available and the template has been updated.

13 Summary and Question Session

Monday, 25 May, 14:15

• Summary of the course content
• Discussion of questions about course content
• Discussion of example exam

Lectures left out in view of time

11 Computability and Undecidability

Monday, 11 May, 14:15

• Computability
• Halting Problem in logic form
• Post correspondence problem (PCP)
• Undecidability of FOL

12 Gödel’s Incompleteness Theorem

Monday, 18 May, 14:15

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

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.