# Logic 2

Vak
2024-2025

Note: in 2024-25 this course is formally not part of any ongoing curriculum, as this 3 EC Logic 2 course together with the 3 EC Logic 1 course replaces the former 6 EC Introduction to Logic course. However, it will be taught in block 4 (2nd half of Spring semester).

Not applicable.

## Description

Logic is both the origin of computer science and at its very foundation. Digital computers work with logic gates to manipulate bits, but the connection between computer science and logic goes much deeper than that. The history of logic is complex and begins with the philosophy and debates of ancient Greece, India and China, as the study of the relations of propositions and arguments. Motivated by the ambiguity of human language, mathematics of the late 19th century started to develop logic as a field in its own right with the hope of finding a universal language and absolutely correct foundation that would allow the formalisation of all mathematical proofs. This hope was shattered by Gödel's incompleteness and Church's undecidability theorems. But these results required a formal definitions of computation, which lead to the theory of computation that we know today. The boundary between logic and computer science is blurred and insights in logic lead to new methods of computation or visa versa.

In this course, you will learn what formal logic is and about its relationship to computer science. In particular, we will study syntax and proof systems for propositional and first-order logic.

## Course objectives

The course gives an introduction to mathematical logic and its computational aspects. Specifically, after completing the you

• Can construct a formal natural deduction proof of a FOL sequent with equality in tree- and in Fitch-style.

• Can analyse the relation of models and formulas in the Boolean semantics of first-order logic.

• Understand the difference between proofs in classical and intuitionistic logic, and the ramifications for the relation between syntax and semantics.

• Can formulate and prove a property using the induction principle for trees, natural numbers and terms.

• Can evaluate primitive recursive functions and recognise a given function as primitive recursive.
Understand the limits of FOL with respect to expressiveness, computability and provability.

## Timetable

The most updated version of the timetables can be found on the students' website:

In MyTimetable, you can find all course and programme schedules, allowing you to create your personal timetable. Activities for which you have enrolled via MyStudyMap will automatically appear in your timetable.

Questions? Watch the video, read the instructions, or contact the ISSC helpdesk.

Note: Joint Degree students from Leiden/Delft need to combine information from both the Leiden and Delft MyTimetables to see a complete schedule. This video explains how to do it.

## Mode of instruction

Weekly lectures, complemented with lecture notes and some in-depth video tutorials. Exercise classes, during which students can work on and ask questions about the weekly assignments and homework.

## Assessment method

Students will be evaluated on the basis of a written examination complemented with homework assignments. Examination is worth 70% of the final grade. The remaining 30% is from the average grade of homework assignments, where the worst homework grades will be dropped. At least half of the homework assignments have to be completed (empty or non-sense submissions do not count). A retake is offered for the exam. The course is passed with a minimum of 5.5 as final grade. This means that the homework grade can compensate the exam grade.

The main source of information are the lectures and the Logic Rondo lecture notes.

Additionally, the following sources can be consulted for further study.

• Michael R. A. Huth and Mark D. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.

• Jon Barwise and John Etchemendy. Language, Proof and Logic, CSLI Publications, 1999.

• Sara Negri and Jan von Plato. Structural Proof Theory

• Jean H. Gallier. Logic for Computer Science, John Wiley & Sons, 1987.

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

A complete list of literature can be found in the lecture notes.

## Registration

As a student, you are responsible for enrolling on time through MyStudyMap.

In this short video, you can see step-by-step how to enrol for courses in MyStudyMap.
Extensive information about the operation of MyStudyMap can be found here.

There are two enrolment periods per year:

• Enrolment for the fall opens in July

• Enrolment for the spring opens in December

Note:

• It is mandatory to enrol for all activities of a course that you are going to follow.

• Your enrolment is only complete when you submit your course planning in the ‘Ready for enrolment’ tab by clicking ‘Send’.

• Not being enrolled for an exam/resit means that you are not allowed to participate in the exam/resit.

## Remarks

Website: Introduction to Logic 2025

Software
Starting from the 2024/2025 academic year, the Faculty of Science will use the software distribution platform Academic Software. Through this platform, you can access the software needed for specific courses in your studies. For some software, your laptop must meet certain system requirements, which will be specified with the software. It is important to install the software before the start of the course. More information about the laptop requirements can be found on the student website.