# Introduction to Logic, Spring 2024

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:

Week | Practical | Lecture |
---|---|---|

1 | None | Lecture 1 (Tue, 06 Feb, 13:15) |

2 | Mon, 12 Feb, 15:15 | Lecture 2 (Tue, 13 Feb, 13:15) |

3 | Mon, 19 Feb, 15:15 | Lecture 3 (Tue, 20 Feb, 13:15) |

4 | Mon, 26 Feb, 15:15 | Lecture 4 (Tue, 27 Feb, 13:15) |

5 | Mon, 04 Mar, 15:15 | Lecture 5 (Tue, 05 Mar, 13:15) |

6 | Mon, 11 Mar, 15:15 | Lecture 6 (Tue, 12 Mar, 13:15) |

7 | Mon, 18 Mar, 15:15 | Lecture 7 (Tue, 19 Mar, 13:15) |

8 | Mon, 25 Mar, 15:15 | None on Tue, 26 Mar, 13:15 |

9 | None | Lecture 8 (Tue, 02 Apr, 13:15) |

10 | Mon, 08 Apr, 15:15 | Lecture 9 (Tue, 09 Apr, 13:15) |

11 | Mon, 15 Apr, 15:15 | Lecture 10 (Tue, 16 Apr, 13:15) |

12 | Mon, 22 Apr, 15:15 | Lecture 11 (Tue, 23 Apr, 13:15) |

13 | Mon, 29 Apr, 15:15 | Lecture 12 (Tue, 30 Apr, 13:15) |

14 | Mon, 06 May, 15:15 | Lecture 13 (Tue, 07 May, 13:15) |

15 | Mon, 13 May, 15:15 | None on Tue, 14 May, 13:15 |

16 | None | Exam Prep. (Tue, 21 May, 13:15) |

17 | Backup Mon, 27 May, 15:15 | Backup (Tue, 28 May, 13:15) |

## 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.

Week | Practical Time | Group 1 | Group 2 | Group 3 | Group 4 | Group 5 |
---|---|---|---|---|---|---|

1 | None | — | — | — | — | — |

2 | Mon, 12 Feb, 15:15 | C1 | C1 | C3 | C3 | C3 |

3 | Mon, 19 Feb, 15:15 | H1.06-1.09 | H2.26 | C3 | C3 | C3 |

4 | Mon, 26 Feb, 15:15 | C1 | C1 | C3 | C3 | C3 |

5 | Mon, 04 Mar, 15:15 | C1 | C1 | C3 | C3 | C3 |

6 | Mon, 11 Mar, 15:15 | H1.06-1.09 | H2.26 | C3 | C3 | C3 |

7 | Mon, 18 Mar, 15:15 | H1.06-1.09 | C1 | C1 | C1 | C1 |

8 | Mon, 25 Mar, 15:15 | Sitter | Sitter | C3 | C3 | C3 |

9 | None | — | — | — | — | |

10 | Mon, 08 Apr, 15:15 | Sitter | Sitter | C3 | C3 | C3 |

11 | Mon, 15 Apr, 15:15 | Sitter | Sitter | C3 | C3 | C3 |

12 | Mon, 22 Apr, 15:15 | H1.06-1.09 | H2.26 | C3 | C3 | C3 |

13 | Mon, 29 Apr, 15:15 | C1 | C1 | C3 | C3 | C3 |

14 | Mon, 06 May, 15:15 | H1.06-1.09 | H2.26 | C3 | C3 | C3 |

15 | Mon, 13 May, 15:15 | Sitter | Sitter | C3 | C3 | C3 |

16 | None | — | — | — | — | |

17 | Mon, 27 May, 15:15 (Backup) |
Sitter | Sitter | C3 | C3 | C3 |

### 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.

The exam will take place in ANS and you have 4 hours to complete it. Officially, the exam runs for 3 hours but the extra hour accounts for possible technical issues. You may find instructions with the exam in ANS, and an example of how the exam looks like on Brightspace.

During the exam, you will be using Proof Rondo. So make sure to be fluent in using it.

## 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.