The official textbook is:

*Logic in Computer Science—Modelling and Reasoning about Systems*

2nd Edition

Michael Huth, Mark Ryan

Cambridge University Press

You might find useful some parts of the book:

*Proofs and Types*

Jean-Yves Girard, Yves Lafont, Paul Taylor

Available here.

Some material is in the paper:

*Basic Proof Theory With Applications to Computation*

Stan Wainer

in*Logic of Computation*H. Schwichtenberg, ed.

NATO ASI Series F 157,- Springer-Verlag, 1997.

Slides by Carsten Führmann:

Some notes of mine:

- Notes (for an old course),
- exercise sheet (for an old course)

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.

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.

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

- Prove, in the natural deduction proof system that we have seen so far, the tautologies:

- (A ∧ (B ∨ C)) → ((A ∧ B) ∨ (A ∧ C));
- ((A ∧ B) ∨ (A ∧ C)) → (A ∧ (B ∨ C));
- (A ∨ (B ∧ C)) → ((A ∨ B) ∧ (A ∨ C));
- ((A ∨ B) ∧ (A ∨ C)) → (A ∨ (B ∧ C)).

*15.2.08—Lecture 5* Exercises and *reductio ad absurdum* rule.

- Try to prove all the tautologies (not just those listed in connection to natural deduction) that you find in my notes (for an old course) and in this exercise sheet (for an old course).
- Try to prove Peirce's law: (((A → B) → A) → A).
- Please bring in class the exercises you found most difficult and we'll see what we can do.

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

- Write some formulae and prove, in natural deduction, that they are equivalent to their De Morgan duals; please bring to the next lecture the cases for which you have difficulties.
- Do Homework 1 in this exercise sheet (for an old course), without looking at the solutions (try to find, for Peirce's law, a different proof from the one seen in class).
- Do exercises 4.6 and 4.8 in my notes (for an old course).

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

- Prove soundness for the natural deduction system for propositional classical logic in my notes (for an old course), by structural induction on proofs.

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

- Try to prove in the given system all the propositional tautologies that you find in my notes (for an old course) and in this exercise sheet (for an old course).
- Prove the soundness of the implication-left rule.

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

- Please have a look at the coursework suggested literature and try quickly to form groups.

*7.3.08—Lecture 11* *Quantifier* rules for the sequent calculus.

- Prove in the system we saw in class all the tautologies of exercise 6.7 in my notes (for an old course).
- In particular, prove that ∃x.∀y.(p(x) → p(y)).

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

- Prove that the cut rule is sound.
- Find the general shape of proofs of Statman tautologies, in the cut-free sequent calculus (you can find an accessible definition of Statman tautologies at p. 14 of this paper, read Definition 3.7 and Example 3.8). How do these proofs grow in the size of Statman tautologies?

*14.3.08—Lecture 13* Tutorial about the sequent calculus.

- Solve the two exercises in this test (they are indicative of real exam exercises).

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

- You find what I presented in class in Wainer's paper (Sect. 3, do not pay much attention to the different cut rank, there are several variants).

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

- You will find what I presented in class in Wainer's paper (Sect. 3 and 1).

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

- Führmann's slides (part 4) contain the definitions and notions about modal logic, but the best treatment is in the textbook.
- Do the examples at pp. 18 and 21 in Führmann's slides (part 4).

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

- Prove the statements in the last slide of Führmann's slides (part 4) `Correspondence Theory´.
- About the Curry-Howard isomorphism, please read Chapter 3 of Proofs and Types, especially section 3.5.

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

- Propositional logic and truth tabling: any source will do fine, for example the slides by Führmann, Part 1.
- Proof system: read up to Definition 2.2, and following explanations, in The Complexity of Propositional Proofs by Alasdair Urquhart.
- Natural deduction: Führmann's slides, Part 2.
- Sections 4 and 6 of my notes (for an old course).
- Soundness and completeness for natural deduction: Führmann's slides, Part 3 (only the statements of the two theorems and what is necessary to understand them, ignore the rules for the quantifiers).
- Statement and meaning of the cut elimination theorem, and the general idea of its proof: section 3 in Wainer's paper.
- Completeness theorem for propositional logic (general idea of the proof): section 1 in Wainer's paper.
- Modal logic: Führmann's slides, Part 4 and textbook.

- Coursework (handout for topic 4, and corresponding, executable Prolog program)
- Group Breakdown Chart
- Questionnaire

*Topic 1—NP vs coNP*Kris Nobes, Mike Davis and Rich Harris (group A) and Ute Kandler, Rok Orel (group B); presentation on 25.4 (during the lecture time and following hour).*Topic 2—Frege vs extended Frege*Adam Gundry, Tom McLean, Peter Dennis, Robert Mead; presentation on 29.4 (during the lecture time).*Topic 3—The correspondence between natural deduction and sequent calculus*Remi Bernal, Jean-François Marquet; presentation on 22.4 (during the lecture time).*Topic 4—The undecidability of first order logic*Zong Guo, Matthew Barsby, Daniel Fowles, Tor Erik Linnerud; presentation on 29.4, from 12:15 to 13:05, in room 1WN 3.12.

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