Welcome to the Logic courses! There are two of them, directly following each other in the semester but distributed in the curriculum over years 1 and 2/3. Logic 2 is mandatory in year 2 for computer science students, while it is an elective year 3 for DSAI students. Students of other programmes are free to follow course, depending on how it fits their schedules. Mathematics students may follow Logic 1 and 2 directly in the same year, but be aware that the lectures are at different times.

The two courses have separate websites for easier navigation, but some information applies to both of them.

• Logic 1
• Logic 2

Communication

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 etc.);
• Use the the e-mailbox Logic 1 & 2 in Spring 24-25 <logic25@liacs.leidenuniv.nl> for individual requests.

Content and Setup

The courses are based on the Logic Rondo 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”. Part I of the lecture notes corresponds to Logic 1 and part II to logic 2.

The learning of formal proofs will be accompanied by Proof Rondo, which is proof checker for Fitch-style proofs that are used to present formal proofs in both courses. This proof checker can give you immediate feedback, which you can use for learning, and we will use it in the exam. So make sure to get familiar with it from the beginning through the exercises that we provide and by making up your own exercises.

The courses will each have weekly lectures that will

1. provide a condensed introduction to the material and
2. focus on difficulties that you encounter during the studies of the lecture notes.

Running the risk of repetition: Make sure to study the lecture notes before the corresponding lecture.

Exercises and Homework

For every exercise class, we will distribute an assignment with practice assignments and 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. To be precise, the average grade of your homework, leaving out the worst, will make for 30% of your final grade. Note that not submitting counts as 0 for that homework.

During the exercise classes you can work on the assignment and get help from the tutors. Homework 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.

Other Tools

We will focus on using Proof Rondo. However, if you want more electronic tools to support your learning besides the Proof Rondo, then you can consider the following options.

CoolProof

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.

Currently, this application is not maintained and my not work on newer Android devices.

Jape

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.

References

The lecture notes contains references on all the material. Here is just a summary of standard reference on the subject. You will not need those but they may help to complement your understanding.

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