LIACS > Marcello M. Bonsangue > Introduction to Logic (I&E)
Lecturer Keyvan Azadbakht
Marcello Bonsangue
Assistants Stef van Dijk
Vera Schous
Levi Vos
Course num.
Prerequisites Fundamentele Informatica 1
Language English
11 June 2018, 14:00-17:00, room Gorlaus 01 (activity 12857).
12 July 2018 14:00-17:00,  
room Gorlaus Havingzaal (activity 12858)
Schedule Spring 2018

6, 9, 13, 156, 20, 23, 27, 30
6, 9, 20, 23, 27
3, 6, 10, 13, 17, 20, 24, 
1, 4, 8, 15, 18, 25
June 1

Lectures: 13:30-15:15 in
Huygens 106-109 on 6/02, 20/03, 03/04; Huygens 211/214 all other dates. 

Practica: 09:00-10:45 in
Snellius 313 and Snellius 412*

* From March 23rd on the practica will be only in Snellius 313.


This course gives an introduction to the field of mathematical logic by presenting the syntax and semantics of propositional logic and of the richer language of predicate logic. The goal is to describe and investigate the above logics by finitary methods, and to train students in formalizing specifications and in verifying properties of systems.


Originally logic was used by the Greek Sophists to demonstrate the correctness of their argument in formal debates. The ambiguity of human languages asked for formulation of logic in a symbolic formal language.

Only towards the end of the 19th century logic has been formulated in the language of mathematics, and in particular of algebra, making it a useful tool to solve mathematical problems. In the same period the language used to prove theorems from mathematics begun suffering the same problems of natural language, showing many paradoxes. Logic was proposed as the foundational language of mathematics, but several limitation where soon discovered.

More recently logic has become the language of computer science, just as calculus is the language of many engineering discipline. In this course we will study propositional and predicate logic, their proof theory, their limitation, as well as some of their applications in computer science.


Here the image of the book
Michael R. A. Huth and Mark D. Ryan Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004 (ISBN 052154310X).

Schedule lectures

Nun Date Topic Reading Extra
1a 6 Feb Overview + history of logic [V03]
1b The language of propositional logic (PL) [HR04]:1.1, 1.3
Ex. 1.1:1-2
14 Feb
Semantics of propositional logic
Ex. 1.4: 1-3, 5

Mathematical induction
Ex. 1.4:7-9

HOMEWORK 1 (deadline 2 March)
3a 20 Feb Semantic entailment [HR04]:Def. 1.34
3b Natural deduction (until rules for implication) [HR04]:1.2.1
Ex. 1.2:1-2
27 Feb
Natural deduction (until rules for negation)  [HR04]:1.2.1 Ex. 1.2:1-2
6 Mar
Natural deduction
Ex. 1.2:3,5
5b Soundness and completeness of PL
Ex. 1.4:12, 13,16,17
HOMEWORK 2 (deadline 23 March)
13 Mar No class
6a 20 Mar completeness of PL [HR04]:1.4..4 Ex. 1.4:16,17
6b Semantic tableau for propositional logic
Ex. 1.2.2
7 27 Mar Validity and conjunctive normal form [HR04]:1.5.1-2 Ex. 1.5:3,4, 7,9

HOMEWORK 3 (deadline 10 Apr)
8a 3 Apr Satisfiability and Horn formulas [HR04]:1.5.3 Ex. 1.5:15
SAT solvers [HR04]:1.6 Ex. 1.6:2-5
10 Apr The language of predicate logic (PL)
[HR04]:2.1, 2.2
Ex. 2.1:1,3
17 Apr
Natural deduction for predicate logic
Ex. 2.3:3,7,
HOMEWORK 4 (deadline 4 May) solution
11 24 Apr
Semantics of predicate logic
Ex. 2.4:1,5,6
12a 1 May
Undecidability of predicate logic  (excluding  proof of Theorem 2.22) [HR04]:2.5
Expressivity of predicate logic
Ex: 2.6: 1, 4, 5, 6, 8, 9
13a 8 May Expressivity of predicate logic [HR04]:2.6 Ex: 2.6: 1, 4, 5, 6, 8, 9
13a Semantic tableau for predicate logic
Ex. 2.3.9,

HOMEWORK 5 (Deadline 25 May )
13 10 May Final discussion


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

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

[Kup05] Jan Kuper. Overview of proposition and predicate logic, notes 2005.

[V03] Moshe Vard.i A Brief History of Logic, 2003.

LaTeX and proofs

For writing natural deduction proofs in LaTeX you can use Paul Taylor's macro's voor proof boxes. Here is an example of a proof in natural deduction from the book in .tex en .pdf.

Exam and homework information

  • Examination is worth 70% of the final grade (with a minimum of 5.5). The remaining 30% is from the average grade of theof the 4 best out of the 5 homeworks.
  • Write clearly your name and student number in your homework solution.
  • Return your homework solution as a single pdf file by email to t.b.a..
  • Name your pdf file containing the solution as HWxxNameSurname.pdf, where xx ranges from 1 to 5 and it is the number of homework.
  • Solutions sent after the deadline are not accepted.
  • Grades  of the homeworks will be published on blackboard.

Past examinations