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).
Admission requirements
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.
Additionally, you can easily link MyTimetable to a calendar app on your phone, and schedule changes will be automatically updated in your calendar. You can also choose to receive email notifications about schedule changes. You can enable notifications in Settings after logging in.
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.
Reading list
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
See this page for more information about deadlines and enrolling for courses and exams.
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.
Contact
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.