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.

Specification

Groups

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 @)