
Schedule
Spring 2019
Lectures:
13:3015:15 in the
Huygens Sitterzaal.
Practica: 15:3017:15 in the Snellius rooms B02, and B03 starting from 13 February. 
Goal
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.
Description
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.
Literature
Schedule lectures
Nun  Date  Topic  Reading  Extra 
1a  6 Feb  Overview + history of logic  [Var03]  [Ari], [Boo], [Fre] 
1b  The language of propositional logic (PL)  [HR04]:1.1, 1.3 
Ex. 1.1:12  
2a 
13 Feb 
Semantics
of propositional logic 
[HR04]:1.4.1 
Ex. 1.4: 13, 5 
2b 
Mathematical
induction 
[HR04]:1.4.2 
Ex.
1.4:79 

HOMEWORK 1 (deadline 27 February 15:30)  solution 

3a  20 Feb  Semantic equivalence  [HR04]:Def. 1.40  Ex. 1.5:3 
3b  Natural deduction (until rules for implication)  [HR04]:1.2.1 
Ex.
1.2:1 

4 
27 Feb 
Natural deduction  [HR04]:1.2.1  Ex.
1.2:12 
5  6 Mar  Soundness
and completeness of PL 
[HR04]:1.4.3, 1.4.4 
Ex. 1.4:1213 
HOMEWORK 2 (deadline 20 March 15:30)  solution 

13 Mar  No class  
6a  20 Mar  Completeness of PL  [HR04]:1.4..4  Ex. 1.4:16,17 
6b  Semantic tableau
(ST) for propositional logic 
[Kup05] [BDKLM03] 
Ex.
1.2:3 using ST 

27 Mar  No class  
7a  3 Apr  Satisfiability and Horn formulas (slides)  [HR04]:1.5.3  Ex. 1.5:15 
7b  SAT solvers (slides)  [HR04]:1.6  Ex. 1.6:25  
HOMEWORK 3 (deadline 20 Apr)  solution  
8a  10 Apr  Normal forms  [HR04]:1.5.12  Ex. 1.5:4,7,9 
8b 
The
language of predicate
logic (PL) 
[HR04]:2.1 
Ex. 2.1:1,3 2.2:3,4 

9  17 Apr 
Semantics of
predicate logic 
[HR04]:2.2, 2.4 
Ex. 2.2:3,4 2.4:1,5,6,11 
10 
24 Apr 
Natural deduction
for predicate logic 
[HR04]:2.3 
Ex. 2.3:3,7, 9,11,12 
HOMEWORK 4 (deadline 8 May)  solution  
11  1 May  Expressiveness of predicate logic  [HR04]:2.6  Ex: 2.6: 1, 4, 5, 6, 8, 9 
12a  8 May  Semantic
tableau
for predicate logic 
[BDKLM03]:9.2,9.4 
Ex. 9.5:13 
12a  Undecidability of predicate logic (excluding proof of Theorem 2.22)  [HR04]:2.5  
HOMEWORK 5 (Deadline 15 May )  solution  
13  15 May  Trial examination (practicum only) 
Bibliography
[Ari] Aristotle, Organon, 4th century BC.[Boo] George Boole, The Mathematical Analysis of Logic, 1847.
[BDKLM03] J.F.A.K. van Benthem, H.P. van Ditmarsch, J. Ketting, J.S. Lodder, and W.P.M. MeyerViol. Logica voor informatica, derde editie Pearson Education, 2003.
[Fre] Gottlob Frege. Begriffsschrift, 1879.
[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.
[Var03] Moshe Vardi 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.Typesetting in LaTeX
You should write your homework solutions in LaTeX, and hand in the compiled pdf.An easy way to start with LaTeX is to use an online editor, such as Overleaf.
 Create an account;
 Start a new project (with the correct name, e.g., hw1s1234567);
 Paste in the homework template (see here de resulting hw1s1234567.pdf); and
 Hit recompile.
Of course, you could also use your preferred offline LaTeX editor/compiler.
The homework template includes the necessary LaTeX packages and examples for parse trees, formal proofs, and semantic tableaux.
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 before the start of the working class as a single pdf file by email to liacs.logic2019@gmail.com .
 Name your pdf file containing the solution as hwKsN.pdf, where K ranges from 1 to 5 and it is the number of homework, and N is your student number.
 Solutions
sent after the deadline are not accepted.
 Grades of the homeworks will be published on blackboard.