CM30071—Logic and Its Applications

1 Textbooks and Other Sources

The official textbook is:

You might find useful some parts of the book:

Some material is in the paper:

Slides by Carsten Führmann:

Some notes of mine:

2 News

This course only has two lectures per week because students are supposed to do some reading by themselves; please follow the suggestions for exercises and reading that you find here!

8.4.08 There will be extra tutorials on Friday 11.4 and on Friday 18.4, at 13:15 in 3WN 3.8.

3 Course Info

In the following, I will link some material distributed or used in the past for this and other courses: please disregard any information related to the organisation of those courses: it is not valid any more. Also, keep in mind that I might change the presentation, sometimes substantially. The material that we cover and that you are supposed to understand is clearly indicated below.

Lectures, Topics and Suggested Exercises

29.1.08—Lecture 1 Introduction to the course.

5.2.08—Lecture 2 Language of propositional logic and truth tabling, further introduction to the course.

8.2.08—Lecture 3 Definition of proof system, two rules of natural deduction (and and implication introduction).

12.2.08—Lecture 4 Rules of natural deduction: and and implication elimination, or introduction and elimination; examples.

    1. (A ∧ (B ∨ C)) → ((A ∧ B) ∨ (A ∧ C));
    2. ((A ∧ B) ∨ (A ∧ C)) → (A ∧ (B ∨ C));
    3. (A ∨ (B ∧ C)) → ((A ∨ B) ∧ (A ∨ C));
    4. ((A ∨ B) ∧ (A ∨ C)) → (A ∨ (B ∧ C)).

15.2.08—Lecture 5 Exercises and reductio ad absurdum rule.

19.2.08—Lecture 6 Exercise on Peirce's law and definition of sequent.

22.2.08—Lecture 7 Exercises and a reminder of soundness and completeness theorems.

26.2.08—Lecture 8 Comments and suggestions about proving a soundness theorem. Introduction to the sequent calculus.

29.2.08—Lecture 9 Gentzen additive sequent system for propositional classical logic.

4.3.08—Lecture 10 Comments on the coursework; hint about proving the soundness theorem for natural deduction.

7.3.08—Lecture 11 Quantifier rules for the sequent calculus.

11.3.08—Lecture 12 The cut rule and an introduction to cut elimination.

14.3.08—Lecture 13 Tutorial about the sequent calculus.

8.4.08—Lecture 14 Motivation and general idea of the cut elimination theorem.

11.4.08—Lectures 15 and 16 Main cases of the cut elimination theorem and completeness theorem, both for propositional logic; solution to problem 1 in this test.

15.4.08—Lecture 17 Introduction to modal logic and definition of Kripke model and forcing.

18.4.08—Lectures 18 and 19 Validity of formulae in modal logic; Curry-Howard isomorphism; solution to problem 3 in this past exam.

22.4.08—Lecture 20 Coursework presentation.

25.4.08—Lectures 21 and 22 Coursework presentations.

29.4.08—Lectures 23 and 24 Coursework presentations.

2.5.08—Lectures 25 and 26 Tutorial, Q&A.

Material Covered and to Be Prepared for the Exam

Past Exams

4 Coursework

The coursework has been set on 4 March 2008 (in class and on this web page) and it should be handed in on 28 April 2008 at 12:00.



5 Office Hours

When you want to talk to me, just drop me an email and we'll arrange for an appointment.

2.5.2008 Alessio Guglielmi email (replace AT by @)